logic.res.oracle

[kernel] Parsing logic.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  t[0..9] ∈ {0}
  u[0..10] ∈ {0}
  s1 ∈ {0}
  s2 ∈ {0}
  s3[0..9] ∈ {0}
  x ∈ {0}
  v ∈ [--..--]
  t_T ∈ {0}
  arr_ptr[0..2] ∈ {0}
  arr_ptr_arr[0..5] ∈ {0}
[eva] computing for function eq_tsets <- main.
  Called from logic.c:542.
[eva] logic.c:103: 
  cannot evaluate ACSL term, unsupported ACSL construct: == operation on non-supported type set<_#8>
[eva:alarm] logic.c:103: Warning: assertion got status unknown.
[eva] logic.c:105: assertion got status valid.
[eva:alarm] logic.c:106: Warning: assertion got status unknown.
[eva:alarm] logic.c:107: Warning: assertion got status unknown.
[eva:alarm] logic.c:108: Warning: assertion got status unknown.
[eva:alarm] logic.c:109: Warning: assertion got status unknown.
[eva] logic.c:110: assertion got status valid.
[eva:alarm] logic.c:111: Warning: assertion got status unknown.
[eva:alarm] logic.c:112: Warning: assertion got status unknown.
[eva] logic.c:113: assertion got status valid.
[eva] logic.c:115: assertion got status valid.
[eva] logic.c:117: assertion got status valid.
[eva] logic.c:119: assertion got status valid.
[eva:alarm] logic.c:120: Warning: assertion got status unknown.
[eva] logic.c:121: assertion got status valid.
[eva:alarm] logic.c:122: Warning: assertion got status unknown.
[eva:alarm] logic.c:125: Warning: assertion got status unknown.
[eva:alarm] logic.c:126: Warning: assertion got status unknown.
[eva:alarm] logic.c:127: Warning: assertion got status unknown.
[eva] logic.c:128: assertion got status valid.
[eva] logic.c:130: assertion got status valid.
[eva:alarm] logic.c:131: Warning: assertion got status unknown.
[eva:alarm] logic.c:132: Warning: assertion got status unknown.
[eva] logic.c:134: 
  cannot evaluate ACSL term, unsupported ACSL construct: == operation on non-supported type struct ts
[eva:alarm] logic.c:134: Warning: assertion got status unknown.
[eva] logic.c:135: 
  cannot evaluate ACSL term, unsupported ACSL construct: != operation on non-supported type int [10]
[eva:alarm] logic.c:135: Warning: assertion got status unknown.
[eva] logic.c:137: assertion got status valid.
[eva] logic.c:138: assertion got status valid.
[eva] logic.c:139: assertion got status valid.
[eva] logic.c:141: assertion got status valid.
[eva] logic.c:143: 
  cannot evaluate ACSL term, unsupported ACSL construct: set intersection
[eva:alarm] logic.c:143: Warning: assertion got status unknown.
[eva] Recording results for eq_tsets
[eva] Done for function eq_tsets
[eva] computing for function eq_char <- main.
  Called from logic.c:543.
[eva] logic.c:149: Frama_C_show_each: {-126}
[eva] logic.c:150: assertion got status valid.
[eva] logic.c:151: assertion got status valid.
[eva] Recording results for eq_char
[eva] Done for function eq_char
[eva] computing for function casts <- main.
  Called from logic.c:544.
[eva] logic.c:155: assertion got status valid.
[eva] logic.c:156: assertion got status valid.
[eva] Recording results for casts
[eva] Done for function casts
[eva] computing for function empty_tset <- main.
  Called from logic.c:545.
[eva] computing for function f_empty_tset <- empty_tset <- main.
  Called from logic.c:166.
[eva] using specification for function f_empty_tset
[eva] logic.c:166: function f_empty_tset: precondition 'r1' got status valid.
[eva] logic.c:166: function f_empty_tset: precondition 'r2' got status valid.
[eva] Done for function f_empty_tset
[eva] logic.c:167: assertion got status valid.
[eva] Recording results for empty_tset
[eva] Done for function empty_tset
[eva] computing for function reduce_by_equal <- main.
  Called from logic.c:546.
[eva:alarm] logic.c:172: Warning: accessing out of bounds index. assert 0 ≤ v;
[eva:alarm] logic.c:172: Warning: accessing out of bounds index. assert v < 10;
[eva:alarm] logic.c:173: Warning: assertion got status unknown.
[eva:alarm] logic.c:174: Warning: assertion got status unknown.
[eva] Recording results for reduce_by_equal
[eva] Done for function reduce_by_equal
[eva] computing for function alarms <- main.
  Called from logic.c:547.
[eva:alarm] logic.c:182: Warning: assertion 'ASSUME' got status unknown.
[eva:alarm] logic.c:184: Warning: assertion 'UNK' got status unknown.
[eva] logic.c:185: Frama_C_show_each: {-1; 1}
[eva:alarm] logic.c:186: Warning: assertion 'UNK' got status unknown.
[eva] logic.c:187: Frama_C_show_each: {-1; 1}
[eva:alarm] logic.c:189: Warning: assertion 'ASSUME' got status unknown.
[eva] logic.c:190: assertion 'OK' got status valid.
[eva] logic.c:191: Frama_C_show_each: {1}
[eva] logic.c:192: assertion 'OK' got status valid.
[eva] logic.c:193: Frama_C_show_each: {1}
[eva:alarm] logic.c:197: Warning: assertion 'ASSUME' got status unknown.
[eva:alarm] logic.c:198: Warning: assertion 'UNK' got status unknown.
[eva] logic.c:199: Frama_C_show_each: {0; 1}
[eva:alarm] logic.c:200: Warning: assertion 'UNK' got status unknown.
[eva] logic.c:201: Frama_C_show_each: {0; 1}
[eva:alarm] logic.c:203: Warning: assertion 'ASSUME' got status unknown.
[eva] logic.c:204: assertion 'OK' got status valid.
[eva] logic.c:205: Frama_C_show_each: {1}
[eva] logic.c:206: assertion 'OK' got status valid.
[eva] logic.c:207: Frama_C_show_each: {1}
[eva] Recording results for alarms
[eva] Done for function alarms
[eva] computing for function cond_in_lval <- main.
  Called from logic.c:548.
[eva] computing for function select_like <- cond_in_lval <- main.
  Called from logic.c:228.
[eva] using specification for function select_like
[eva] Done for function select_like
[eva] logic.c:229: assertion got status valid.
[eva] computing for function select_like <- cond_in_lval <- main.
  Called from logic.c:230.
[eva] Done for function select_like
[eva] logic.c:231: assertion got status valid.
[eva] logic.c:232: assertion got status valid.
[eva] logic.c:233: assertion got status valid.
[eva] computing for function select_like <- cond_in_lval <- main.
  Called from logic.c:234.
[eva] Done for function select_like
[eva] logic.c:235: assertion got status valid.
[eva] logic.c:236: assertion got status valid.
[eva] computing for function select_like <- cond_in_lval <- main.
  Called from logic.c:239.
[eva] Done for function select_like
[eva] logic.c:240: assertion got status valid.
[eva] logic.c:241: assertion got status valid.
[eva] logic.c:243: assertion got status valid.
[eva] logic.c:245: assertion got status valid.
[eva:alarm] logic.c:246: Warning: assertion got status unknown.
[eva] Recording results for cond_in_lval
[eva] Done for function cond_in_lval
[eva] computing for function pred <- main.
  Called from logic.c:549.
[eva] logic.c:90: assertion got status valid.
[eva] logic.c:91: assertion got status valid.
[eva] logic.c:31: cannot evaluate ACSL term, \at() on a C label is unsupported
[eva:alarm] logic.c:92: Warning: assertion got status unknown.
[eva] logic.c:92: cannot evaluate ACSL term, \at() on a C label is unsupported
[eva] logic.c:93: assertion got status valid.
[eva] computing for function f <- pred <- main.
  Called from logic.c:94.
[eva] logic.c:46: assertion got status valid.
[eva] logic.c:47: assertion got status valid.
[eva] Recording results for f
[eva] Done for function f
[eva] computing for function g <- pred <- main.
  Called from logic.c:95.
[eva] logic.c:55: assertion got status valid.
[eva] logic.c:56: assertion got status valid.
[eva] logic.c:57: assertion got status valid.
[eva] logic.c:35: cannot evaluate ACSL term, \at() on a C label is unsupported
[eva:alarm] logic.c:58: Warning: assertion got status unknown.
[eva] logic.c:58: cannot evaluate ACSL term, \at() on a C label is unsupported
[eva] Recording results for g
[eva] Done for function g
[eva] computing for function unsup <- pred <- main.
  Called from logic.c:96.
[eva:alarm] logic.c:81: Warning: assertion got status unknown.
[eva] Recording results for unsup
[eva] Done for function unsup
[eva] computing for function h <- pred <- main.
  Called from logic.c:97.
[eva] logic.c:69: 
  cannot evaluate ACSL term, unsupported ACSL construct: logic function h_acsl
[eva:alarm] logic.c:69: Warning: assertion got status unknown.
[eva:alarm] logic.c:70: Warning: assertion got status unknown.
[eva] logic.c:71: assertion got status valid.
[eva:alarm] logic.c:72: Warning: 
  assertion got status invalid (stopping propagation).
[eva] logic.c:73: assertion got status valid.
[eva] logic.c:75: assertion got status valid.
[eva] logic.c:76: assertion got status valid.
[eva] Recording results for h
[eva] Done for function h
[eva] Recording results for pred
[eva] Done for function pred
[eva] computing for function float_sign <- main.
  Called from logic.c:550.
[eva] logic.c:251: assertion got status valid.
[eva] logic.c:252: assertion got status valid.
[eva] logic.c:253: assertion got status valid.
[eva] logic.c:254: assertion got status valid.
[eva:alarm] logic.c:256: Warning: assertion got status unknown.
[eva] Recording results for float_sign
[eva] Done for function float_sign
[eva] computing for function min_max <- main.
  Called from logic.c:551.
[eva] computing for function Frama_C_interval <- min_max <- main.
  Called from logic.c:274.
[eva] using specification for function Frama_C_interval
[eva] logic.c:274: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- min_max <- main.
  Called from logic.c:275.
[eva] logic.c:275: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- min_max <- main.
  Called from logic.c:276.
[eva] logic.c:276: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva:alarm] logic.c:281: Warning: assertion got status unknown.
[eva:alarm] logic.c:282: Warning: assertion got status unknown.
[eva:alarm] logic.c:283: Warning: assertion got status unknown.
[eva:alarm] logic.c:284: Warning: assertion got status unknown.
[eva:alarm] logic.c:288: Warning: assertion got status unknown.
[eva] Recording results for min_max
[eva] Done for function min_max
[eva] computing for function assign_tsets <- main.
  Called from logic.c:552.
[eva] computing for function assign_tsets_aux <- assign_tsets <- main.
  Called from logic.c:269.
[eva] using specification for function assign_tsets_aux
[eva] Done for function assign_tsets_aux
[eva] Recording results for assign_tsets
[eva] Done for function assign_tsets
[eva] computing for function check_and_assert <- main.
  Called from logic.c:553.
[eva:alarm] logic.c:295: Warning: assertion got status unknown.
[eva] logic.c:296: Frama_C_show_each_42: {42}
[eva] logic.c:297: check got status valid.
[eva:alarm] logic.c:299: Warning: check got status unknown.
[eva] logic.c:300: Frama_C_show_each_imprecise: [-2147483648..2147483647]
[eva:alarm] logic.c:301: Warning: assertion got status unknown.
[eva:alarm] logic.c:303: Warning: 
  assertion got status invalid (stopping propagation).
[eva:alarm] logic.c:306: Warning: check got status invalid.
[eva] logic.c:307: Frama_C_show_each_reachable: {42}
[eva] Recording results for check_and_assert
[eva] Done for function check_and_assert
[eva] computing for function min_max_quantifier <- main.
  Called from logic.c:554.
[eva] logic.c:321: check 'valid' got status valid.
[eva] logic.c:322: check 'valid' got status valid.
[eva] logic.c:323: check 'valid' got status valid.
[eva] logic.c:324: check 'valid' got status valid.
[eva] logic.c:325: check 'valid' got status valid.
[eva] logic.c:326: check 'valid' got status valid.
[eva:alarm] logic.c:327: Warning: check 'valid' got status unknown.
[eva:alarm] logic.c:328: Warning: check 'valid' got status unknown.
[eva:alarm] logic.c:329: Warning: check 'unknown' got status unknown.
[eva:alarm] logic.c:330: Warning: check 'unknown' got status unknown.
[eva] computing for function Frama_C_interval <- min_max_quantifier <- main.
  Called from logic.c:331.
[eva] logic.c:331: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- min_max_quantifier <- main.
  Called from logic.c:332.
[eva] logic.c:332: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] logic.c:333: check 'valid' got status valid.
[eva] logic.c:334: check 'valid' got status valid.
[eva] logic.c:335: check 'valid' got status valid.
[eva] logic.c:336: check 'valid' got status valid.
[eva:alarm] logic.c:337: Warning: check 'unknown' got status unknown.
[eva:alarm] logic.c:338: Warning: check 'unknown' got status unknown.
[eva:alarm] logic.c:339: Warning: check 'unknown' got status unknown.
[eva:alarm] logic.c:340: Warning: check 'unknown' got status unknown.
[eva] computing for function Frama_C_interval <- min_max_quantifier <- main.
  Called from logic.c:341.
[eva] logic.c:341: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- min_max_quantifier <- main.
  Called from logic.c:342.
[eva] logic.c:342: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] logic.c:343: check 'valid' got status valid.
[eva] logic.c:344: check 'valid' got status valid.
[eva] logic.c:345: check 'valid' got status valid.
[eva] logic.c:346: check 'valid' got status valid.
[eva:alarm] logic.c:347: Warning: check 'unknown' got status unknown.
[eva:alarm] logic.c:348: Warning: check 'unknown' got status unknown.
[eva:alarm] logic.c:349: Warning: check 'unknown' got status unknown.
[eva:alarm] logic.c:350: Warning: check 'unknown' got status unknown.
[eva] computing for function Frama_C_interval <- min_max_quantifier <- main.
  Called from logic.c:351.
[eva] logic.c:351: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- min_max_quantifier <- main.
  Called from logic.c:352.
[eva] logic.c:352: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva:alarm] logic.c:353: Warning: check 'unknown' got status unknown.
[eva:alarm] logic.c:354: Warning: check 'unknown' got status unknown.
[eva] Recording results for min_max_quantifier
[eva] Done for function min_max_quantifier
[eva] computing for function int_abs <- main.
  Called from logic.c:555.
[eva] computing for function abs <- int_abs <- main.
  Called from logic.c:365.
[eva] using specification for function abs
[eva] Done for function abs
[eva] computing for function abs <- int_abs <- main.
  Called from logic.c:366.
[eva] Done for function abs
[eva] computing for function abs <- int_abs <- main.
  Called from logic.c:367.
[eva] Done for function abs
[eva] computing for function Frama_C_interval <- int_abs <- main.
  Called from logic.c:370.
[eva] logic.c:370: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function abs <- int_abs <- main.
  Called from logic.c:371.
[eva] Done for function abs
[eva] logic.c:372: Frama_C_show_each_5_10: {5; 6; 7; 8; 9; 10}
[eva] computing for function Frama_C_interval <- int_abs <- main.
  Called from logic.c:373.
[eva] logic.c:373: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function abs <- int_abs <- main.
  Called from logic.c:374.
[eva] Done for function abs
[eva] logic.c:375: Frama_C_show_each_0_4: {0; 1; 2; 3; 4}
[eva] computing for function Frama_C_interval <- int_abs <- main.
  Called from logic.c:377.
[eva] logic.c:377: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function abs <- int_abs <- main.
  Called from logic.c:378.
[eva] Done for function abs
[eva] logic.c:379: Frama_C_show_each_10_100: [10..100]
[eva] computing for function Frama_C_interval <- int_abs <- main.
  Called from logic.c:380.
[eva] logic.c:380: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function abs <- int_abs <- main.
  Called from logic.c:381.
[eva] Done for function abs
[eva] logic.c:382: Frama_C_show_each_0_100: [0..100]
[eva] computing for function Frama_C_interval <- int_abs <- main.
  Called from logic.c:383.
[eva] logic.c:383: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function abs <- int_abs <- main.
  Called from logic.c:384.
[eva] Done for function abs
[eva] logic.c:385: Frama_C_show_each_10_20: [10..20]
[eva] computing for function Frama_C_interval <- int_abs <- main.
  Called from logic.c:386.
[eva] logic.c:386: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function abs <- int_abs <- main.
  Called from logic.c:387.
[eva] Done for function abs
[eva] logic.c:388: Frama_C_show_each_0_12: [0..12]
[eva] computing for function Frama_C_interval <- int_abs <- main.
  Called from logic.c:389.
[eva] logic.c:389: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function abs <- int_abs <- main.
  Called from logic.c:390.
[eva] Done for function abs
[eva] logic.c:391: Frama_C_show_each_0_16: [0..16]
[eva] computing for function Frama_C_interval <- int_abs <- main.
  Called from logic.c:393.
[eva] logic.c:393: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function abs <- int_abs <- main.
  Called from logic.c:395.
[eva] Done for function abs
[eva] logic.c:396: Frama_C_show_each_2_mod_4: [2..82],2%4
[eva] computing for function Frama_C_interval <- int_abs <- main.
  Called from logic.c:397.
[eva] logic.c:397: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function abs <- int_abs <- main.
  Called from logic.c:399.
[eva] Done for function abs
[eva] logic.c:400: Frama_C_show_each_1_mod_2: [1..83],1%2
[eva] computing for function Frama_C_interval <- int_abs <- main.
  Called from logic.c:401.
[eva] logic.c:401: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function abs <- int_abs <- main.
  Called from logic.c:403.
[eva] Done for function abs
[eva] logic.c:404: Frama_C_show_each_no_mod: [0..35]
[eva] computing for function Frama_C_interval <- int_abs <- main.
  Called from logic.c:406.
[eva] logic.c:406: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function abs <- int_abs <- main.
  Called from logic.c:407.
[eva] Done for function abs
[eva] logic.c:408: Frama_C_show_each_set: {0; 1; 2; 3; 4; 5}
[eva] computing for function abs <- int_abs <- main.
  Called from logic.c:411.
[eva:garbled-mix:assigns] logic.c:411: 
  The specification of function abs has generated a garbled mix of addresses
  for assigns clause \result.
[eva] Done for function abs
[eva] logic.c:412: 
  Frama_C_show_each_gm:
  {{ garbled mix of &{x_0} (origin: Library function {logic.c:411}) }}
[eva] Recording results for int_abs
[eva] Done for function int_abs
[eva] computing for function float_abs <- main.
  Called from logic.c:556.
[eva] computing for function fabs <- float_abs <- main.
  Called from logic.c:421.
[eva] using specification for function fabs
[eva] Done for function fabs
[eva] computing for function fabs <- float_abs <- main.
  Called from logic.c:422.
[eva] Done for function fabs
[eva] computing for function fabs <- float_abs <- main.
  Called from logic.c:423.
[eva] Done for function fabs
[eva] computing for function Frama_C_double_interval <- float_abs <- main.
  Called from logic.c:426.
[eva] using specification for function Frama_C_double_interval
[eva] logic.c:426: 
  function Frama_C_double_interval: precondition 'finite' got status valid.
[eva] logic.c:426: 
  function Frama_C_double_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_double_interval
[eva] computing for function fabs <- float_abs <- main.
  Called from logic.c:427.
[eva] Done for function fabs
[eva] logic.c:428: Frama_C_show_each_zero: [-0. .. 0.]
[eva] computing for function Frama_C_double_interval <- float_abs <- main.
  Called from logic.c:429.
[eva] logic.c:429: 
  function Frama_C_double_interval: precondition 'finite' got status valid.
[eva] logic.c:429: 
  function Frama_C_double_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_double_interval
[eva] computing for function fabs <- float_abs <- main.
  Called from logic.c:430.
[eva] Done for function fabs
[eva] logic.c:431: Frama_C_show_each_half_two: [0.5 .. 2.]
[eva] computing for function Frama_C_double_interval <- float_abs <- main.
  Called from logic.c:432.
[eva] logic.c:432: 
  function Frama_C_double_interval: precondition 'finite' got status valid.
[eva] logic.c:432: 
  function Frama_C_double_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_double_interval
[eva] computing for function fabs <- float_abs <- main.
  Called from logic.c:433.
[eva] Done for function fabs
[eva] logic.c:434: Frama_C_show_each_0_10: [-0. .. 10.]
[eva] computing for function Frama_C_double_interval <- float_abs <- main.
  Called from logic.c:435.
[eva] logic.c:435: 
  function Frama_C_double_interval: precondition 'finite' got status valid.
[eva] logic.c:435: 
  function Frama_C_double_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_double_interval
[eva] computing for function fabs <- float_abs <- main.
  Called from logic.c:436.
[eva] Done for function fabs
[eva] logic.c:437: Frama_C_show_each_0_3: [-0. .. 3.]
[eva] Recording results for float_abs
[eva] Done for function float_abs
[eva] computing for function set_comprehension <- main.
  Called from logic.c:557.
[eva:alarm] logic.c:444: Warning: assertion got status unknown.
[eva] logic.c:445: Frama_C_show_each_10_100: [10..100]
[eva:alarm] logic.c:448: Warning: assertion got status unknown.
[eva] logic.c:449: Frama_C_show_each_10_100: [10..100]
[eva:alarm] logic.c:452: Warning: assertion got status unknown.
[eva] logic.c:453: Frama_C_show_each_31_301: [31..301],1%3
[eva:alarm] logic.c:456: Warning: assertion got status unknown.
[eva] logic.c:457: Frama_C_show_each_5_50: [-2147483648..2147483647]
[eva:alarm] logic.c:460: Warning: assertion got status unknown.
[eva] logic.c:461: Frama_C_show_each_0: [-90..90]
[eva:alarm] logic.c:464: Warning: assertion got status unknown.
[eva] logic.c:465: Frama_C_show_each_bottom: [-2147483648..2147483647]
[eva] computing for function Frama_C_interval <- set_comprehension <- main.
  Called from logic.c:467.
[eva] logic.c:467: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- set_comprehension <- main.
  Called from logic.c:468.
[eva] logic.c:468: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva:alarm] logic.c:470: Warning: assertion got status unknown.
[eva] logic.c:471: Frama_C_show_each_12_32: [12..32]
[eva:alarm] logic.c:474: Warning: assertion got status unknown.
[eva] logic.c:475: Frama_C_show_each_16_24: [16..24]
[eva:alarm] logic.c:478: Warning: assertion got status unknown.
[eva] logic.c:479: Frama_C_show_each_24_68: [24..68]
[eva:alarm] logic.c:483: Warning: assertion got status unknown.
[eva] logic.c:484: Frama_C_show_each_5_41: [5..41],1%2
[eva:alarm] logic.c:487: Warning: assertion got status unknown.
[eva] logic.c:488: Frama_C_show_each: [-2147483648..2147483647]
[eva] Recording results for set_comprehension
[eva] Done for function set_comprehension
[eva] computing for function set_comprehension_assigns <- main.
  Called from logic.c:558.
[eva] computing for function multi_memset <- set_comprehension_assigns <- main.
  Called from logic.c:503.
[eva] using specification for function multi_memset
[eva] Done for function multi_memset
[eva] Recording results for set_comprehension_assigns
[eva] Done for function set_comprehension_assigns
[eva] computing for function plet <- main.
  Called from logic.c:559.
[eva] computing for function Frama_C_interval <- plet <- main.
  Called from logic.c:508.
[eva] logic.c:508: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- plet <- main.
  Called from logic.c:509.
[eva] logic.c:509: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- plet <- main.
  Called from logic.c:510.
[eva] logic.c:510: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva:alarm] logic.c:512: Warning: assertion 'unknown' got status unknown.
[eva] logic.c:513: Frama_C_show_each_0_24: [0..24]
[eva] logic.c:516: assertion 'true' got status valid.
[eva] logic.c:517: Frama_C_show_each_0_120: [0..120]
[eva:alarm] logic.c:520: Warning: 
  assertion 'false' got status invalid (stopping propagation).
[eva] logic.c:525: assertion 'true' got status valid.
[eva:alarm] logic.c:526: Warning: assertion 'unknown' got status unknown.
[eva] logic.c:530: assertion 'valid' got status valid.
[eva:alarm] logic.c:531: Warning: assertion 'unknown' got status unknown.
[eva:alarm] logic.c:533: Warning: 
  assertion 'invalid' got status invalid (stopping propagation).
[eva] logic.c:538: 
  cannot evaluate ACSL term, unsupported ACSL construct: \let binding
[eva:alarm] logic.c:538: Warning: assertion 'unsupported' got status unknown.
[eva] Recording results for plet
[eva] Done for function plet
[eva] Recording results for main
[eva] Done for function main
[eva:garbled-mix:summary] 
  Origins of garbled mix generated during analysis:
    logic.c:411: assigns clause on addresses
      (read in 1 statement, propagated through 1 statement)
      garbled mix of &{x_0}
[eva] logic.c:530: 
  Cannot evaluate range bound __fc_len - 1
  (unsupported logic var __fc_len). Approximating
[eva] logic.c:533: 
  Cannot evaluate range bound __fc_len
  (unsupported logic var __fc_len). Approximating
[scope:rm_asserts] removing 5 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function alarms:
  x_0 ∈ {1}
[eva:final-states] Values at end of function assign_tsets:
  arr_ptr[0] ∈ {{ &arr_ptr_arr[1] }}
         [1] ∈ {{ &arr_ptr_arr[4] }}
         [2] ∈ {{ &arr_ptr_arr[5] }}
  arr_ptr_arr[0] ∈ {0}
             [1] ∈ [--..--]
             [2..3] ∈ {0}
             [4..5] ∈ [--..--]
[eva:final-states] Values at end of function casts:
  
[eva:final-states] Values at end of function check_and_assert:
  x_0 ∈ {42}
[eva:final-states] Values at end of function eq_char:
  c ∈ {-126}
[eva:final-states] Values at end of function eq_tsets:
  
[eva:final-states] Values at end of function f:
  temp_1 ∈ {0}
  temp_2 ∈ {0}
[eva:final-states] Values at end of function empty_tset:
  T[0] ∈ {2}
[eva:final-states] Values at end of function float_abs:
  Frama_C_entropy_source ∈ [--..--]
  zero ∈ [-0. .. 0.]
  ten ∈ {10.}
  eleven ∈ {11.}
  x_0 ∈ [-0. .. 3.]
[eva:final-states] Values at end of function float_sign:
  d ∈ [-0. .. 0.]
[eva:final-states] Values at end of function g:
  x_0 ∈ {0}
  y ∈ {1}
[eva:final-states] Values at end of function h:
  s1.f1 ∈ {1}
    .f2 ∈ {0}
  x_0 ∈ {0}
  y ∈ {0}
  k ∈ {5}
  j ∈ {6}
  p ∈ {{ &k }}
  q ∈ {{ &j }}
[eva:final-states] Values at end of function int_abs:
  Frama_C_entropy_source ∈ [--..--]
  zero ∈ {0}
  ten ∈ {10}
  eleven ∈ {11}
  x_0 ∈
     {{ garbled mix of &{x_0} (origin: Library function {logic.c:411}) }}
[eva:final-states] Values at end of function min_max:
  Frama_C_entropy_source ∈ [--..--]
  x_0 ∈ [3..17]
  y ∈ {1; 2; 3; 4; 5}
  z ∈ [1..100]
  r1 ∈ [3..17]
  r2 ∈ [3..100]
  r3 ∈ {1; 2; 3; 4; 5}
  r4 ∈ [1..17]
  a ∈ {0}
  b ∈ {-0.}
  d ∈ [-0. .. 0.]
[eva:final-states] Values at end of function min_max_quantifier:
  Frama_C_entropy_source ∈ [--..--]
  i ∈ [4..16]
  j ∈ [12..24]
  t_0[0] ∈ {0}
     [1] ∈ {1}
     [2] ∈ {2}
     [3] ∈ {3}
     [4] ∈ {4}
     [5] ∈ {5}
     [6] ∈ {6}
     [7] ∈ {7}
     [8] ∈ {8}
     [9] ∈ {9}
     [10] ∈ {10}
     [11] ∈ {11}
     [12] ∈ {12}
     [13] ∈ {13}
     [14] ∈ {14}
     [15] ∈ {15}
     [16] ∈ {16}
     [17] ∈ {17}
     [18] ∈ {18}
     [19] ∈ {19}
     [20] ∈ {20}
     [21] ∈ {21}
     [22] ∈ {22}
     [23] ∈ {23}
     [24] ∈ {24}
     [25] ∈ {25}
     [26] ∈ {26}
     [27] ∈ {27}
     [28] ∈ {28}
     [29] ∈ {29}
     [30] ∈ {30}
     [31] ∈ {31}
     [32] ∈ {0}
     [33] ∈ {31}
     [34] ∈ {30}
     [35] ∈ {29}
     [36] ∈ {28}
     [37] ∈ {27}
     [38] ∈ {26}
     [39] ∈ {25}
     [40] ∈ {24}
     [41] ∈ {23}
     [42] ∈ {22}
     [43] ∈ {21}
     [44] ∈ {20}
     [45] ∈ {19}
     [46] ∈ {18}
     [47] ∈ {17}
     [48] ∈ {16}
     [49] ∈ {15}
     [50] ∈ {14}
     [51] ∈ {13}
     [52] ∈ {12}
     [53] ∈ {11}
     [54] ∈ {10}
     [55] ∈ {9}
     [56] ∈ {8}
     [57] ∈ {7}
     [58] ∈ {6}
     [59] ∈ {5}
     [60] ∈ {4}
     [61] ∈ {3}
     [62] ∈ {2}
     [63] ∈ {1}
[eva:final-states] Values at end of function plet:
  Frama_C_entropy_source ∈ [--..--]
  x_0 ∈ [0..120]
  y ∈ [0..10]
  z ∈ [10..30]
[eva:final-states] Values at end of function reduce_by_equal:
  a[0..8] ∈ {1}
   [9] ∈ [--..--]
[eva:final-states] Values at end of function cond_in_lval:
  a ∈ {4}
  out ∈ {40}
  b.i1 ∈ {6}
   .i2 ∈ {8}
  x_0 ∈ [-2147483648..0]
[eva:final-states] Values at end of function set_comprehension:
  Frama_C_entropy_source ∈ [--..--]
  x_0 ∈ [--..--]
  a ∈ [12..24]
  b ∈ [16..32]
  t_0[0] ∈ {2}
     [1] ∈ {3}
     [2] ∈ {5}
     [3] ∈ {7}
     [4] ∈ {11}
     [5] ∈ {13}
     [6] ∈ {17}
     [7] ∈ {19}
     [8] ∈ {23}
     [9] ∈ {29}
     [10] ∈ {31}
     [11] ∈ {37}
     [12] ∈ {41}
     [13] ∈ {43}
     [14] ∈ {47}
[eva:final-states] Values at end of function set_comprehension_assigns:
  buf0[0..9] ∈ {0}
  buf1[0..9] ∈ [--..--]
      [10..11] ∈ {0}
  buf2[0..7] ∈ [--..--]
  buf3[0..9] ∈ {0}
  p[0] ∈ {{ &buf0[0] }}
   [1] ∈ {{ &buf1[0] }}
   [2] ∈ {{ &buf2[0] }}
   [3] ∈ {{ &buf3[0] }}
[eva:final-states] Values at end of function unsup:
  t_T{.z; .t} ∈ {21}
[eva:final-states] Values at end of function pred:
  s1.f1 ∈ {1}
    .f2 ∈ {0}
  t_T{.z; .t} ∈ {21}
  x_0 ∈ {10}
  y ∈ {11}
[eva:final-states] Values at end of function main:
  Frama_C_entropy_source ∈ [--..--]
  s1.f1 ∈ {1}
    .f2 ∈ {0}
  t_T{.z; .t} ∈ {21}
  arr_ptr[0] ∈ {{ &arr_ptr_arr[1] }}
         [1] ∈ {{ &arr_ptr_arr[4] }}
         [2] ∈ {{ &arr_ptr_arr[5] }}
  arr_ptr_arr[0] ∈ {0}
             [1] ∈ [--..--]
             [2..3] ∈ {0}
             [4..5] ∈ [--..--]
[from] Computing for function alarms
[from] Done for function alarms
[from] Computing for function assign_tsets
[from] Computing for function assign_tsets_aux <-assign_tsets
[from] Done for function assign_tsets_aux
[from] Done for function assign_tsets
[from] Computing for function casts
[from] Done for function casts
[from] Computing for function check_and_assert
[from] Done for function check_and_assert
[from] Computing for function eq_char
[from] Done for function eq_char
[from] Computing for function eq_tsets
[from] Done for function eq_tsets
[from] Computing for function f
[from] Done for function f
[from] Computing for function empty_tset
[from] Computing for function f_empty_tset <-empty_tset
[from] Done for function f_empty_tset
[from] Done for function empty_tset
[from] Computing for function float_abs
[from] Computing for function fabs <-float_abs
[from] Done for function fabs
[from] Computing for function Frama_C_double_interval <-float_abs
[from] Done for function Frama_C_double_interval
[from] Done for function float_abs
[from] Computing for function float_sign
[from] Done for function float_sign
[from] Computing for function g
[from] Done for function g
[from] Computing for function h
[from] Done for function h
[from] Computing for function int_abs
[from] Computing for function abs <-int_abs
[from] Done for function abs
[from] Computing for function Frama_C_interval <-int_abs
[from] Done for function Frama_C_interval
[from] Done for function int_abs
[from] Computing for function min_max
[from] Done for function min_max
[from] Computing for function min_max_quantifier
[from] Done for function min_max_quantifier
[from] Computing for function plet
[from] Done for function plet
[from] Computing for function reduce_by_equal
[from] Done for function reduce_by_equal
[from] Computing for function cond_in_lval
[from] Computing for function select_like <-cond_in_lval
[from] Done for function select_like
[from] Done for function cond_in_lval
[from] Computing for function set_comprehension
[from] Done for function set_comprehension
[from] Computing for function set_comprehension_assigns
[from] Computing for function multi_memset <-set_comprehension_assigns
[from] Done for function multi_memset
[from] Done for function set_comprehension_assigns
[from] Computing for function unsup
[from] Done for function unsup
[from] Computing for function pred
[from] Done for function pred
[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 Frama_C_double_interval:
  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
  \result FROM Frama_C_entropy_source; min; max
[from] Function Frama_C_interval:
  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
  \result FROM Frama_C_entropy_source; min; max
[from] Function abs:
  \result FROM x
[from] Function alarms:
  NO EFFECTS
[from] Function assign_tsets_aux:
  arr_ptr_arr{[1]; [4..5]} FROM \nothing
[from] Function assign_tsets:
  arr_ptr[0..2] FROM \nothing
  arr_ptr_arr{[1]; [4..5]} FROM \nothing
[from] Function casts:
  NO EFFECTS
[from] Function check_and_assert:
  NO EFFECTS
[from] Function eq_char:
  NO EFFECTS
[from] Function eq_tsets:
  NO EFFECTS
[from] Function f:
  NO EFFECTS
[from] Function f_empty_tset:
  NO EFFECTS
[from] Function empty_tset:
  NO EFFECTS
[from] Function fabs:
  \result FROM f
[from] Function float_abs:
  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function float_sign:
  NO EFFECTS
[from] Function g:
  NO EFFECTS
[from] Function h:
  s1.f1 FROM \nothing
[from] Function int_abs:
  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function min_max:
  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function min_max_quantifier:
  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function multi_memset:
  buf1[0..9] FROM \nothing (and SELF)
  buf2[0..7] FROM \nothing (and SELF)
[from] Function plet:
  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function reduce_by_equal:
  NO EFFECTS
[from] Function select_like:
  a FROM p; q; a; b (and SELF)
  out FROM p; q; a; b
  b FROM p; q; a; b (and SELF)
[from] Function cond_in_lval:
  NO EFFECTS
[from] Function set_comprehension:
  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function set_comprehension_assigns:
  NO EFFECTS
[from] Function unsup:
  t_T FROM \nothing
[from] Function pred:
  s1.f1 FROM \nothing
  t_T FROM \nothing
[from] Function main:
  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
  s1.f1 FROM \nothing
  t_T FROM \nothing
  arr_ptr[0..2] FROM \nothing
  arr_ptr_arr{[1]; [4..5]} FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function alarms:
    x_0
[inout] Inputs for function alarms:
    v
[inout] Out (internal) for function assign_tsets:
    arr_ptr[0..2]; arr_ptr_arr{[1]; [4..5]}
[inout] Inputs for function assign_tsets:
    \nothing
[inout] Out (internal) for function casts:
    \nothing
[inout] Inputs for function casts:
    \nothing
[inout] Out (internal) for function check_and_assert:
    x_0
[inout] Inputs for function check_and_assert:
    v
[inout] Out (internal) for function eq_char:
    c
[inout] Inputs for function eq_char:
    \nothing
[inout] Out (internal) for function eq_tsets:
    \nothing
[inout] Inputs for function eq_tsets:
    \nothing
[inout] Out (internal) for function f:
    temp_1; temp_2
[inout] Inputs for function f:
    \nothing
[inout] Out (internal) for function empty_tset:
    T[0]
[inout] Inputs for function empty_tset:
    \nothing
[inout] Out (internal) for function float_abs:
    Frama_C_entropy_source; zero; ten; eleven; x_0
[inout] Inputs for function float_abs:
    Frama_C_entropy_source
[inout] Out (internal) for function float_sign:
    d; tmp
[inout] Inputs for function float_sign:
    v
[inout] Out (internal) for function g:
    x_0; y
[inout] Inputs for function g:
    \nothing
[inout] Out (internal) for function h:
    s1.f1; x_0; y; k; j; p; q
[inout] Inputs for function h:
    v
[inout] Out (internal) for function int_abs:
    Frama_C_entropy_source; zero; ten; eleven; x_0
[inout] Inputs for function int_abs:
    Frama_C_entropy_source
[inout] Out (internal) for function min_max:
    Frama_C_entropy_source; x_0; y; z; r1; r2; r3; r4; a; b; d
[inout] Inputs for function min_max:
    Frama_C_entropy_source; v
[inout] Out (internal) for function min_max_quantifier:
    Frama_C_entropy_source; i; j; t_0[0..63]
[inout] Inputs for function min_max_quantifier:
    Frama_C_entropy_source
[inout] Out (internal) for function plet:
    Frama_C_entropy_source; x_0; y; z
[inout] Inputs for function plet:
    Frama_C_entropy_source; v
[inout] Out (internal) for function reduce_by_equal:
    a[0..9]
[inout] Inputs for function reduce_by_equal:
    v
[inout] Out (internal) for function cond_in_lval:
    a; out; b; x_0
[inout] Inputs for function cond_in_lval:
    v
[inout] Out (internal) for function set_comprehension:
    Frama_C_entropy_source; x_0; a; b; t_0[0..14]
[inout] Inputs for function set_comprehension:
    Frama_C_entropy_source; v
[inout] Out (internal) for function set_comprehension_assigns:
    buf0[0..9]; buf1[0..11]; buf2[0..7]; buf3[0..9]; p[0..3]
[inout] Inputs for function set_comprehension_assigns:
    \nothing
[inout] Out (internal) for function unsup:
    t_T
[inout] Inputs for function unsup:
    \nothing
[inout] Out (internal) for function pred:
    s1.f1; t_T; x_0; y
[inout] Inputs for function pred:
    v
[inout] Out (internal) for function main:
    Frama_C_entropy_source; s1.f1; t_T; arr_ptr[0..2]; arr_ptr_arr{[1]; [4..5]}
[inout] Inputs for function main:
    Frama_C_entropy_source; v