[Eva] New test file for the octagons domain.

tests/value/diff_apron

@@ -670,6 +670,17 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_apron/modulo.res.or
 60a109,110
 > [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-10..10], [-9..9], [-8..8]
 > [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-9..9], [-8..8], [-7..7]
+diff tests/value/oracle/octagons.res.oracle tests/value/oracle_apron/octagons.res.oracle
+270,273c270,273
+<   a ∈ [-1024..2147483647]
+<   b ∈ [-1023..2147483647]
+<   c ∈ [-1023..2147483647]
+<   d ∈ [-1032..2147483647]
+---
+>   a ∈ [-603..2147483646]
+>   b ∈ [-602..2147483647]
+>   c ∈ [-602..1446]
+>   d ∈ [-611..2147483647]
 diff tests/value/oracle/offsetmap.0.res.oracle tests/value/oracle_apron/offsetmap.0.res.oracle
 62,63c62
 <   a[bits 0 to 7] ∈ {1; 6}

tests/value/diff_equalities

@@ -610,6 +610,15 @@ diff tests/value/oracle/nonlin.res.oracle tests/value/oracle_equalities/nonlin.r
 <   q ∈ {{ &x + [-400..400],0%4 }}
 ---
 >   q ∈ {{ &x }}
+diff tests/value/oracle/octagons.res.oracle tests/value/oracle_equalities/octagons.res.oracle
+29c29
+<   Frama_C_show_each_unreduced_unsigned: [0..4294967295], [0..4294967295]
+---
+>   Frama_C_show_each_unreduced_unsigned: [0..4294967295], [6..4294967295]
+255c255
+<   t ∈ [--..--] or UNINITIALIZED
+---
+>   t ∈ [6..4294967295] or UNINITIALIZED
 diff tests/value/oracle/offsetmap.0.res.oracle tests/value/oracle_equalities/offsetmap.0.res.oracle
 38d37
 < [eva] Recording results for g

tests/value/diff_gauges

@@ -889,6 +889,34 @@ diff tests/value/oracle/noreturn.res.oracle tests/value/oracle_gauges/noreturn.r
 > [eva] tests/value/noreturn.i:7: starting to merge loop iterations
 36a40
 > [eva] tests/value/noreturn.i:13: starting to merge loop iterations
+diff tests/value/oracle/octagons.res.oracle tests/value/oracle_gauges/octagons.res.oracle
+121,128d120
+< [eva:alarm] tests/value/octagons.c:107: Warning: 
+<   signed overflow. assert a + 2 ≤ 2147483647;
+< [eva:alarm] tests/value/octagons.c:108: Warning: 
+<   signed overflow. assert b + 2 ≤ 2147483647;
+< [eva:alarm] tests/value/octagons.c:110: Warning: 
+<   signed overflow. assert a + k ≤ 2147483647;
+< [eva:alarm] tests/value/octagons.c:113: Warning: 
+<   signed overflow. assert -2147483648 ≤ c - a;
+130c122
+< [eva] tests/value/octagons.c:116: Frama_C_show_each_imprecise: [-2147483648..1]
+---
+> [eva] tests/value/octagons.c:116: Frama_C_show_each_imprecise: [-2468..1]
+270,273c262,265
+<   a ∈ [-1024..2147483647]
+<   b ∈ [-1023..2147483647]
+<   c ∈ [-1023..2147483647]
+<   d ∈ [-1032..2147483647]
+---
+>   a ∈ [-182..1866]
+>   b ∈ [-181..1867]
+>   c ∈ [-602..1446]
+>   d ∈ [-190..1874]
+275c267
+<   d2 ∈ [-2147483648..1]
+---
+>   d2 ∈ [-2468..1]
 diff tests/value/oracle/reduce_formals.res.oracle tests/value/oracle_gauges/reduce_formals.res.oracle
 10a11
 > [eva] tests/value/reduce_formals.i:5: starting to merge loop iterations

tests/value/octagons.c

+/* run.config*
+   STDOPT: +" -eva-octagons-domain -eva-octagons-through-calls -eva-msg-key=d-octagons,-d-cvalue"
+*/
+
+#include <__fc_builtin.h>
+
+volatile int undet;
+
+/* Minimal example from the Eva user manual. */
+void demo () {
+  int y = undet;
+  int k = Frama_C_interval(0, 10);
+  int x = y - k;
+  int r = x + 3 - y;  // r \in [-7..3]
+  int t;
+  if (y > 15)
+    t = x;            // t \in [6..]
+}
+
+/* Same example as [demo] but with other integer types. */
+void integer_types () {
+  unsigned int k, x, y, r, t;
+  y = undet;
+  k = Frama_C_interval(0, 10);
+  x = y - k;        // No octagon inferred as [y - k] may overflow.
+  r = x + 3 - y;
+  if (y > 15)
+    t = x;
+  Frama_C_show_each_unreduced_unsigned(r, t);
+  char ck, cx, cy, cr, ct;
+  cy = undet;
+  ck = Frama_C_interval(0, 10);
+  cx = cy - ck;    // An octagon should be inferred despite the casts to int.
+  cr = cx + 3 - cy;
+  if (cy > 15)
+    ct = cx;
+  Frama_C_show_each_reduced_char(cr, ct);
+}
+
+/* A test with multiple mathematical operations to complicate the inference
+   and use of octagons. */
+void arith () {
+  int k = Frama_C_interval(0, 4);
+  int a, b, x, y, r;
+  /* 1. Infer octagons from assignments. */
+  a = Frama_C_interval(5, 25);
+  b = Frama_C_interval(-12, 12);
+  x = 1 - (a + 2*k - 4);                                  // x + a ∈ [-3..5]
+  y = 4*4 - k + (1 + b);                                  // y - b ∈ [13..17]
+  /* 1.1 Use octagons in the evaluation of expressions. */
+  r = 2 * (10 - (b - 1 - y) - (x - 2 + a));               // r ∈ [42..66]
+  Frama_C_show_each_precise(r);
+  r = 2 * (10 - (b + x - 3 - y + a));                    // r ∈ [42..66]
+  Frama_C_show_each_imprecise(r);
+  k = Frama_C_interval(0, 4);
+  /* 1.1 Use octagons to propagate variable reductions. */
+  if (12 - x < (k+1)*3) {                                 // x > -3
+    r = 10 * a;                                           // so a < 8
+    Frama_C_show_each(r);                                 // {50; 60; 70}
+  }
+  /* 2. Infer octagons from conditions. */
+  a = Frama_C_interval(-1024, 1024);
+  b = Frama_C_interval(-1024, 1024);
+  if (20*k - a - 17 < 5 - b + (1 << 3)                    // a - b > -30
+      && a + (k+6)/2 - b <= 32) {                         // a - b <= 29
+    r = b - a;
+    Frama_C_show_each(r);                                 // [-29..29]
+  }
+  if (a < b && b <= a)
+    Frama_C_show_each_BOTTOM(a, b);
+}
+
+/* Tests the join of the octagons domain. */
+void join () {
+  int a, b, r;
+  int k = Frama_C_interval(-1, 4);
+  if (undet) {
+    a = undet;
+    b = a + k;
+  } else {
+    a = Frama_C_interval(-32, -10);
+    b = k * 5;
+  }
+  // In both case, we have b - a >= -1. The "else" branch was more precise.
+  r = b - a + 1;
+  Frama_C_show_each_join_positive(r);
+  if (undet) {
+    a = undet;
+    b = - (a + k);
+  } else {
+    a = Frama_C_interval(-32, -10);
+    b = k * 5;
+  }
+  // In both case, we have b + a <= 10. The "then" branch was more precise.
+  r = b + a - 10;
+  Frama_C_show_each_join_negative(r);
+}
+
+/* Tests the octagons domain within loops. */
+void loop () {
+  int k = Frama_C_interval(-8, 8);
+  int a = Frama_C_interval(-1024, 1024);
+  int b = a + 1;
+  int c = a + 1;
+  int d = a + k;
+  for (int i = 0; i < 421; i++) {
+    a = a + 2;
+    b = b + 2; // The relation between a and b should be maintained in the loop.
+    c = c + 1; // The relation between a and c should be lost in the loop.
+    d = a + k; // This relation should be maintained.
+  }
+  int d1 = b - a;
+  int d2 = c - a;
+  int d3 = d - a;
+  Frama_C_show_each_singleton_1(d1);
+  Frama_C_show_each_imprecise(d2);
+  Frama_C_show_each_precise(d3);
+}
+
+/* Tests the soundness of the octagons domain in presence of pointers. */
+void pointers () {
+  int x, y, r;
+  int *px = &x, *pr = &r;
+  x = Frama_C_interval(-1024, 1024);
+  y = x + 1;
+  r = y - x;
+  Frama_C_show_each_singleton_1(r);
+  *px = Frama_C_interval(-1024, 1024);
+  Frama_C_show_each_singleton_1(r);
+  *pr = Frama_C_interval(-1024, 1024);
+  Frama_C_show_each_unknown(r);
+  r = y - x;
+  Frama_C_show_each_unknown(r);
+  y = x + 2;
+  r = y - x;
+  Frama_C_show_each_singleton_2(r);
+}
+
+/* Tests the saturation of octagons: inference of a relation between (x, z)
+   from relations between (x, y) and between (y, z). */
+void saturate () {
+  int k = Frama_C_interval(-6, 4);
+  int x = Frama_C_interval(-1024, 1024);
+  int y = k - x;
+  int z = y + 1;
+  int result = - z - x;                  // result == k + 1
+  Frama_C_show_each_saturate(result);    // ∈ [-5..5]
+}
+
+int diff (int x, int y) { return x - y; }
+int neg (int x) { return -x; }
+
+/* Tests the propagation of octagons through function calls. */
+void interprocedural () {
+  int a = Frama_C_interval(-4, 12);
+  int b = Frama_C_interval(-4, 12);
+  int neg_a = neg(a);
+  int neg_b = neg(b);
+  /* [r1] is the direct difference [a-b], [r2] uses the result of the function
+     [neg] (and thus need the octagon inferred in [neg]), and [r3] calls the
+     function [diff] (and the analysis of [diff] needs the octagons inferred
+     here about a and b). */
+  int r1, r2, r3;
+  if (a > b) {
+    r1 = a - b;
+    r2 = a + neg_b;
+    r3 = diff (a, b);
+  } else {
+    r1 = b - a;
+    r2 = b + neg_a;
+    r3 = diff (b, a);
+  }
+  /* With the interprocedural octagons, r1, r2 and r3 must be equally precise. */
+  Frama_C_show_each_equal(r1, r2, r3);
+}
+
+/* Prints the octagons state. */
+void dump () {
+  char k = Frama_C_interval(0, 8);
+  char a = undet;
+  char b = a + k;
+  char c = b - k;
+  Frama_C_dump_each();
+}
+
+void main () {
+  demo ();
+  integer_types ();
+  arith ();
+  join ();
+  loop ();
+  pointers ();
+  saturate ();
+  interprocedural ();
+  dump ();
+}

tests/value/oracle/octagons.res.oracle

+[kernel] Parsing tests/value/octagons.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
+  undet ∈ [--..--]
+[eva] computing for function demo <- main.
+  Called from tests/value/octagons.c:187.
+[eva] computing for function Frama_C_interval <- demo <- main.
+  Called from tests/value/octagons.c:12.
+[eva] using specification for function Frama_C_interval
+[eva] tests/value/octagons.c:12: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:alarm] tests/value/octagons.c:13: Warning: 
+  signed overflow. assert -2147483648 ≤ y - k;
+[eva:alarm] tests/value/octagons.c:14: Warning: 
+  signed overflow. assert x + 3 ≤ 2147483647;
+[eva] Recording results for demo
+[eva] Done for function demo
+[eva] computing for function integer_types <- main.
+  Called from tests/value/octagons.c:188.
+[eva] computing for function Frama_C_interval <- integer_types <- main.
+  Called from tests/value/octagons.c:24.
+[eva] tests/value/octagons.c:24: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:29: 
+  Frama_C_show_each_unreduced_unsigned: [0..4294967295], [0..4294967295]
+[eva] computing for function Frama_C_interval <- integer_types <- main.
+  Called from tests/value/octagons.c:32.
+[eva] tests/value/octagons.c:32: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:37: 
+  Frama_C_show_each_reduced_char: [-7..3], [6..127]
+[eva] Recording results for integer_types
+[eva] Done for function integer_types
+[eva] computing for function arith <- main.
+  Called from tests/value/octagons.c:189.
+[eva] computing for function Frama_C_interval <- arith <- main.
+  Called from tests/value/octagons.c:43.
+[eva] tests/value/octagons.c:43: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- arith <- main.
+  Called from tests/value/octagons.c:46.
+[eva] tests/value/octagons.c:46: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- arith <- main.
+  Called from tests/value/octagons.c:47.
+[eva] tests/value/octagons.c:47: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:52: Frama_C_show_each_precise: [42..66],0%2
+[eva] tests/value/octagons.c:54: Frama_C_show_each_imprecise: [2..106],0%2
+[eva] computing for function Frama_C_interval <- arith <- main.
+  Called from tests/value/octagons.c:55.
+[eva] tests/value/octagons.c:55: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:59: Frama_C_show_each: {50; 60; 70}
+[eva] computing for function Frama_C_interval <- arith <- main.
+  Called from tests/value/octagons.c:62.
+[eva] tests/value/octagons.c:62: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- arith <- main.
+  Called from tests/value/octagons.c:63.
+[eva] tests/value/octagons.c:63: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:67: Frama_C_show_each: [-29..29]
+[eva] Recording results for arith
+[eva] Done for function arith
+[eva] computing for function join <- main.
+  Called from tests/value/octagons.c:190.
+[eva] computing for function Frama_C_interval <- join <- main.
+  Called from tests/value/octagons.c:76.
+[eva] tests/value/octagons.c:76: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:alarm] tests/value/octagons.c:79: Warning: 
+  signed overflow. assert -2147483648 ≤ a + k;
+[eva:alarm] tests/value/octagons.c:79: Warning: 
+  signed overflow. assert a + k ≤ 2147483647;
+[eva] computing for function Frama_C_interval <- join <- main.
+  Called from tests/value/octagons.c:81.
+[eva] tests/value/octagons.c:81: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:86: Frama_C_show_each_join_positive: [0..53]
+[eva:alarm] tests/value/octagons.c:89: Warning: 
+  signed overflow. assert -2147483648 ≤ a + k;
+[eva:alarm] tests/value/octagons.c:89: Warning: 
+  signed overflow. assert a + k ≤ 2147483647;
+[eva:alarm] tests/value/octagons.c:89: Warning: 
+  signed overflow. assert -((int)(a + k)) ≤ 2147483647;
+[eva] computing for function Frama_C_interval <- join <- main.
+  Called from tests/value/octagons.c:91.
+[eva] tests/value/octagons.c:91: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:96: Frama_C_show_each_join_negative: [-47..0]
+[eva] Recording results for join
+[eva] Done for function join
+[eva] computing for function loop <- main.
+  Called from tests/value/octagons.c:191.
+[eva] computing for function Frama_C_interval <- loop <- main.
+  Called from tests/value/octagons.c:101.
+[eva] tests/value/octagons.c:101: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- loop <- main.
+  Called from tests/value/octagons.c:102.
+[eva] tests/value/octagons.c:102: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:106: starting to merge loop iterations
+[eva:alarm] tests/value/octagons.c:107: Warning: 
+  signed overflow. assert a + 2 ≤ 2147483647;
+[eva:alarm] tests/value/octagons.c:108: Warning: 
+  signed overflow. assert b + 2 ≤ 2147483647;
+[eva:alarm] tests/value/octagons.c:110: Warning: 
+  signed overflow. assert a + k ≤ 2147483647;
+[eva:alarm] tests/value/octagons.c:113: Warning: 
+  signed overflow. assert -2147483648 ≤ c - a;
+[eva] tests/value/octagons.c:115: Frama_C_show_each_singleton_1: {1}
+[eva] tests/value/octagons.c:116: Frama_C_show_each_imprecise: [-2147483648..1]
+[eva] tests/value/octagons.c:117: Frama_C_show_each_precise: [-8..8]
+[eva] Recording results for loop
+[eva] Done for function loop
+[eva] computing for function pointers <- main.
+  Called from tests/value/octagons.c:192.
+[eva] computing for function Frama_C_interval <- pointers <- main.
+  Called from tests/value/octagons.c:124.
+[eva] tests/value/octagons.c:124: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:127: Frama_C_show_each_singleton_1: {1}
+[eva] computing for function Frama_C_interval <- pointers <- main.
+  Called from tests/value/octagons.c:128.
+[eva] tests/value/octagons.c:128: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:129: Frama_C_show_each_singleton_1: {1}
+[eva] computing for function Frama_C_interval <- pointers <- main.
+  Called from tests/value/octagons.c:130.
+[eva] tests/value/octagons.c:130: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:131: Frama_C_show_each_unknown: [-1024..1024]
+[eva] tests/value/octagons.c:133: Frama_C_show_each_unknown: [-2047..2049]
+[eva] tests/value/octagons.c:136: Frama_C_show_each_singleton_2: {2}
+[eva] Recording results for pointers
+[eva] Done for function pointers
+[eva] computing for function saturate <- main.
+  Called from tests/value/octagons.c:193.
+[eva] computing for function Frama_C_interval <- saturate <- main.
+  Called from tests/value/octagons.c:142.
+[eva] tests/value/octagons.c:142: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- saturate <- main.
+  Called from tests/value/octagons.c:143.
+[eva] tests/value/octagons.c:143: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:147: Frama_C_show_each_saturate: [-5..5]
+[eva] Recording results for saturate
+[eva] Done for function saturate
+[eva] computing for function interprocedural <- main.
+  Called from tests/value/octagons.c:194.
+[eva] computing for function Frama_C_interval <- interprocedural <- main.
+  Called from tests/value/octagons.c:155.
+[eva] tests/value/octagons.c:155: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- interprocedural <- main.
+  Called from tests/value/octagons.c:156.
+[eva] tests/value/octagons.c:156: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function neg <- interprocedural <- main.
+  Called from tests/value/octagons.c:157.
+[eva] Recording results for neg
+[eva] Done for function neg
+[eva] computing for function neg <- interprocedural <- main.
+  Called from tests/value/octagons.c:158.
+[eva] Recording results for neg
+[eva] Done for function neg
+[eva] computing for function diff <- interprocedural <- main.
+  Called from tests/value/octagons.c:167.
+[eva] Recording results for diff
+[eva] Done for function diff
+[eva] computing for function diff <- interprocedural <- main.
+  Called from tests/value/octagons.c:171.
+[eva] Recording results for diff
+[eva] Done for function diff
+[eva] tests/value/octagons.c:174: 
+  Frama_C_show_each_equal: [0..16], [0..16], [0..16]
+[eva] Recording results for interprocedural
+[eva] Done for function interprocedural
+[eva] computing for function dump <- main.
+  Called from tests/value/octagons.c:195.
+[eva] computing for function Frama_C_interval <- dump <- main.
+  Called from tests/value/octagons.c:179.
+[eva] tests/value/octagons.c:179: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:183: 
+  Frama_C_dump_each:
+  # Octagon domain:
+  {[ k - tmp ∈ {0}
+     a - b ∈ [-8..0]
+     b - c ∈ [0..8]
+     a - c ∈ [-8..8]
+      ]}
+  ==END OF DUMP==
+[eva] Recording results for dump
+[eva] Done for function dump
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function arith:
+  Frama_C_entropy_source ∈ [--..--]
+  k ∈ {0; 1; 2; 3; 4}
+  a ∈ [-1024..1024]
+  b ∈ [-1024..1024]
+  x ∈ [-28..0]
+  y ∈ [1..29]
+  r ∈ [-29..106]
+[eva:final-states] Values at end of function demo:
+  Frama_C_entropy_source ∈ [--..--]
+  y ∈ [--..--]
+  k ∈ [0..10]
+  x ∈ [-2147483648..2147483644]
+  r ∈ [-7..3]
+  t ∈ [6..2147483644] or UNINITIALIZED
+[eva:final-states] Values at end of function diff:
+  __retres ∈ [0..16]
+[eva:final-states] Values at end of function dump:
+  Frama_C_entropy_source ∈ [--..--]
+  k ∈ [0..8]
+  a ∈ [--..--]
+  b ∈ [--..--]
+  c ∈ [--..--]
+[eva:final-states] Values at end of function integer_types:
+  Frama_C_entropy_source ∈ [--..--]
+  k ∈ [0..10]
+  x ∈ [--..--]
+  y ∈ [--..--]
+  r ∈ [--..--]
+  t ∈ [--..--] or UNINITIALIZED
+  ck ∈ [0..10]
+  cx ∈ [--..--]
+  cy ∈ [--..--]
+  cr ∈ [-7..3]
+  ct ∈ [6..127] or UNINITIALIZED
+[eva:final-states] Values at end of function join:
+  Frama_C_entropy_source ∈ [--..--]
+  a ∈ [--..--]
+  b ∈ [-2147483647..2147483647]
+  r ∈ [-47..0]
+  k ∈ {-1; 0; 1; 2; 3; 4}
+[eva:final-states] Values at end of function loop:
+  Frama_C_entropy_source ∈ [--..--]
+  k ∈ [-8..8]
+  a ∈ [-1024..2147483647]
+  b ∈ [-1023..2147483647]
+  c ∈ [-1023..2147483647]
+  d ∈ [-1032..2147483647]
+  d1 ∈ {1}
+  d2 ∈ [-2147483648..1]
+  d3 ∈ [-8..8]
+[eva:final-states] Values at end of function neg:
+  __retres ∈ [-12..4]
+[eva:final-states] Values at end of function interprocedural:
+  Frama_C_entropy_source ∈ [--..--]
+  a ∈ [-4..12]
+  b ∈ [-4..12]
+  neg_a ∈ [-12..4]
+  neg_b ∈ [-12..4]
+  r1 ∈ [0..16]
+  r2 ∈ [0..16]
+  r3 ∈ [0..16]
+[eva:final-states] Values at end of function pointers:
+  Frama_C_entropy_source ∈ [--..--]
+  x ∈ [-1024..1024]
+  y ∈ [-1022..1026]
+  r ∈ {2}
+  px ∈ {{ &x }}
+  pr ∈ {{ &r }}
+[eva:final-states] Values at end of function saturate:
+  Frama_C_entropy_source ∈ [--..--]
+  k ∈ [-6..4]
+  x ∈ [-1024..1024]
+  y ∈ [-1030..1028]
+  z ∈ [-1029..1029]
+  result ∈ [-5..5]
+[eva:final-states] Values at end of function main:
+  Frama_C_entropy_source ∈ [--..--]
+[from] Computing for function arith
+[from] Computing for function Frama_C_interval <-arith
+[from] Done for function Frama_C_interval
+[from] Done for function arith
+[from] Computing for function demo
+[from] Done for function demo
+[from] Computing for function diff
+[from] Done for function diff
+[from] Computing for function dump
+[from] Done for function dump
+[from] Computing for function integer_types
+[from] Done for function integer_types
+[from] Computing for function join
+[from] Done for function join
+[from] Computing for function loop
+[from] Done for function loop
+[from] Computing for function neg
+[from] Done for function neg
+[from] Computing for function interprocedural
+[from] Done for function interprocedural
+[from] Computing for function pointers
+[from] Done for function pointers
+[from] Computing for function saturate
+[from] Done for function saturate
+[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_interval:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+  \result FROM Frama_C_entropy_source; min; max
+[from] Function arith:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function demo:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function diff:
+  \result FROM x; y
+[from] Function dump:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function integer_types:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function join:
+  Frama_C_entropy_source FROM Frama_C_entropy_source; undet (and SELF)
+[from] Function loop:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function neg:
+  \result FROM x
+[from] Function interprocedural:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function pointers:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function saturate:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function main:
+  Frama_C_entropy_source FROM Frama_C_entropy_source; undet (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function arith:
+    Frama_C_entropy_source; k; a; b; x; y; r
+[inout] Inputs for function arith:
+    Frama_C_entropy_source
+[inout] Out (internal) for function demo:
+    Frama_C_entropy_source; y; k; x; r; t
+[inout] Inputs for function demo:
+    Frama_C_entropy_source; undet
+[inout] Out (internal) for function diff:
+    __retres
+[inout] Inputs for function diff:
+    \nothing
+[inout] Out (internal) for function dump:
+    Frama_C_entropy_source; k; tmp; a; b; c
+[inout] Inputs for function dump:
+    Frama_C_entropy_source; undet
+[inout] Out (internal) for function integer_types:
+    Frama_C_entropy_source; k; x; y; r; t; tmp; ck; cx; cy; cr; ct; tmp_0
+[inout] Inputs for function integer_types:
+    Frama_C_entropy_source; undet
+[inout] Out (internal) for function join:
+    Frama_C_entropy_source; a; b; r; k
+[inout] Inputs for function join:
+    Frama_C_entropy_source; undet
+[inout] Out (internal) for function loop:
+    Frama_C_entropy_source; k; a; b; c; d; i; d1; d2; d3
+[inout] Inputs for function loop:
+    Frama_C_entropy_source
+[inout] Out (internal) for function neg:
+    __retres
+[inout] Inputs for function neg:
+    \nothing
+[inout] Out (internal) for function interprocedural:
+    Frama_C_entropy_source; a; b; neg_a; neg_b; r1; r2; r3
+[inout] Inputs for function interprocedural:
+    Frama_C_entropy_source
+[inout] Out (internal) for function pointers:
+    Frama_C_entropy_source; x; y; r; px; pr
+[inout] Inputs for function pointers:
+    Frama_C_entropy_source
+[inout] Out (internal) for function saturate:
+    Frama_C_entropy_source; k; x; y; z; result
+[inout] Inputs for function saturate:
+    Frama_C_entropy_source
+[inout] Out (internal) for function main:
+    Frama_C_entropy_source
+[inout] Inputs for function main:
+    Frama_C_entropy_source; undet