Merge branch 'feature/eva/float-octagon' into 'master'

[Eva] Octagon: infers relations on the integer conversion of floating-point variables

See merge request frama-c/frama-c!3953

tests/value/octagons.c

@@ -223,6 +223,39 @@ void pub301 () {
   }
 }
 
+#define MAX 20
+
+void arrays () {
+  int a[MAX], t[MAX];
+  /*@ loop unroll MAX; */ // Unroll to ensure array initialization.
+  for (int i = 0; i < MAX; i++) {
+    a[i] = undet;
+  }
+
+  int x = Frama_C_interval(1, MAX);
+  for (int j = x - 1; j >= 0; j--) {
+    // Need the relation j <= x-1 to prove that index x-1-j >= 0.
+    t[j] = a[x - 1 - j];
+  }
+
+  int y = Frama_C_interval(0, MAX-1);
+  int index = (MAX-1) - y;
+  for (int j = y; j < MAX; j++) {
+    // Need the relation index + j == MAX-1 to prove index >= 0.
+    t[index] = a[j];
+    index --;
+  }
+
+  // Same with a floating-point variable f instead of x.
+  float f = Frama_C_float_interval(0., (float)(MAX-1));
+  index = (MAX-1) - (int)f;
+  for (int j = (int)f; j < MAX; j++) {
+    // Need the relation index + j == MAX-1 to prove index >= 0.
+    t[index] = a[j];
+    index --;
+  }
+}
+
 void main () {
   demo ();
   integer_types ();
@@ -234,4 +267,5 @@ void main () {
   interprocedural ();
   dump ();
   pub301 ();
+  arrays ();
 }

tests/value/oracle/octagons.res.oracle

@@ -5,7 +5,7 @@
 [eva:initial-state] Values of globals at initialization
   undet ∈ [--..--]
 [eva] computing for function demo <- main.
-  Called from octagons.c:227.
+  Called from octagons.c:260.
 [eva] computing for function Frama_C_interval <- demo <- main.
   Called from octagons.c:12.
 [eva] using specification for function Frama_C_interval
@@ -19,7 +19,7 @@
 [eva] Recording results for demo
 [eva] Done for function demo
 [eva] computing for function integer_types <- main.
-  Called from octagons.c:228.
+  Called from octagons.c:261.
 [eva] computing for function Frama_C_interval <- integer_types <- main.
   Called from octagons.c:23.
 [eva] octagons.c:23: 
@@ -69,7 +69,7 @@
 [eva] Recording results for integer_types
 [eva] Done for function integer_types
 [eva] computing for function arith <- main.
-  Called from octagons.c:229.
+  Called from octagons.c:262.
 [eva] computing for function Frama_C_interval <- arith <- main.
   Called from octagons.c:70.
 [eva] octagons.c:70: 
@@ -107,7 +107,7 @@
 [eva] Recording results for arith
 [eva] Done for function arith
 [eva] computing for function join <- main.
-  Called from octagons.c:230.
+  Called from octagons.c:263.
 [eva] computing for function Frama_C_interval <- join <- main.
   Called from octagons.c:103.
 [eva] octagons.c:103: 
@@ -138,7 +138,7 @@
 [eva] Recording results for join
 [eva] Done for function join
 [eva] computing for function loop <- main.
-  Called from octagons.c:231.
+  Called from octagons.c:264.
 [eva] computing for function Frama_C_interval <- loop <- main.
   Called from octagons.c:128.
 [eva] octagons.c:128: 
@@ -164,7 +164,7 @@
 [eva] Recording results for loop
 [eva] Done for function loop
 [eva] computing for function pointers <- main.
-  Called from octagons.c:232.
+  Called from octagons.c:265.
 [eva] computing for function Frama_C_interval <- pointers <- main.
   Called from octagons.c:151.
 [eva] octagons.c:151: 
@@ -188,7 +188,7 @@
 [eva] Recording results for pointers
 [eva] Done for function pointers
 [eva] computing for function saturate <- main.
-  Called from octagons.c:233.
+  Called from octagons.c:266.
 [eva] computing for function Frama_C_interval <- saturate <- main.
   Called from octagons.c:169.
 [eva] octagons.c:169: 
@@ -203,7 +203,7 @@
 [eva] Recording results for saturate
 [eva] Done for function saturate
 [eva] computing for function interprocedural <- main.
-  Called from octagons.c:234.
+  Called from octagons.c:267.
 [eva] computing for function Frama_C_interval <- interprocedural <- main.
   Called from octagons.c:182.
 [eva] octagons.c:182: 
@@ -218,10 +218,7 @@
   Called from octagons.c:184.
 [eva] Recording results for neg
 [eva] Done for function neg
-[eva] computing for function neg <- interprocedural <- main.
-  Called from octagons.c:185.
-[eva] Recording results for neg
-[eva] Done for function neg
+[eva] octagons.c:185: Reusing old results for call to neg
 [eva] computing for function diff <- interprocedural <- main.
   Called from octagons.c:194.
 [eva] Recording results for diff
@@ -234,7 +231,7 @@
 [eva] Recording results for interprocedural
 [eva] Done for function interprocedural
 [eva] computing for function dump <- main.
-  Called from octagons.c:235.
+  Called from octagons.c:268.
 [eva] computing for function Frama_C_interval <- dump <- main.
   Called from octagons.c:206.
 [eva] octagons.c:206: 
@@ -259,7 +256,7 @@
 [eva] Recording results for dump
 [eva] Done for function dump
 [eva] computing for function pub301 <- main.
-  Called from octagons.c:236.
+  Called from octagons.c:269.
 [eva] computing for function Frama_C_interval <- pub301 <- main.
   Called from octagons.c:216.
 [eva] octagons.c:216: 
@@ -272,6 +269,31 @@
 [eva] Done for function Frama_C_interval
 [eva] Recording results for pub301
 [eva] Done for function pub301
+[eva] computing for function arrays <- main.
+  Called from octagons.c:270.
+[eva] computing for function Frama_C_interval <- arrays <- main.
+  Called from octagons.c:235.
+[eva] octagons.c:235: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] octagons.c:236: starting to merge loop iterations
+[eva] computing for function Frama_C_interval <- arrays <- main.
+  Called from octagons.c:241.
+[eva] octagons.c:241: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] octagons.c:243: starting to merge loop iterations
+[eva] computing for function Frama_C_float_interval <- arrays <- main.
+  Called from octagons.c:250.
+[eva] using specification for function Frama_C_float_interval
+[eva] octagons.c:250: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] octagons.c:250: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva] octagons.c:252: starting to merge loop iterations
+[eva] Recording results for arrays
+[eva] Done for function arrays
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -283,6 +305,14 @@
   x ∈ [-28..0]
   y ∈ [1..29]
   r ∈ [-29..106]
+[eva:final-states] Values at end of function arrays:
+  Frama_C_entropy_source ∈ [--..--]
+  a[0..19] ∈ [--..--]
+  t[0..19] ∈ [--..--] or UNINITIALIZED
+  x ∈ [1..20]
+  y ∈ [0..19]
+  index ∈ {-1}
+  f ∈ [-0. .. 19.]
 [eva:final-states] Values at end of function demo:
   Frama_C_entropy_source ∈ [--..--]
   y ∈ [--..--]
@@ -364,6 +394,10 @@
 [from] Computing for function Frama_C_interval <-arith
 [from] Done for function Frama_C_interval
 [from] Done for function arith
+[from] Computing for function arrays
+[from] Computing for function Frama_C_float_interval <-arrays
+[from] Done for function Frama_C_float_interval
+[from] Done for function arrays
 [from] Computing for function demo
 [from] Done for function demo
 [from] Computing for function diff
@@ -390,11 +424,16 @@
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_float_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 arith:
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function arrays:
+  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:
@@ -424,6 +463,10 @@
     Frama_C_entropy_source; k; a; b; x; y; r
 [inout] Inputs for function arith:
     Frama_C_entropy_source
+[inout] Out (internal) for function arrays:
+    Frama_C_entropy_source; a[0..19]; t[0..19]; i; x; j; y; index; j_0; f; j_1
+[inout] Inputs for function arrays:
+    Frama_C_entropy_source; undet
 [inout] Out (internal) for function demo:
     Frama_C_entropy_source; y; k; x; r; t
 [inout] Inputs for function demo:

tests/value/oracle_apron/octagons.res.oracle

-325,328c325,328
+221c221,224
+< [eva] octagons.c:185: Reusing old results for call to neg
+---
+> [eva] computing for function neg <- interprocedural <- main.
+>   Called from octagons.c:185.
+> [eva] Recording results for neg
+> [eva] Done for function neg
+355,358c358,361
 <   a ∈ [-1024..2147483647]
 <   b ∈ [-1023..2147483647]
 <   c ∈ [-1023..2147483647]

tests/value/oracle_equality/octagons.res.oracle

@@ -2,7 +2,14 @@
 < [eva] octagons.c:54: Frama_C_show_each_unreduced_char: [-128..127], [-128..127]
 ---
 > [eva] octagons.c:54: Frama_C_show_each_unreduced_char: [-118..114], [6..127]
-312c312
+221c221,224
+< [eva] octagons.c:185: Reusing old results for call to neg
+---
+> [eva] computing for function neg <- interprocedural <- main.
+>   Called from octagons.c:185.
+> [eva] Recording results for neg
+> [eva] Done for function neg
+342c345
 <   ct ∈ [--..--] or UNINITIALIZED
 ---
 >   ct ∈ [6..127] or UNINITIALIZED

tests/value/oracle_gauges/octagons.res.oracle

@@ -11,7 +11,7 @@
 < [eva] octagons.c:143: Frama_C_show_each_imprecise: [-2147483648..1]
 ---
 > [eva] octagons.c:143: Frama_C_show_each_imprecise: [-2468..1]
-325,328c317,320
+355,358c347,350
 <   a ∈ [-1024..2147483647]
 <   b ∈ [-1023..2147483647]
 <   c ∈ [-1023..2147483647]
@@ -21,7 +21,7 @@
 >   b ∈ [-181..1867]
 >   c ∈ [-602..1446]
 >   d ∈ [-190..1874]
-330c322
+360c352
 <   d2 ∈ [-2147483648..1]
 ---
 >   d2 ∈ [-2468..1]