[eva] testing annotation generator

tests/misc/eva_annot.c

+/* run.config
+   PLUGIN: @EVA_PLUGINS@
+   OPT: -eva -eva-precision 2 -eva-annot main -print
+*/
+
+/* -------------------------------------------------------------------------- */
+/* --- Testing EVA Annotations                                            --- */
+/* -------------------------------------------------------------------------- */
+
+//@ ghost int world;
+int a[20];
+
+/*@
+  ensures 0 <= \result <= 100;
+  assigns \result,world \from world;
+*/
+int value(void);
+
+int main(void) {
+  int s = 0;
+  for (int i = 0; i < 20; i++) {
+    int v = value();
+    a[i] = v;
+    s += v;
+  }
+  return s;
+}
+
+/* -------------------------------------------------------------------------- */

tests/misc/eva_annot_float.c

+/* run.config
+   PLUGIN: @EVA_PLUGINS@
+   OPT: -eva -eva-precision 2 -eva-annot main -print
+*/
+
+/* -------------------------------------------------------------------------- */
+/* --- Testing EVA Annotations                                            --- */
+/* -------------------------------------------------------------------------- */
+
+//@ ghost int world;
+double a[20];
+
+/*@
+  ensures \is_finite(\result);
+  ensures 0.0 <= \result <= 100.0;
+  assigns \result,world \from world;
+*/
+double value(void);
+
+double main(void) {
+  double s = 0;
+  for (int i = 0; i < 20; i++) {
+    double v = value();
+    a[i] = v;
+    s += v;
+  }
+  return s;
+}
+
+/* -------------------------------------------------------------------------- */

tests/misc/eva_annot_range.c

+/* run.config
+   PLUGIN: @EVA_PLUGINS@
+   OPT: -eva -eva-precision 2 -eva-annot main -print
+*/
+
+/* -------------------------------------------------------------------------- */
+/* --- Testing EVA Annotations                                            --- */
+/* -------------------------------------------------------------------------- */
+
+//@ ghost int world;
+int a[20];
+
+/*@
+  ensures 0 <= \result <= 100;
+  assigns \result,world \from world;
+*/
+int value(void);
+
+int main(void) {
+  int s = 0;
+  for (int i = 0; i < 20; i+=2) {
+    int v = value();
+    a[i] = v;
+    s += v;
+  }
+  return s;
+}
+
+/* -------------------------------------------------------------------------- */

tests/misc/oracle/eva_annot.res.oracle

+[kernel] Parsing eva_annot.c (with preprocessing)
+[eva] Option -eva-precision 2 detected, automatic configuration of the analysis:
+  option -eva-min-loop-unroll set to 0 (default value).
+  option -eva-auto-loop-unroll set to 32.
+  option -eva-widening-delay set to 2.
+  option -eva-partition-history set to 0 (default value).
+  option -eva-slevel set to 20.
+  option -eva-ilevel set to 16.
+  option -eva-plevel set to 40.
+  option -eva-subdivide-non-linear set to 40.
+  option -eva-remove-redundant-alarms set to true (default value).
+  option -eva-domains set to 'cvalue,equality,symbolic-locations'.
+  option -eva-split-return set to '' (default value).
+  option -eva-equality-through-calls set to 'none'.
+  option -eva-octagon-through-calls set to false (default value).
+[eva] Analyzing a complete application starting at main
+[eva:initial-state] Values of globals at initialization
+  world ∈ {0}
+  a[0..19] ∈ {0}
+[eva:loop-unroll:auto] eva_annot.c:21: Automatic loop unrolling.
+[eva] using specification for function value
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  world ∈ [--..--]
+  a[0..19] ∈ [0..100]
+  s ∈ [0..2000]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 12 statements reached (out of 12): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
+[eva] Annotate main
+/* Generated by Frama-C */
+/*@ ghost int world; */
+int a[20];
+/*@ ensures 0 ≤ \result ≤ 100;
+    assigns \result, world;
+    assigns \result \from world;
+    assigns world \from world;
+ */
+int value(void);
+
+int main(void)
+{
+  int s = 0;
+  {
+    int i = 0;
+    while (1) {
+      /*@ assert Eva_domain: 0 ≤ i ≤ 20; */
+      if (! (i < 20)) break;
+      {
+        int v = value();
+        /*@ assert Eva_domain: 0 ≤ i ≤ 19; */
+        /*@ assert Eva_domain: 0 ≤ v ≤ 100; */
+        a[i] = v;
+        /*@ assert Eva_domain: 0 ≤ s ≤ 1900; */
+        /*@ assert Eva_domain: 0 ≤ v ≤ 100; */
+        s += v;
+      }
+      /*@ assert Eva_domain: 0 ≤ i ≤ 19; */
+      i ++;
+    }
+  }
+  /*@ assert Eva_domain: 0 ≤ s ≤ 2000; */
+  return s;
+}
+
+

tests/misc/oracle/eva_annot_float.res.oracle

+[kernel] Parsing eva_annot_float.c (with preprocessing)
+[eva] Option -eva-precision 2 detected, automatic configuration of the analysis:
+  option -eva-min-loop-unroll set to 0 (default value).
+  option -eva-auto-loop-unroll set to 32.
+  option -eva-widening-delay set to 2.
+  option -eva-partition-history set to 0 (default value).
+  option -eva-slevel set to 20.
+  option -eva-ilevel set to 16.
+  option -eva-plevel set to 40.
+  option -eva-subdivide-non-linear set to 40.
+  option -eva-remove-redundant-alarms set to true (default value).
+  option -eva-domains set to 'cvalue,equality,symbolic-locations'.
+  option -eva-split-return set to '' (default value).
+  option -eva-equality-through-calls set to 'none'.
+  option -eva-octagon-through-calls set to false (default value).
+[eva] Analyzing a complete application starting at main
+[eva:initial-state] Values of globals at initialization
+  world ∈ {0}
+  a[0..19] ∈ {0}
+[eva:loop-unroll:auto] eva_annot_float.c:22: Automatic loop unrolling.
+[eva] using specification for function value
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  world ∈ [--..--]
+  a[0..19] ∈ [-0. .. 100.]
+  s ∈ [0. .. 2000.]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 12 statements reached (out of 12): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
+[eva] Annotate main
+/* Generated by Frama-C */
+/*@ ghost int world; */
+double a[20];
+/*@ ensures \is_finite(\result);
+    ensures 0.0 ≤ \result ≤ 100.0;
+    assigns \result, world;
+    assigns \result \from world;
+    assigns world \from world;
+ */
+double value(void);
+
+double main(void)
+{
+  double s = (double)0;
+  {
+    int i = 0;
+    while (1) {
+      /*@ assert Eva_domain: 0 ≤ i ≤ 20; */
+      if (! (i < 20)) break;
+      {
+        double v = value();
+        /*@ assert Eva_domain: 0 ≤ i ≤ 19; */
+        /*@ assert
+            Eva_domain:
+              -0.0000000000000000e+00d ≤ v ≤ 1.0000000000000000e+02d;
+        */
+        a[i] = v;
+        /*@ assert
+            Eva_domain:
+              0.0000000000000000e+00d ≤ s ≤ 1.9000000000000000e+03d;
+        */
+        /*@ assert
+            Eva_domain:
+              -0.0000000000000000e+00d ≤ v ≤ 1.0000000000000000e+02d;
+        */
+        s += v;
+      }
+      /*@ assert Eva_domain: 0 ≤ i ≤ 19; */
+      i ++;
+    }
+  }
+  /*@ assert
+      Eva_domain: 0.0000000000000000e+00d ≤ s ≤ 2.0000000000000000e+03d;
+  */
+  return s;
+}
+
+

tests/misc/oracle/eva_annot_range.res.oracle

+[kernel] Parsing eva_annot_range.c (with preprocessing)
+[eva] Option -eva-precision 2 detected, automatic configuration of the analysis:
+  option -eva-min-loop-unroll set to 0 (default value).
+  option -eva-auto-loop-unroll set to 32.
+  option -eva-widening-delay set to 2.
+  option -eva-partition-history set to 0 (default value).
+  option -eva-slevel set to 20.
+  option -eva-ilevel set to 16.
+  option -eva-plevel set to 40.
+  option -eva-subdivide-non-linear set to 40.
+  option -eva-remove-redundant-alarms set to true (default value).
+  option -eva-domains set to 'cvalue,equality,symbolic-locations'.
+  option -eva-split-return set to '' (default value).
+  option -eva-equality-through-calls set to 'none'.
+  option -eva-octagon-through-calls set to false (default value).
+[eva] Analyzing a complete application starting at main
+[eva:initial-state] Values of globals at initialization
+  world ∈ {0}
+  a[0..19] ∈ {0}
+[eva:loop-unroll:auto] eva_annot_range.c:21: Automatic loop unrolling.
+[eva] using specification for function value
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  world ∈ [--..--]
+  a[0] ∈ [0..100]
+   [1] ∈ {0}
+   [2] ∈ [0..100]
+   [3] ∈ {0}
+   [4] ∈ [0..100]
+   [5] ∈ {0}
+   [6] ∈ [0..100]
+   [7] ∈ {0}
+   [8] ∈ [0..100]
+   [9] ∈ {0}
+   [10] ∈ [0..100]
+   [11] ∈ {0}
+   [12] ∈ [0..100]
+   [13] ∈ {0}
+   [14] ∈ [0..100]
+   [15] ∈ {0}
+   [16] ∈ [0..100]
+   [17] ∈ {0}
+   [18] ∈ [0..100]
+   [19] ∈ {0}
+  s ∈ [0..1000]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 12 statements reached (out of 12): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
+[eva] Annotate main
+/* Generated by Frama-C */
+/*@ ghost int world; */
+int a[20];
+/*@ ensures 0 ≤ \result ≤ 100;
+    assigns \result, world;
+    assigns \result \from world;
+    assigns world \from world;
+ */
+int value(void);
+
+int main(void)
+{
+  int s = 0;
+  {
+    int i = 0;
+    while (1) {
+      /*@ assert
+          Eva_domain:
+            i ≡ 0 ∨ i ≡ 2 ∨ i ≡ 4 ∨ i ≡ 6 ∨ i ≡ 8 ∨
+            i ≡ 10 ∨ i ≡ 12 ∨ i ≡ 14 ∨ i ≡ 16 ∨ i ≡ 18 ∨
+            i ≡ 20;
+      */
+      if (! (i < 20)) break;
+      {
+        int v = value();
+        /*@ assert
+            Eva_domain:
+              i ≡ 0 ∨ i ≡ 2 ∨ i ≡ 4 ∨ i ≡ 6 ∨ i ≡ 8 ∨
+              i ≡ 10 ∨ i ≡ 12 ∨ i ≡ 14 ∨ i ≡ 16 ∨ i ≡ 18;
+        */
+        /*@ assert Eva_domain: 0 ≤ v ≤ 100; */
+        a[i] = v;
+        /*@ assert Eva_domain: 0 ≤ s ≤ 900; */
+        /*@ assert Eva_domain: 0 ≤ v ≤ 100; */
+        s += v;
+      }
+      /*@ assert
+          Eva_domain:
+            i ≡ 0 ∨ i ≡ 2 ∨ i ≡ 4 ∨ i ≡ 6 ∨ i ≡ 8 ∨
+            i ≡ 10 ∨ i ≡ 12 ∨ i ≡ 14 ∨ i ≡ 16 ∨ i ≡ 18;
+      */
+      i += 2;
+    }
+  }
+  /*@ assert Eva_domain: 0 ≤ s ≤ 1000; */
+  return s;
+}
+
+