[tests] prepare test configs for deletion of spurious warnings

tests/journal/control.i

 /* run.config
+
+
  COMMENT: do not compare generated journals since they depend on current time
  PLUGIN: @EVA_PLUGINS@
    EXECNOW: BIN control_journal.ml @frama-c@ @PTEST_FILE@ -journal-enable -eva -deps -out @EVA_OPTIONS@ -main f -journal-name @PTEST_RESULT@/control_journal.ml > @DEV_NULL@ 2> @DEV_NULL@

tests/journal/control2.c

 /* run.config
+
+
  PLUGIN: @EVA_PLUGINS@
    EXECNOW: BIN control_journal2.ml @frama-c@ -journal-enable -eva -deps -out -main f -journal-name @PTEST_RESULT@/control_journal2.ml @PTEST_FILE@ > @DEV_NULL@ 2> @DEV_NULL@
  SCRIPT: @PTEST_RESULT@/control_journal2.ml

tests/journal/intra.i

 /* run.config
+
+
  PLUGIN: @EVA_PLUGINS@ sparecode
  MODULE: @PTEST_NAME@
    EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -journal-enable -journal-name @PTEST_RESULT@/intra_journal.ml @PTEST_FILE@ > @DEV_NULL@ 2> @DEV_NULL@

tests/journal/oracle/control.0.res.oracle

@@ -7,8 +7,8 @@
   y ∈ {0}
   c ∈ {0}
   d ∈ {0}
-[eva] control.i:22: starting to merge loop iterations
-[eva:alarm] control.i:25: Warning: signed overflow. assert x + 1 ≤ 2147483647;
+[eva] control.i:24: starting to merge loop iterations
+[eva:alarm] control.i:27: Warning: signed overflow. assert x + 1 ≤ 2147483647;
 [eva] Recording results for f
 [eva] done for function f
 [eva] ====== VALUES COMPUTED ======

tests/journal/oracle/control.1.res.oracle

@@ -7,8 +7,8 @@
   y ∈ {0}
   c ∈ {0}
   d ∈ {0}
-[eva] control.i:22: starting to merge loop iterations
-[eva:alarm] control.i:25: Warning: signed overflow. assert x + 1 ≤ 2147483647;
+[eva] control.i:24: starting to merge loop iterations
+[eva:alarm] control.i:27: Warning: signed overflow. assert x + 1 ≤ 2147483647;
 [eva] Recording results for f
 [eva] done for function f
 [eva] ====== VALUES COMPUTED ======
@@ -43,7 +43,7 @@
   y ∈ {0}
   c ∈ {0}
   d ∈ {0}
-[eva:alarm] control.i:25: Warning: signed overflow. assert x + 1 ≤ 2147483647;
+[eva:alarm] control.i:27: Warning: signed overflow. assert x + 1 ≤ 2147483647;
 [eva] Recording results for f
 [from] Computing for function f
 [from] Done for function f

tests/journal/oracle/control2.res.oracle

@@ -7,8 +7,8 @@
   y ∈ {0}
   c ∈ {0}
   d ∈ {0}
-[eva] control2.c:12: starting to merge loop iterations
-[eva:alarm] control2.c:15: Warning: 
+[eva] control2.c:14: starting to merge loop iterations
+[eva:alarm] control2.c:17: Warning: 
   signed overflow. assert x + 1 ≤ 2147483647;
 [eva] done for function f
 [eva] ====== VALUES COMPUTED ======
@@ -37,12 +37,12 @@
   y ∈ [--..--]
   c ∈ [--..--]
   d ∈ [--..--]
-[eva:alarm] control2.c:13: Warning: 
+[eva:alarm] control2.c:15: Warning: 
   signed overflow. assert y + 1 ≤ 2147483647;
-[eva:alarm] control2.c:13: Warning: 
-  signed overflow. assert x + 1 ≤ 2147483647;
 [eva:alarm] control2.c:15: Warning: 
   signed overflow. assert x + 1 ≤ 2147483647;
+[eva:alarm] control2.c:17: Warning: 
+  signed overflow. assert x + 1 ≤ 2147483647;
 [eva] done for function f
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function f:

tests/journal/oracle/control2_sav.res

@@ -7,8 +7,8 @@
   y ∈ {0}
   c ∈ {0}
   d ∈ {0}
-[eva] control2.c:12: starting to merge loop iterations
-[eva:alarm] control2.c:15: Warning: 
+[eva] control2.c:14: starting to merge loop iterations
+[eva:alarm] control2.c:17: Warning: 
   signed overflow. assert x + 1 ≤ 2147483647;
 [eva] done for function f
 [eva] ====== VALUES COMPUTED ======
@@ -38,12 +38,12 @@
   y ∈ [--..--]
   c ∈ [--..--]
   d ∈ [--..--]
-[eva:alarm] control2.c:13: Warning: 
+[eva:alarm] control2.c:15: Warning: 
   signed overflow. assert y + 1 ≤ 2147483647;
-[eva:alarm] control2.c:13: Warning: 
-  signed overflow. assert x + 1 ≤ 2147483647;
 [eva:alarm] control2.c:15: Warning: 
   signed overflow. assert x + 1 ≤ 2147483647;
+[eva:alarm] control2.c:17: Warning: 
+  signed overflow. assert x + 1 ≤ 2147483647;
 [eva] done for function f
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function f:

tests/journal/oracle/intra.res.oracle

@@ -8,49 +8,49 @@
   X10 ∈ {0}
   Y10 ∈ {0}
 [eva] computing for function param <- main.
-  Called from intra.i:81.
+  Called from intra.i:83.
 [eva] Recording results for param
 [eva] Done for function param
 [eva] computing for function tmp <- main.
-  Called from intra.i:82.
-[eva] intra.i:20: assertion got status valid.
+  Called from intra.i:84.
 [eva] intra.i:22: assertion got status valid.
+[eva] intra.i:24: assertion got status valid.
 [eva] Recording results for tmp
 [eva] Done for function tmp
 [eva] computing for function spare_called_fct <- main.
-  Called from intra.i:83.
+  Called from intra.i:85.
 [eva] Recording results for spare_called_fct
 [eva] Done for function spare_called_fct
 [eva] computing for function call_two_outputs <- main.
-  Called from intra.i:84.
+  Called from intra.i:86.
 [eva] computing for function two_outputs <- call_two_outputs <- main.
-  Called from intra.i:48.
+  Called from intra.i:50.
 [eva] Recording results for two_outputs
 [eva] Done for function two_outputs
 [eva] computing for function two_outputs <- call_two_outputs <- main.
-  Called from intra.i:52.
+  Called from intra.i:54.
 [eva] Recording results for two_outputs
 [eva] Done for function two_outputs
 [eva] Recording results for call_two_outputs
 [eva] Done for function call_two_outputs
 [eva] computing for function loop <- main.
-  Called from intra.i:85.
-[eva] intra.i:63: assertion got status valid.
-[eva] intra.i:64: loop invariant got status valid.
-[eva] intra.i:66: starting to merge loop iterations
+  Called from intra.i:87.
+[eva] intra.i:65: assertion got status valid.
+[eva] intra.i:66: loop invariant got status valid.
+[eva] intra.i:68: starting to merge loop iterations
 [eva] Recording results for loop
 [eva] Done for function loop
 [eva] computing for function assign <- main.
-  Called from intra.i:86.
+  Called from intra.i:88.
 [eva] Recording results for assign
 [eva] Done for function assign
 [eva] computing for function assign <- main.
-  Called from intra.i:87.
+  Called from intra.i:89.
 [eva] Recording results for assign
 [eva] Done for function assign
 [eva] computing for function stop <- main.
-  Called from intra.i:90.
-[kernel:annot:missing-spec] intra.i:90: Warning: 
+  Called from intra.i:92.
+[kernel:annot:missing-spec] intra.i:92: Warning: 
   Neither code nor specification for function stop, generating default assigns from the prototype
 [eva] using specification for function stop
 [eva] Done for function stop

tests/misc/my_visitor.c

 /* run.config
+
+
  PLUGIN:
  MODULE: @PTEST_NAME@
    EXECNOW: LOG my_visitor_sav.res LOG my_visitor_sav.err BIN my_visitor.sav @frama-c@ @PTEST_FILE@ -main f -save @PTEST_RESULT@/@PTEST_NAME@.sav > @PTEST_RESULT@/@PTEST_NAME@_sav.res 2> @PTEST_RESULT@/@PTEST_NAME@_sav.err

tests/saveload/basic.i

 /* run.config
+
+
  MODULE: @PTEST_NAME@
    EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
  MODULE:

tests/saveload/bool.c

 /* run.config
+
+
    EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -save @PTEST_NAME@.sav -machdep x86_32 -eva @EVA_OPTIONS@ @PTEST_FILE@ > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
    STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -out -input -deps"
    STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -eva @EVA_OPTIONS@"

tests/saveload/callbacks.i

 /* run.config
+
+
    EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ @PTEST_FILE@ -out -calldeps -eva-show-progress -main main1 -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
    STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -main main2 -then -main main3"
 */

tests/saveload/deps.i

 /* run.config
+
+
  MODULE: deps_A
    EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
    STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -eva @EVA_OPTIONS@ -out -input -deps "

tests/saveload/isset.c

 /* run.config
+
+
    EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -quiet -eva @EVA_OPTIONS@ -save @PTEST_NAME@.sav @PTEST_FILE@ > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
    STDOPT: +"-quiet -load %{dep:@PTEST_NAME@.sav}"
    STDOPT: +"-load %{dep:@PTEST_NAME@.sav}"

tests/saveload/oracle/basic_sav.1.res

@@ -4,9 +4,9 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] basic.i:18: assertion got status valid.
-[eva] basic.i:19: starting to merge loop iterations
-[eva:alarm] basic.i:19: Warning: signed overflow. assert -2147483648 ≤ i - 1;
+[eva] basic.i:20: assertion got status valid.
+[eva] basic.i:21: starting to merge loop iterations
+[eva:alarm] basic.i:21: Warning: signed overflow. assert -2147483648 ≤ i - 1;
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======

tests/saveload/oracle/basic_sav.res

@@ -4,9 +4,9 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] basic.i:18: assertion got status valid.
-[eva] basic.i:19: starting to merge loop iterations
-[eva:alarm] basic.i:19: Warning: signed overflow. assert -2147483648 ≤ i - 1;
+[eva] basic.i:20: assertion got status valid.
+[eva] basic.i:21: starting to merge loop iterations
+[eva:alarm] basic.i:21: Warning: signed overflow. assert -2147483648 ≤ i - 1;
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======

tests/saveload/oracle/bool_sav.res

@@ -6,36 +6,36 @@
   x ∈ {0}
   y ∈ {0}
 [eva] computing for function f <- main.
-  Called from bool.c:25.
-[eva] bool.c:17: assertion got status valid.
-[eva] bool.c:18: starting to merge loop iterations
-[eva:alarm] bool.c:18: Warning: signed overflow. assert -2147483648 ≤ i - 1;
+  Called from bool.c:27.
+[eva] bool.c:19: assertion got status valid.
+[eva] bool.c:20: starting to merge loop iterations
+[eva:alarm] bool.c:20: Warning: signed overflow. assert -2147483648 ≤ i - 1;
 [eva] Recording results for f
 [eva] Done for function f
 [eva] computing for function printf_va_1 <- main.
-  Called from bool.c:27.
+  Called from bool.c:29.
 [eva] using specification for function printf_va_1
-[eva] bool.c:27: function printf_va_1: precondition got status valid.
+[eva] bool.c:29: function printf_va_1: precondition got status valid.
 [eva] Done for function printf_va_1
 [eva] computing for function printf_va_2 <- main.
-  Called from bool.c:29.
+  Called from bool.c:31.
 [eva] using specification for function printf_va_2
-[eva] bool.c:29: function printf_va_2: precondition got status valid.
+[eva] bool.c:31: function printf_va_2: precondition got status valid.
 [eva] Done for function printf_va_2
 [eva] computing for function printf_va_3 <- main.
-  Called from bool.c:31.
+  Called from bool.c:33.
 [eva] using specification for function printf_va_3
-[eva] bool.c:31: function printf_va_3: precondition got status valid.
+[eva] bool.c:33: function printf_va_3: precondition got status valid.
 [eva] Done for function printf_va_3
 [eva] computing for function printf_va_4 <- main.
-  Called from bool.c:33.
+  Called from bool.c:35.
 [eva] using specification for function printf_va_4
-[eva] bool.c:33: function printf_va_4: precondition got status valid.
+[eva] bool.c:35: function printf_va_4: precondition got status valid.
 [eva] Done for function printf_va_4
 [eva] computing for function printf_va_5 <- main.
-  Called from bool.c:35.
+  Called from bool.c:37.
 [eva] using specification for function printf_va_5
-[eva] bool.c:35: function printf_va_5: precondition got status valid.
+[eva] bool.c:37: function printf_va_5: precondition got status valid.
 [eva] Done for function printf_va_5
 [eva] Recording results for main
 [eva] done for function main

tests/saveload/oracle/callbacks.res.oracle

@@ -6,9 +6,9 @@
   x ∈ {0}
   y ∈ {0}
 [eva] computing for function g1 <- main2.
-  Called from callbacks.i:30.
+  Called from callbacks.i:32.
 [eva] computing for function f <- g1 <- main2.
-  Called from callbacks.i:16.
+  Called from callbacks.i:18.
 [eva] Recording results for f
 [from] Computing for function f
 [from] Done for function f
@@ -18,9 +18,9 @@
 [from] Done for function g1
 [eva] Done for function g1
 [eva] computing for function g2 <- main2.
-  Called from callbacks.i:31.
+  Called from callbacks.i:33.
 [eva] computing for function f <- g2 <- main2.
-  Called from callbacks.i:21.
+  Called from callbacks.i:23.
 [eva] Recording results for f
 [from] Computing for function f
 [from] Done for function f
@@ -34,13 +34,13 @@
 [from] Done for function main2
 [eva] done for function main2
 [from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to f at callbacks.i:16 (by g1):
+[from] call to f at callbacks.i:18 (by g1):
   x FROM p
-[from] call to f at callbacks.i:21 (by g2):
+[from] call to f at callbacks.i:23 (by g2):
   y FROM p
-[from] call to g1 at callbacks.i:30 (by main2):
+[from] call to g1 at callbacks.i:32 (by main2):
   x FROM \nothing
-[from] call to g2 at callbacks.i:31 (by main2):
+[from] call to g2 at callbacks.i:33 (by main2):
   y FROM \nothing
 [from] entry point:
   x FROM \nothing
@@ -61,9 +61,9 @@
   x ∈ {0}
   y ∈ {0}
 [eva] computing for function g1 <- main3.
-  Called from callbacks.i:35.
+  Called from callbacks.i:37.
 [eva] computing for function f <- g1 <- main3.
-  Called from callbacks.i:16.
+  Called from callbacks.i:18.
 [eva] Recording results for f
 [from] Computing for function f
 [from] Done for function f
@@ -73,9 +73,9 @@
 [from] Done for function g1
 [eva] Done for function g1
 [eva] computing for function g2 <- main3.
-  Called from callbacks.i:36.
+  Called from callbacks.i:38.
 [eva] computing for function f <- g2 <- main3.
-  Called from callbacks.i:21.
+  Called from callbacks.i:23.
 [eva] Recording results for f
 [from] Computing for function f
 [from] Done for function f
@@ -89,13 +89,13 @@
 [from] Done for function main3
 [eva] done for function main3
 [from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to f at callbacks.i:16 (by g1):
+[from] call to f at callbacks.i:18 (by g1):
   x FROM p
-[from] call to f at callbacks.i:21 (by g2):
+[from] call to f at callbacks.i:23 (by g2):
   y FROM p
-[from] call to g1 at callbacks.i:35 (by main3):
+[from] call to g1 at callbacks.i:37 (by main3):
   x FROM \nothing
-[from] call to g2 at callbacks.i:36 (by main3):
+[from] call to g2 at callbacks.i:38 (by main3):
   y FROM \nothing
 [from] entry point:
   x FROM \nothing

tests/saveload/oracle/callbacks_sav.res

@@ -6,9 +6,9 @@
   x ∈ {0}
   y ∈ {0}
 [eva] computing for function g1 <- main1.
-  Called from callbacks.i:25.
+  Called from callbacks.i:27.
 [eva] computing for function f <- g1 <- main1.
-  Called from callbacks.i:16.
+  Called from callbacks.i:18.
 [eva] Recording results for f
 [from] Computing for function f
 [from] Done for function f
@@ -18,9 +18,9 @@
 [from] Done for function g1
 [eva] Done for function g1
 [eva] computing for function g2 <- main1.
-  Called from callbacks.i:26.
+  Called from callbacks.i:28.
 [eva] computing for function f <- g2 <- main1.
-  Called from callbacks.i:21.
+  Called from callbacks.i:23.
 [eva] Recording results for f
 [from] Computing for function f
 [from] Done for function f
@@ -45,13 +45,13 @@
   No logical properties have been reached by the analysis.
   ----------------------------------------------------------------------------
 [from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to f at callbacks.i:16 (by g1):
+[from] call to f at callbacks.i:18 (by g1):
   x FROM p
-[from] call to f at callbacks.i:21 (by g2):
+[from] call to f at callbacks.i:23 (by g2):
   y FROM p
-[from] call to g1 at callbacks.i:25 (by main1):
+[from] call to g1 at callbacks.i:27 (by main1):
   x FROM \nothing
-[from] call to g2 at callbacks.i:26 (by main1):
+[from] call to g2 at callbacks.i:28 (by main1):
   y FROM \nothing
 [from] entry point:
   x FROM \nothing

tests/saveload/oracle/deps_sav.res

@@ -4,8 +4,8 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] deps.i:19: starting to merge loop iterations
-[eva:alarm] deps.i:19: Warning: signed overflow. assert -2147483648 ≤ i - 1;
+[eva] deps.i:21: starting to merge loop iterations
+[eva:alarm] deps.i:21: Warning: signed overflow. assert -2147483648 ≤ i - 1;
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======