[Eva] Removes useless pragma in test.

tests/value/loop_wvar.i

@@ -9,9 +9,6 @@
 void main(void)
 { int n = 13;
   int i,j;
-// ceci était une annotation, mais on ne fait pas moins bien sans
-// maintenant:
-// loop pragma WIDEN_VARIABLES i;
   /*@ loop widen_hints i, 12, 13; */
   for (i=0; i<n; i++)
     {
@@ -35,7 +32,6 @@ void main_err1(void)
 void main_err2(void)
 { int n = 13;
   int i,j;
-  /*@ loop pragma WIDEN_VARIABLES 12; */
   for (i=0; i<n; i++)
     {
       j = 4 * i + 7;
@@ -48,7 +44,7 @@ void main_unhelpful () {
   int next = 0;
   int i;
 
-/*@ loop widen_hints next, 24; */ // This pragma is unhelpful, but used to interfere with the bound for i.
+/*@ loop widen_hints next, 24; */ // This hint is unhelpful, but used to interfere with the bound for i.
   for (i=0;i<30;i++) {
     int vsize = max;
     int vnext = next;

tests/value/oracle/loop_wvar.0.res.oracle

@@ -4,7 +4,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] loop_wvar.i:16: starting to merge loop iterations
+[eva] loop_wvar.i:13: starting to merge loop iterations
 [eva] Recording results for main
 [eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -13,14 +13,12 @@
   i ∈ [13..2147483647]
   j ∈ [7..55],3%4 or UNINITIALIZED
 [kernel] Parsing loop_wvar.i (no preprocessing)
-[kernel:annot-error] loop_wvar.i:38: Warning: 
-  invalid pragma '12'. Ignoring loop annotation
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] loop_wvar.i:16: starting to merge loop iterations
+[eva] loop_wvar.i:13: starting to merge loop iterations
 [eva] Recording results for main
 [eva] Done for function main
 [eva] ====== VALUES COMPUTED ======

tests/value/oracle/loop_wvar.1.res.oracle

 [kernel] Parsing loop_wvar.i (no preprocessing)
-[kernel:annot-error] loop_wvar.i:38: Warning: 
-  invalid pragma '12'. Ignoring loop annotation
 [eva] Analyzing a complete application starting at main3
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
 [eva] computing for function main_unhelpful <- main3.
-  Called from loop_wvar.i:84.
-[eva] loop_wvar.i:52: starting to merge loop iterations
-[eva:alarm] loop_wvar.i:57: Warning: 
+  Called from loop_wvar.i:80.
+[eva] loop_wvar.i:48: starting to merge loop iterations
+[eva:alarm] loop_wvar.i:53: Warning: 
   signed overflow. assert next + 1 ≤ 2147483647;
 [eva] Recording results for main_unhelpful
 [eva] Done for function main_unhelpful
 [eva] computing for function main_multiple_hints <- main3.
-  Called from loop_wvar.i:85.
-[eva] loop_wvar.i:71: Frama_C_show_each: {0}, {0}, {0}
-[eva] loop_wvar.i:69: starting to merge loop iterations
-[eva] loop_wvar.i:71: Frama_C_show_each: {0; 1}, {0; 1}, {0; 1}
-[eva] loop_wvar.i:71: Frama_C_show_each: {0; 1; 2}, {0; 1; 2}, {0; 1; 2}
-[eva] loop_wvar.i:71: Frama_C_show_each: [0..9], {0; 1; 2; 3}, {0; 1; 2; 3}
-[eva] loop_wvar.i:71: 
+  Called from loop_wvar.i:81.
+[eva] loop_wvar.i:67: Frama_C_show_each: {0}, {0}, {0}
+[eva] loop_wvar.i:65: starting to merge loop iterations
+[eva] loop_wvar.i:67: Frama_C_show_each: {0; 1}, {0; 1}, {0; 1}
+[eva] loop_wvar.i:67: Frama_C_show_each: {0; 1; 2}, {0; 1; 2}, {0; 1; 2}
+[eva] loop_wvar.i:67: Frama_C_show_each: [0..9], {0; 1; 2; 3}, {0; 1; 2; 3}
+[eva] loop_wvar.i:67: 
   Frama_C_show_each: [0..9], {0; 1; 2; 3; 4}, {0; 1; 2; 3; 4}
-[eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..17], [0..11]
-[eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..18], [0..12]
+[eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..17], [0..11]
+[eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..18], [0..12]
 [eva] Recording results for main_multiple_hints
 [eva] Done for function main_multiple_hints
 [eva] Recording results for main3

tests/value/oracle/loop_wvar.2.res.oracle

 [kernel] Parsing loop_wvar.i (no preprocessing)
-[kernel:annot-error] loop_wvar.i:38: Warning: 
-  invalid pragma '12'. Ignoring loop annotation
 [eva] Analyzing a complete application starting at main_err1
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] loop_wvar.i:27: starting to merge loop iterations
+[eva] loop_wvar.i:24: starting to merge loop iterations
 [eva] Recording results for main_err1
 [eva] Done for function main_err1
 [eva] ====== VALUES COMPUTED ======

tests/value/oracle/loop_wvar.3.res.oracle

 [kernel] Parsing loop_wvar.i (no preprocessing)
-[kernel:annot-error] loop_wvar.i:38: Warning: 
-  invalid pragma '12'. Ignoring loop annotation
 [eva] Analyzing a complete application starting at main_err2
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] loop_wvar.i:39: starting to merge loop iterations
+[eva] loop_wvar.i:35: starting to merge loop iterations
 [eva] Recording results for main_err2
 [eva] Done for function main_err2
 [eva] ====== VALUES COMPUTED ======

tests/value/oracle_apron/loop_wvar.1.res.oracle

-12,13d11
-< [eva:alarm] loop_wvar.i:57: Warning: 
+10,11d9
+< [eva:alarm] loop_wvar.i:53: Warning: 
 <   signed overflow. assert next + 1 ≤ 2147483647;
-25,26c23
-< [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..17], [0..11]
-< [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..18], [0..12]
+23,24c21
+< [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..17], [0..11]
+< [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..18], [0..12]
 ---
-> [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..9], [0..9]
-35,36c32,33
+> [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..9], [0..9]
+33,34c30,31
 <   j ∈ [0..18]
 <   k ∈ [0..12]
 ---
 >   j ∈ [0..17]
 >   k ∈ [0..11]
-39c36
+37c34
 <   next ∈ [0..2147483647]
 ---
 >   next ∈ [0..25]

tests/value/oracle_gauges/loop_wvar.1.res.oracle

-25,26c25
-< [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..17], [0..11]
-< [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..18], [0..12]
+23,24c23
+< [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..17], [0..11]
+< [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..18], [0..12]
 ---
-> [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..9], [0..9]
-35,36c34,35
+> [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..9], [0..9]
+33,34c32,33
 <   j ∈ [0..18]
 <   k ∈ [0..12]
 ---

tests/value/oracle_octagon/loop_wvar.1.res.oracle

-12,13d11
-< [eva:alarm] loop_wvar.i:57: Warning: 
+10,11d9
+< [eva:alarm] loop_wvar.i:53: Warning: 
 <   signed overflow. assert next + 1 ≤ 2147483647;
-39c37
+37c35
 <   next ∈ [0..2147483647]
 ---
 >   next ∈ [0..25]