[cst folding] required by dune tests

tests/constant_propagation/array_pointers.i

 /* run.config
-   STDOPT: +"-eva"
+   STDOPT: #"-eva"
 */
 
 void *p;

tests/constant_propagation/const_field_return_struct.i

 /* run.config
-   STDOPT: +"-eva"
+   STDOPT: #"-eva"
 */
 
 struct S {

tests/constant_propagation/const_globals.c

 /* run.config
+   PLUGIN:
    OPT: -constfold -print -machdep x86_32
 */
-
 #include <stddef.h>
 
 typedef const size_t const_size_t;

tests/constant_propagation/const_propagate.c

 /* run.config
-PLUGIN: @CONSTANT_PROPAGATION_PLUGINS@ from inout
-   OPT: -eva @EVA_OPTIONS@ -deps -out -input -scf
+   OPT: -eva @EVA_OPTIONS@ -deps -out -input -then -scf
    OPT: -scf @EVA_OPTIONS@ -main init -cast-from-constant -semantic-const-fold add3
 */
+
 int x,y,z, TAB[10];
 struct st { int a, b ; } s1, s2;
 typedef struct st ST ;

tests/constant_propagation/declaration2.c

 /* run.config
-   OPT: -eva @EVA_OPTIONS@ -scf
+   OPT: -eva @EVA_OPTIONS@ -then -scf
 */
 
 void f(int *x) { (*x)++; }

tests/constant_propagation/introduction_of_non_explicit_cast.c

 /* run.config
-   MODULE: @PTEST_NAME@
+ MODULE: @PTEST_NAME@
    OPT: -eva @EVA_OPTIONS@ -deps
 */
 
+
 int x,y,z;
 int TAB[10];
 struct st { int a, b ; } s1, s2;

tests/constant_propagation/oracle/const_propagate.0.res.oracle

@@ -128,6 +128,107 @@
   p ∈ {{ &x }}
   q ∈ {{ &x ; &y }}
   yy ∈ {7}
+[from] Computing for function add3
+[from] Done for function add3
+[from] Computing for function init
+[from] Done for function init
+[from] Computing for function test_float_double
+[from] Done for function test_float_double
+[from] Computing for function test_ptr
+[from] Done for function test_ptr
+[from] Computing for function test_struct
+[from] Done for function test_struct
+[from] Computing for function test_struct_ptr
+[from] Done for function test_struct_ptr
+[from] Computing for function test_tab
+[from] Done for function test_tab
+[from] Computing for function test_ull
+[from] Done for function test_ull
+[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 add3:
+  \result FROM v1; v2; v3
+[from] Function init:
+  x FROM v
+  y FROM \nothing
+  z FROM v
+  \result FROM \nothing
+[from] Function test_float_double:
+  f1 FROM f0
+  f2 FROM f0
+  f3 FROM f0
+  d1 FROM d0
+  d2 FROM d0
+  d3 FROM d0
+[from] Function test_ptr:
+  x FROM v
+  \result FROM \nothing
+[from] Function test_struct:
+  s1 FROM \nothing
+  s2 FROM \nothing
+[from] Function test_struct_ptr:
+  \result FROM \nothing
+[from] Function test_tab:
+  TAB[1] FROM TAB[2]; s1.b; s2.b
+     [4..5] FROM v
+  s2.b FROM s2.b
+[from] Function test_ull:
+  ull FROM ull
+[from] Function main:
+  x FROM \nothing
+  y FROM \nothing
+  z FROM a
+  TAB[1] FROM TAB[2]
+     [4..5] FROM \nothing
+  s1 FROM \nothing
+  s2 FROM \nothing
+  ull FROM ull
+  f1 FROM f0
+  f2 FROM f0
+  f3 FROM f0
+  d1 FROM d0
+  d2 FROM d0
+  d3 FROM d0
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function add3:
+    __retres
+[inout] Inputs for function add3:
+    \nothing
+[inout] Out (internal) for function init:
+    x; y; z; zero; sept; z1
+[inout] Inputs for function init:
+    x; y; z
+[inout] Out (internal) for function test_float_double:
+    f1; f2; f3; d1; d2; d3
+[inout] Inputs for function test_float_double:
+    f0; f1; f2; d0; d1; d2
+[inout] Out (internal) for function test_ptr:
+    x; p; s; decal; __retres
+[inout] Inputs for function test_ptr:
+    \nothing
+[inout] Out (internal) for function test_struct:
+    s1; s2; s
+[inout] Inputs for function test_struct:
+    s1.a
+[inout] Out (internal) for function test_struct_ptr:
+    q; __retres
+[inout] Inputs for function test_struct_ptr:
+    \nothing
+[inout] Out (internal) for function test_tab:
+    TAB{[1]; [4..5]}; s2.b; r; q; decal
+[inout] Inputs for function test_tab:
+    TAB[2]; s1.b; s2.b
+[inout] Out (internal) for function test_ull:
+    ull
+[inout] Inputs for function test_ull:
+    ull
+[inout] Out (internal) for function main:
+    x; y; z; TAB{[1]; [4..5]}; s1; s2; ull; f1; f2; f3; d1; d2; d3; b; 
+    p; q; tmp_1; yy
+[inout] Inputs for function main:
+    x; y; z; TAB[2]; s1; s2.b; ull; f0; f1; f2; d0; d1; d2
 [scf] beginning constant propagation
 /* Generated by Frama-C */
 struct st {
@@ -257,104 +358,3 @@ void main(int a)
 
 
 [scf] constant propagation done
-[from] Computing for function add3
-[from] Done for function add3
-[from] Computing for function init
-[from] Done for function init
-[from] Computing for function test_float_double
-[from] Done for function test_float_double
-[from] Computing for function test_ptr
-[from] Done for function test_ptr
-[from] Computing for function test_struct
-[from] Done for function test_struct
-[from] Computing for function test_struct_ptr
-[from] Done for function test_struct_ptr
-[from] Computing for function test_tab
-[from] Done for function test_tab
-[from] Computing for function test_ull
-[from] Done for function test_ull
-[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 add3:
-  \result FROM v1; v2; v3
-[from] Function init:
-  x FROM v
-  y FROM \nothing
-  z FROM v
-  \result FROM \nothing
-[from] Function test_float_double:
-  f1 FROM f0
-  f2 FROM f0
-  f3 FROM f0
-  d1 FROM d0
-  d2 FROM d0
-  d3 FROM d0
-[from] Function test_ptr:
-  x FROM v
-  \result FROM \nothing
-[from] Function test_struct:
-  s1 FROM \nothing
-  s2 FROM \nothing
-[from] Function test_struct_ptr:
-  \result FROM \nothing
-[from] Function test_tab:
-  TAB[1] FROM TAB[2]; s1.b; s2.b
-     [4..5] FROM v
-  s2.b FROM s2.b
-[from] Function test_ull:
-  ull FROM ull
-[from] Function main:
-  x FROM \nothing
-  y FROM \nothing
-  z FROM a
-  TAB[1] FROM TAB[2]
-     [4..5] FROM \nothing
-  s1 FROM \nothing
-  s2 FROM \nothing
-  ull FROM ull
-  f1 FROM f0
-  f2 FROM f0
-  f3 FROM f0
-  d1 FROM d0
-  d2 FROM d0
-  d3 FROM d0
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function add3:
-    __retres
-[inout] Inputs for function add3:
-    \nothing
-[inout] Out (internal) for function init:
-    x; y; z; zero; sept; z1
-[inout] Inputs for function init:
-    x; y; z
-[inout] Out (internal) for function test_float_double:
-    f1; f2; f3; d1; d2; d3
-[inout] Inputs for function test_float_double:
-    f0; f1; f2; d0; d1; d2
-[inout] Out (internal) for function test_ptr:
-    x; p; s; decal; __retres
-[inout] Inputs for function test_ptr:
-    \nothing
-[inout] Out (internal) for function test_struct:
-    s1; s2; s
-[inout] Inputs for function test_struct:
-    s1.a
-[inout] Out (internal) for function test_struct_ptr:
-    q; __retres
-[inout] Inputs for function test_struct_ptr:
-    \nothing
-[inout] Out (internal) for function test_tab:
-    TAB{[1]; [4..5]}; s2.b; r; q; decal
-[inout] Inputs for function test_tab:
-    TAB[2]; s1.b; s2.b
-[inout] Out (internal) for function test_ull:
-    ull
-[inout] Inputs for function test_ull:
-    ull
-[inout] Out (internal) for function main:
-    x; y; z; TAB{[1]; [4..5]}; s1; s2; ull; f1; f2; f3; d1; d2; d3; b; 
-    p; q; tmp_1; yy
-[inout] Inputs for function main:
-    x; y; z; TAB[2]; s1; s2.b; ull; f0; f1; f2; d0; d1; d2

tests/constant_propagation/oracle/introduction_of_non_explicit_cast.res.oracle

@@ -11,41 +11,41 @@
   s2 ∈ {0}
   ull ∈ {0}
 [eva] computing for function test_ull <- main.
-  Called from introduction_of_non_explicit_cast.c:68.
+  Called from introduction_of_non_explicit_cast.c:69.
 [eva] Recording results for test_ull
 [eva] Done for function test_ull
 [eva] computing for function test_struct <- main.
-  Called from introduction_of_non_explicit_cast.c:69.
+  Called from introduction_of_non_explicit_cast.c:70.
 [eva] Recording results for test_struct
 [eva] Done for function test_struct
 [eva] computing for function test_struct_ptr <- main.
-  Called from introduction_of_non_explicit_cast.c:70.
+  Called from introduction_of_non_explicit_cast.c:71.
 [eva] Recording results for test_struct_ptr
 [eva] Done for function test_struct_ptr
 [eva] computing for function test_tab <- main.
-  Called from introduction_of_non_explicit_cast.c:71.
+  Called from introduction_of_non_explicit_cast.c:72.
 [eva] Recording results for test_tab
 [eva] Done for function test_tab
 [eva] computing for function init <- main.
-  Called from introduction_of_non_explicit_cast.c:73.
+  Called from introduction_of_non_explicit_cast.c:74.
 [eva] computing for function add3 <- init <- main.
-  Called from introduction_of_non_explicit_cast.c:57.
+  Called from introduction_of_non_explicit_cast.c:58.
 [eva] Recording results for add3
 [eva] Done for function add3
 [eva] Recording results for init
 [eva] Done for function init
 [eva] computing for function add3 <- main.
-  Called from introduction_of_non_explicit_cast.c:74.
+  Called from introduction_of_non_explicit_cast.c:75.
 [eva] Recording results for add3
 [eva] Done for function add3
 [eva] computing for function test_ptr <- main.
-  Called from introduction_of_non_explicit_cast.c:76.
+  Called from introduction_of_non_explicit_cast.c:77.
 [eva] Recording results for test_ptr
 [eva] Done for function test_ptr
-[eva] introduction_of_non_explicit_cast.c:77: assertion got status valid.
-[eva:alarm] introduction_of_non_explicit_cast.c:80: Warning: 
+[eva] introduction_of_non_explicit_cast.c:78: assertion got status valid.
+[eva:alarm] introduction_of_non_explicit_cast.c:81: Warning: 
   assertion got status unknown.
-[eva] introduction_of_non_explicit_cast.c:81: assertion got status valid.
+[eva] introduction_of_non_explicit_cast.c:82: assertion got status valid.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======

tests/constant_propagation/struct_field.i

 /* run.config
-   STDOPT: +"-eva"
+   STDOPT: #"-eva"
 */
 
 struct st {

tests/constant_propagation/test_config

-MACRO: CONSTANT_PROPAGATION_PLUGINS constant_propagation eva,scope
+MACRO: CONSTANT_PROPAGATION_PLUGINS constant_propagation @EVA_MAIN_PLUGINS@ from,inout
 PLUGIN: @CONSTANT_PROPAGATION_PLUGINS@
-OPT: -journal-disable -scf @EVA_OPTIONS@ -machdep x86_32
+OPT: @EVA_OPTIONS@ -machdep x86_32 -then -scf