[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/const.i (no preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
  G ∈ [--..--]
  I ∈ {2}
  J ∈ {8}
  v ∈ [--..--]
  X ∈ {0}
  s.i1 ∈ {3}
   .i2 ∈ {4}
  t[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {3}
   [3] ∈ {4}
   [4] ∈ {5}
   [5] ∈ {6}
   [6..9] ∈ {0}
[value] computing for function const_formal <- main.
        Called from tests/value/const.i:84.
[value] Called Frama_C_show_each([-2147483648..2147483647])
[value] Recording results for const_formal
[value] Done for function const_formal
[value] computing for function const_formal <- main.
        Called from tests/value/const.i:85.
[value] Called Frama_C_show_each({42})
[value] Recording results for const_formal
[value] Done for function const_formal
[value] computing for function modify_I <- main.
        Called from tests/value/const.i:87.
[value] Called Frama_C_show_each({2})
[value] computing for function pointer_to_const <- modify_I <- main.
        Called from tests/value/const.i:39.
[value] Called Frama_C_show_each({2; 3})
[value] Called Frama_C_show_each_dead()
[value] Recording results for pointer_to_const
[value] Done for function pointer_to_const
[value] computing for function const_destination <- modify_I <- main.
        Called from tests/value/const.i:40.
[value] Called Frama_C_show_each({0; 2; 3})
[value] Called Frama_C_show_each({{ &I }})
[value] Recording results for const_destination
[value] Done for function const_destination
[value] Recording results for modify_I
[value] Done for function modify_I
[value] computing for function modify_J <- main.
        Called from tests/value/const.i:88.
[value] Called Frama_C_show_each({8})
[value] computing for function pointer_to_const <- modify_J <- main.
        Called from tests/value/const.i:46.
[value] Called Frama_C_show_each({8; 9})
[value] Called Frama_C_show_each_dead()
[value] Recording results for pointer_to_const
[value] Done for function pointer_to_const
[value] computing for function const_destination <- modify_J <- main.
        Called from tests/value/const.i:47.
[value] Called Frama_C_show_each({0; 8; 9})
[value] Called Frama_C_show_each({{ &J }})
[value] Recording results for const_destination
[value] Done for function const_destination
[value] Recording results for modify_J
[value] Done for function modify_J
[value] computing for function modify_s <- main.
        Called from tests/value/const.i:89.
[value] Called Frama_C_show_each({3})
[value] computing for function pointer_to_const <- modify_s <- main.
        Called from tests/value/const.i:53.
[value] Called Frama_C_show_each({4})
[value] Called Frama_C_show_each_dead()
[value] Recording results for pointer_to_const
[value] Done for function pointer_to_const
[value] computing for function const_destination <- modify_s <- main.
        Called from tests/value/const.i:54.
[value] Called Frama_C_show_each({0; 4})
[value] Called Frama_C_show_each({{ &s + {4} }})
[value] Recording results for const_destination
[value] Done for function const_destination
[value] Recording results for modify_s
[value] Done for function modify_s
[value] computing for function modify_t <- main.
        Called from tests/value/const.i:90.
[value] Called Frama_C_show_each({6})
[value] computing for function pointer_to_const <- modify_t <- main.
        Called from tests/value/const.i:60.
[value] Called Frama_C_show_each({4})
[value] Called Frama_C_show_each_dead()
[value] Recording results for pointer_to_const
[value] Done for function pointer_to_const
[value] computing for function const_destination <- modify_t <- main.
        Called from tests/value/const.i:61.
[value] Called Frama_C_show_each({3})
[value] Called Frama_C_show_each({{ &t + {8} }})
[value] Recording results for const_destination
[value] Done for function const_destination
[value] Recording results for modify_t
[value] Done for function modify_t
[value] computing for function constrain_G <- main.
        Called from tests/value/const.i:91.
tests/value/const.i:71:[value] warning: assertion got status unknown.
[value] Called Frama_C_show_each({1; 4})
[value] Recording results for constrain_G
[value] Done for function constrain_G
[value] computing for function pointer_to_const_logic <- main.
        Called from tests/value/const.i:93.
[value] Recording results for pointer_to_const_logic
[value] Done for function pointer_to_const_logic
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function const_destination:
  I ∈ {0; 2; 3}
  J ∈ {0; 8; 9}
  s.i1 ∈ {3; 4}
   .i2 ∈ {0; 4}
  t[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {0; 3}
   [3] ∈ {0; 4}
   [4] ∈ {5}
   [5] ∈ {6; 7}
   [6..9] ∈ {0}
[value:final-states] Values at end of function const_formal:
  i ∈ [--..--]
[value:final-states] Values at end of function constrain_G:
  r ∈ {3; 5}
[value:final-states] Values at end of function pointer_to_const:
  I ∈ {0; 2; 3}
  J ∈ {0; 8; 9}
  s.i1 ∈ {3; 4}
   .i2 ∈ {0; 4}
  t[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {3}
   [3] ∈ {0; 4}
   [4] ∈ {5}
   [5] ∈ {6; 7}
   [6..9] ∈ {0}
[value:final-states] Values at end of function modify_I:
  I ∈ {0; 2; 3}
  J ∈ {8}
  s.i1 ∈ {3}
   .i2 ∈ {4}
  t[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {3}
   [3] ∈ {4}
   [4] ∈ {5}
   [5] ∈ {6}
   [6..9] ∈ {0}
[value:final-states] Values at end of function modify_J:
  I ∈ {0; 2; 3}
  J ∈ {0; 8; 9}
  s.i1 ∈ {3}
   .i2 ∈ {4}
  t[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {3}
   [3] ∈ {4}
   [4] ∈ {5}
   [5] ∈ {6}
   [6..9] ∈ {0}
[value:final-states] Values at end of function modify_s:
  I ∈ {0; 2; 3}
  J ∈ {0; 8; 9}
  s.i1 ∈ {3; 4}
   .i2 ∈ {0; 4}
  t[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {3}
   [3] ∈ {4}
   [4] ∈ {5}
   [5] ∈ {6}
   [6..9] ∈ {0}
[value:final-states] Values at end of function modify_t:
  I ∈ {0; 2; 3}
  J ∈ {0; 8; 9}
  s.i1 ∈ {3; 4}
   .i2 ∈ {0; 4}
  t[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {0; 3}
   [3] ∈ {0; 4}
   [4] ∈ {5}
   [5] ∈ {6; 7}
   [6..9] ∈ {0}
[value:final-states] Values at end of function pointer_to_const_logic:
  J ∈ {0; 8; 9; 12}
[value:final-states] Values at end of function main:
  I ∈ {0; 2; 3}
  J ∈ {0; 8; 9; 12}
  s.i1 ∈ {3; 4}
   .i2 ∈ {0; 4}
  t[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {0; 3}
   [3] ∈ {0; 4}
   [4] ∈ {5}
   [5] ∈ {6; 7}
   [6..9] ∈ {0}
[from] Computing for function const_destination
[from] Done for function const_destination
[from] Computing for function const_formal
[from] Done for function const_formal
[from] Computing for function constrain_G
[from] Done for function constrain_G
[from] Computing for function pointer_to_const
[from] Done for function pointer_to_const
[from] Computing for function modify_I
[from] Done for function modify_I
[from] Computing for function modify_J
[from] Done for function modify_J
[from] Computing for function modify_s
[from] Done for function modify_s
[from] Computing for function modify_t
[from] Done for function modify_t
[from] Computing for function pointer_to_const_logic
[from] Done for function pointer_to_const_logic
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
       These dependencies hold at termination for the executions that terminate:
[from] Function const_destination:
  I FROM p (and SELF)
  J FROM p (and SELF)
  s.i2 FROM p (and SELF)
  t[2] FROM p (and SELF)
[from] Function const_formal:
  NO EFFECTS
[from] Function constrain_G:
  NO EFFECTS
[from] Function pointer_to_const:
  I FROM p (and SELF)
  J FROM p (and SELF)
  s.i2 FROM p (and SELF)
  t[3] FROM p (and SELF)
[from] Function modify_I:
  I FROM I; v (and SELF)
  J FROM v (and SELF)
  s.i2 FROM v (and SELF)
  t[2..3] FROM v (and SELF)
[from] Function modify_J:
  I FROM v (and SELF)
  J FROM J; v (and SELF)
  s.i2 FROM v (and SELF)
  t[2..3] FROM v (and SELF)
[from] Function modify_s:
  I FROM v (and SELF)
  J FROM v (and SELF)
  s.i1 FROM v; s.i1 (and SELF)
   .i2 FROM v (and SELF)
  t[2..3] FROM v (and SELF)
[from] Function modify_t:
  I FROM v (and SELF)
  J FROM v (and SELF)
  s.i2 FROM v (and SELF)
  t[2..3] FROM v (and SELF)
   [5] FROM v; t[5] (and SELF)
[from] Function pointer_to_const_logic:
  J FROM v; p (and SELF)
[from] Function main:
  I FROM I; v (and SELF)
  J FROM J; v (and SELF)
  s.i1 FROM v; s.i1 (and SELF)
   .i2 FROM v (and SELF)
  t[2..3] FROM v (and SELF)
   [5] FROM v; t[5] (and SELF)
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function const_destination:
          I; J; s.i2; t[2]
[inout] Inputs for function const_destination:
          I; J; s.i2; t[2]
[inout] Out (internal) for function const_formal:
          i
[inout] Inputs for function const_formal:
          v
[inout] Out (internal) for function constrain_G:
          r
[inout] Inputs for function constrain_G:
          G
[inout] Out (internal) for function pointer_to_const:
          I; J; s.i2; t[3]
[inout] Inputs for function pointer_to_const:
          I; J; s.i2; t[3]
[inout] Out (internal) for function modify_I:
          I; J; s.i2; t[2..3]
[inout] Inputs for function modify_I:
          I; J; v; s.i2; t[2..3]
[inout] Out (internal) for function modify_J:
          I; J; s.i2; t[2..3]
[inout] Inputs for function modify_J:
          I; J; v; s.i2; t[2..3]
[inout] Out (internal) for function modify_s:
          I; J; s; t[2..3]
[inout] Inputs for function modify_s:
          I; J; v; s; t[2..3]
[inout] Out (internal) for function modify_t:
          I; J; s.i2; t{[2..3]; [5]}
[inout] Inputs for function modify_t:
          I; J; v; s.i2; t{[2..3]; [5]}
[inout] Out (internal) for function pointer_to_const_logic:
          J
[inout] Inputs for function pointer_to_const_logic:
          v
[inout] Out (internal) for function main:
          I; J; s; t{[2..3]; [5]}
[inout] Inputs for function main:
          G; I; J; v; s; t{[2..3]; [5]}
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
  G ∈ [--..--]
  I ∈ {2}
  J ∈ {8}
  v ∈ [--..--]
  X ∈ {0}
  s.i1 ∈ {3}
   .i2 ∈ {4}
  t[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {3}
   [3] ∈ {4}
   [4] ∈ {5}
   [5] ∈ {6}
   [6..9] ∈ {0}
[value] computing for function const_formal <- main.
        Called from tests/value/const.i:84.
[value] Called Frama_C_show_each([-2147483648..2147483647])
tests/value/const.i:21:[value] warning: out of bounds write. assert \valid(&i);
tests/value/const.i:21:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
[value] Recording results for const_formal
[value] Done for function const_formal
[value] computing for function const_formal <- main.
        Called from tests/value/const.i:85.
[value] Called Frama_C_show_each({42})
[value] Recording results for const_formal
[value] Done for function const_formal
[value] computing for function modify_I <- main.
        Called from tests/value/const.i:87.
[value] Called Frama_C_show_each({2})
tests/value/const.i:38:[value] warning: out of bounds write. assert \valid(&I);
tests/value/const.i:38:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
[value] computing for function pointer_to_const <- modify_I <- main.
        Called from tests/value/const.i:39.
[value] Called Frama_C_show_each({2})
tests/value/const.i:26:[value] warning: out of bounds write. assert \valid(p);
tests/value/const.i:26:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
[value] Recording results for pointer_to_const
[value] Done for function pointer_to_const
[value] computing for function const_destination <- modify_I <- main.
        Called from tests/value/const.i:40.
[value] Called Frama_C_show_each({2})
tests/value/const.i:32:[value] warning: out of bounds write. assert \valid(p);
tests/value/const.i:32:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
[value] Recording results for const_destination
[value] Done for function const_destination
[value] Recording results for modify_I
[value] Done for function modify_I
[value] computing for function modify_J <- main.
        Called from tests/value/const.i:88.
[value] Called Frama_C_show_each({8})
[value] computing for function pointer_to_const <- modify_J <- main.
        Called from tests/value/const.i:46.
[value] Called Frama_C_show_each({8; 9})
[value] Recording results for pointer_to_const
[value] Done for function pointer_to_const
[value] computing for function const_destination <- modify_J <- main.
        Called from tests/value/const.i:47.
[value] Called Frama_C_show_each({8; 9})
[value] Called Frama_C_show_each({{ &J }})
[value] Recording results for const_destination
[value] Done for function const_destination
[value] Recording results for modify_J
[value] Done for function modify_J
[value] computing for function modify_s <- main.
        Called from tests/value/const.i:89.
[value] Called Frama_C_show_each({3})
tests/value/const.i:52:[value] warning: out of bounds write. assert \valid(&s.i1);
tests/value/const.i:52:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
[value] computing for function pointer_to_const <- modify_s <- main.
        Called from tests/value/const.i:53.
[value] Called Frama_C_show_each({4})
[value] Recording results for pointer_to_const
[value] Done for function pointer_to_const
[value] computing for function const_destination <- modify_s <- main.
        Called from tests/value/const.i:54.
[value] Called Frama_C_show_each({4})
[value] Recording results for const_destination
[value] Done for function const_destination
[value] Recording results for modify_s
[value] Done for function modify_s
[value] computing for function modify_t <- main.
        Called from tests/value/const.i:90.
[value] Called Frama_C_show_each({6})
tests/value/const.i:59:[value] warning: out of bounds write. assert \valid(&t[5]);
tests/value/const.i:59:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
[value] computing for function pointer_to_const <- modify_t <- main.
        Called from tests/value/const.i:60.
[value] Called Frama_C_show_each({4})
[value] Recording results for pointer_to_const
[value] Done for function pointer_to_const
[value] computing for function const_destination <- modify_t <- main.
        Called from tests/value/const.i:61.
[value] Called Frama_C_show_each({3})
[value] Recording results for const_destination
[value] Done for function const_destination
[value] Recording results for modify_t
[value] Done for function modify_t
[value] computing for function constrain_G <- main.
        Called from tests/value/const.i:91.
[value] Called Frama_C_show_each({1; 4})
[value] Recording results for constrain_G
[value] Done for function constrain_G
[value] computing for function pointer_to_const_logic <- main.
        Called from tests/value/const.i:93.
tests/value/const.i:80:[value] warning: out of bounds write. assert \valid(p);
tests/value/const.i:80:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
[value] Recording results for pointer_to_const_logic
[value] Done for function pointer_to_const_logic
[value] Recording results for main
[value] done for function main
tests/value/const.i:21:[value] assertion 'Value,mem_access' got final status invalid.
tests/value/const.i:26:[value] assertion 'Value,mem_access' got final status invalid.
tests/value/const.i:38:[value] assertion 'Value,mem_access' got final status invalid.
tests/value/const.i:52:[value] assertion 'Value,mem_access' got final status invalid.
tests/value/const.i:59:[value] assertion 'Value,mem_access' got final status invalid.
tests/value/const.i:80:[value] assertion 'Value,mem_access' got final status invalid.
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function const_destination:
  J ∈ {0}
[value:final-states] Values at end of function const_formal:
  
[value:final-states] Values at end of function constrain_G:
  r ∈ {3; 5}
[value:final-states] Values at end of function pointer_to_const:
  NON TERMINATING FUNCTION
[value:final-states] Values at end of function modify_I:
  J ∈ {8}
[value:final-states] Values at end of function modify_J:
  J ∈ {0; 8; 9}
[value:final-states] Values at end of function modify_s:
  J ∈ {0; 8; 9}
[value:final-states] Values at end of function modify_t:
  J ∈ {0; 8; 9}
[value:final-states] Values at end of function pointer_to_const_logic:
  
[value:final-states] Values at end of function main:
  J ∈ {0; 8; 9}
[from] Computing for function const_destination
[from] Done for function const_destination
[from] Computing for function const_formal
[from] Done for function const_formal
[from] Computing for function constrain_G
[from] Done for function constrain_G
[from] Computing for function pointer_to_const
[from] Non-terminating function pointer_to_const (no dependencies)
[from] Done for function pointer_to_const
[from] Computing for function modify_I
[from] Done for function modify_I
[from] Computing for function modify_J
[from] Done for function modify_J
[from] Computing for function modify_s
[from] Done for function modify_s
[from] Computing for function modify_t
[from] Done for function modify_t
[from] Computing for function pointer_to_const_logic
[from] Done for function pointer_to_const_logic
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
       These dependencies hold at termination for the executions that terminate:
[from] Function const_destination:
  J FROM p
[from] Function const_formal:
  NO EFFECTS
[from] Function constrain_G:
  NO EFFECTS
[from] Function pointer_to_const:
  NON TERMINATING - NO EFFECTS
[from] Function modify_I:
  J FROM v (and SELF)
[from] Function modify_J:
  J FROM J; v (and SELF)
[from] Function modify_s:
  J FROM v (and SELF)
[from] Function modify_t:
  J FROM v (and SELF)
[from] Function pointer_to_const_logic:
  J FROM v; p (and SELF)
[from] Function main:
  J FROM J; v (and SELF)
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function const_destination:
          J
[inout] Inputs for function const_destination:
          I; J; s.i2; t[2]
[inout] Out (internal) for function const_formal:
          \nothing
[inout] Inputs for function const_formal:
          v
[inout] Out (internal) for function constrain_G:
          r
[inout] Inputs for function constrain_G:
          G
[inout] Out (internal) for function pointer_to_const:
          \nothing
[inout] Inputs for function pointer_to_const:
          I; J; s.i2; t[3]
[inout] Out (internal) for function modify_I:
          J
[inout] Inputs for function modify_I:
          I; J; v; s.i2; t[2..3]
[inout] Out (internal) for function modify_J:
          J
[inout] Inputs for function modify_J:
          I; J; v; s.i2; t[2..3]
[inout] Out (internal) for function modify_s:
          J
[inout] Inputs for function modify_s:
          I; J; v; s; t[2..3]
[inout] Out (internal) for function modify_t:
          J
[inout] Inputs for function modify_t:
          I; J; v; s.i2; t{[2..3]; [5]}
[inout] Out (internal) for function pointer_to_const_logic:
          \nothing
[inout] Inputs for function pointer_to_const_logic:
          v
[inout] Out (internal) for function main:
          J
[inout] Inputs for function main:
          G; I; J; v; s; t{[2..3]; [5]}