diff --git a/tests/value/diff_apron b/tests/value/diff_apron
index 2ead3a445bbc76a876c5e89fb0e57325a79f52a0..e43d97743cb15e14e2c12e5d5ca200006be5b5a1 100644
--- a/tests/value/diff_apron
+++ b/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}
diff --git a/tests/value/diff_equalities b/tests/value/diff_equalities
index 821b7e3c2fc6803fa2584c2b2deedc7692ba8b60..83d093f00364f8bd80e50ed2ff37c260660b6c70 100644
--- a/tests/value/diff_equalities
+++ b/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
diff --git a/tests/value/diff_gauges b/tests/value/diff_gauges
index e0312fea2b92804faca6c4ccae3d2e2afc83fda6..ab9ecdc28fc62ed33d66256204e38c85a05476ed 100644
--- a/tests/value/diff_gauges
+++ b/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
diff --git a/tests/value/octagons.c b/tests/value/octagons.c
new file mode 100644
index 0000000000000000000000000000000000000000..34f6a7191191f6c61b10a9a4b7dc9f96f0352111
--- /dev/null
+++ b/tests/value/octagons.c
@@ -0,0 +1,196 @@
+/* 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 ();
+}
diff --git a/tests/value/oracle/octagons.res.oracle b/tests/value/oracle/octagons.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..2f2626a65ffa2d0009b042400cd207ba02de8264
--- /dev/null
+++ b/tests/value/oracle/octagons.res.oracle
@@ -0,0 +1,407 @@
+[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