diff --git a/tests/test_config b/tests/test_config
index d10b6975ccf781f27ec19ef63614d25799f44156..997a6c54b93356a25a034a6a18cc58a0b4769da0 100644
--- a/tests/test_config
+++ b/tests/test_config
@@ -1,4 +1,5 @@
-MACRO: EVA_PLUGINS from,inout,eva,scope,variadic
+MACRO: EVA_MAIN_PLUGINS eva,scope
+MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
 MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0
 MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
 MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
diff --git a/tests/test_config_apron b/tests/test_config_apron
index 411673ceafcafde7b9e20b8a40abe841a1cbd1a5..3da27e2a2ef973e561bf30f4da5b776a334d68bb 100644
--- a/tests/test_config_apron
+++ b/tests/test_config_apron
@@ -1,9 +1,13 @@
-MACRO: EVA_PLUGINS from,inout,eva,scope,variadic
+MACRO: EVA_MAIN_PLUGINS eva,scope
+MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
 MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains apron-octagon -eva-warn-key experimental=inactive
 MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
+MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
+
+MACRO: RTE_TEST -rte -no-warn-invalid-pointer
 
 # Compare the result with the oracle of the default config.
 FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
 
 PLUGIN: @EVA_PLUGINS@
-OPT: -eva @EVA_CONFIG@ -out -input -deps
+OPT: @EVA_TEST@
diff --git a/tests/test_config_bitwise b/tests/test_config_bitwise
index 19dd5d40c9f00151a44d21a20b5cb797d1c1fe6c..c234708a10793096e2773baa50cf00ba2696340c 100644
--- a/tests/test_config_bitwise
+++ b/tests/test_config_bitwise
@@ -1,8 +1,13 @@
-MACRO: EVA_PLUGINS from,inout,eva,scope,variadic
+MACRO: EVA_MAIN_PLUGINS eva,scope
+MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
 MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains bitwise
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
+MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
+
+MACRO: RTE_TEST -rte -no-warn-invalid-pointer
 
 # Compare the result with the oracle of the default config.
 FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
 
-OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
+PLUGIN: @EVA_PLUGINS@
+OPT: @EVA_TEST@
diff --git a/tests/test_config_equality b/tests/test_config_equality
index fff8c6fb43f010c4d22835dbf0a4e5c43f2a249f..b631fa9d65f22f66a0453dcd5a787f4f78255a64 100644
--- a/tests/test_config_equality
+++ b/tests/test_config_equality
@@ -1,9 +1,13 @@
-MACRO: EVA_PLUGINS from,inout,eva,scope,variadic
+MACRO: EVA_MAIN_PLUGINS eva,scope
+MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
 MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains equality
 MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
+MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
+
+MACRO: RTE_TEST -rte -no-warn-invalid-pointer
 
 # Compare the result with the oracle of the default config.
 FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
 
 PLUGIN: @EVA_PLUGINS@
-OPT: -eva @EVA_CONFIG@ -out -input -deps
+OPT: @EVA_TEST@
diff --git a/tests/test_config_gauges b/tests/test_config_gauges
index 37ea7dfeb18c677bbb3d58d199a4d7030cd5dcac..177f05dbccdf68c101fdc0a0d54c8e3a708c7705 100644
--- a/tests/test_config_gauges
+++ b/tests/test_config_gauges
@@ -1,9 +1,13 @@
-MACRO: EVA_PLUGINS from,inout,eva,scope,variadic
+MACRO: EVA_MAIN_PLUGINS eva,scope
+MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
 MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains gauges
 MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
+MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
+
+MACRO: RTE_TEST -rte -no-warn-invalid-pointer
 
 # Compare the result with the oracle of the default config.
 FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
 
 PLUGIN: @EVA_PLUGINS@
-OPT: -eva @EVA_CONFIG@ -out -input -deps
+OPT: @EVA_TEST@
diff --git a/tests/test_config_octagon b/tests/test_config_octagon
index a63c091418a391a00eee6a9f0bb681358a49d7c5..e72845bbe14aa428519172c4a1fdd9ee55a00af7 100644
--- a/tests/test_config_octagon
+++ b/tests/test_config_octagon
@@ -1,9 +1,13 @@
-MACRO: EVA_PLUGINS from,inout,eva,scope,variadic
+MACRO: EVA_MAIN_PLUGINS eva,scope
+MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
 MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-domains octagon
 MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
+MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
+
+MACRO: RTE_TEST -rte -no-warn-invalid-pointer
 
 # Compare the result with the oracle of the default config.
 FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
 
 PLUGIN: @EVA_PLUGINS@
-OPT: -eva @EVA_CONFIG@ -out -input -deps
+OPT: @EVA_TEST@
diff --git a/tests/test_config_symblocs b/tests/test_config_symblocs
index 3b082f3869cd61f8bb7baf1944ea34ca3eb2e66f..6910404f9a855d0e334e60a4f6cbbb83534a6a75 100644
--- a/tests/test_config_symblocs
+++ b/tests/test_config_symblocs
@@ -1,9 +1,13 @@
-MACRO: EVA_PLUGINS from,inout,eva,scope,variadic
+MACRO: EVA_MAIN_PLUGINS eva,scope
+MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
 MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains symbolic-locations
 MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
+MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
+
+MACRO: RTE_TEST -rte -no-warn-invalid-pointer
 
 # Compare the result with the oracle of the default config.
 FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
 
 PLUGIN: @EVA_PLUGINS@
-OPT: -eva @EVA_CONFIG@ -out -input -deps
+OPT: @EVA_TEST@
diff --git a/tests/value/ai_annot.i b/tests/value/ai_annot.i
index 16034a0e0f48ea1185d1aca2066ddbc5c08bdcde..8b344d612e4d1bf211d505a5113f6259abd0c35e 100644
--- a/tests/value/ai_annot.i
+++ b/tests/value/ai_annot.i
@@ -1,5 +1,5 @@
 /* run.config*
-   STDOPT: #"-load-module scope -scope-verbose 2 -eva-remove-redundant-alarms -eva-context-width 3"
+   STDOPT: #"-scope-verbose 2 -eva-remove-redundant-alarms -eva-context-width 3"
    */
 
 
diff --git a/tests/value/align_char_array.c b/tests/value/align_char_array.c
index de692f2f709f3533998e31d902afee308ad011df..7c62d4cef2dd1a3473b43222e7383e7cff08d27e 100644
--- a/tests/value/align_char_array.c
+++ b/tests/value/align_char_array.c
@@ -1,9 +1,9 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
+ PLUGIN: @EVA_MAIN_PLUGINS@ 
+   OPT: -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST"
 */
 
 
-
 #ifndef PTEST
 #include <stdio.h>
 #endif
diff --git a/tests/value/array_initializer.i b/tests/value/array_initializer.i
index 04029accd9cbbc52b82684a435bb807b5c29d50a..2b815ae1da68fe36d0e467584cbc8b3a664f5906 100644
--- a/tests/value/array_initializer.i
+++ b/tests/value/array_initializer.i
@@ -1,7 +1,7 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -then -eva-initialization-padding-globals maybe
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -then -eva-initialization-padding-globals maybe
 */
-
 int t[5] = { [2] = 3 };
 
 struct { char a; int t[5]; } s = { 'a' , { [2] = 3 } };
diff --git a/tests/value/array_zero_length.i b/tests/value/array_zero_length.i
index 98d5d3527c9c68817323dbc5cd45ac47a16e355a..567f1f654992ce400acdff528a1bfa1d78f754f2 100644
--- a/tests/value/array_zero_length.i
+++ b/tests/value/array_zero_length.i
@@ -1,10 +1,10 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -journal-disable -machdep gcc_x86_32
-   OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -journal-disable -machdep gcc_x86_32
+  PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -machdep gcc_x86_32
+   OPT: -eva @EVA_CONFIG@ -lib-entry -machdep gcc_x86_32
  EXIT: 1
-   OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -journal-disable
+   OPT: -eva @EVA_CONFIG@ -lib-entry
 */
-
 char T[];
 char U[0];
 char V[][2];
diff --git a/tests/value/base_addr_offset_block_length.i b/tests/value/base_addr_offset_block_length.i
index b3aad4d14b7a622e69f1e547cd8f84ef8434dfbd..b67eccb47f9ed40945fca405e35261fddf66262f 100644
--- a/tests/value/base_addr_offset_block_length.i
+++ b/tests/value/base_addr_offset_block_length.i
@@ -1,8 +1,8 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -eva-context-width 3 -then -eva-slevel 3
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -eva-context-width 3 -then -eva-slevel 3
 */
 
-
 int x, y;
 short z;
 
diff --git a/tests/value/big_lib_entry.i b/tests/value/big_lib_entry.i
index 0c2770eab0fefe3254629223350644dbbf8493e2..a6ee597b2fc58dc57ca2d6d79bb5201fc0769a78 100644
--- a/tests/value/big_lib_entry.i
+++ b/tests/value/big_lib_entry.i
@@ -1,7 +1,7 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -eva-context-width 4 -eva-initialization-padding-globals no
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -lib-entry -eva-context-width 4 -eva-initialization-padding-globals no
 */
-
 typedef struct {
   int f1;
   float f2;
diff --git a/tests/value/bitfield_longlong.c b/tests/value/bitfield_longlong.c
index c2bdb9d6234e025769ac59c269deac5d6f03ec7e..808dfad6cde7a637ad75c4769c626fbe16500ac5 100644
--- a/tests/value/bitfield_longlong.c
+++ b/tests/value/bitfield_longlong.c
@@ -1,15 +1,15 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -cpp-extra-args="-Dprintf=Frama_C_show_each" -journal-disable
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -cpp-extra-args="-Dprintf=Frama_C_show_each"
 */
 struct X50 {
  long long int z:50;
 } s50 = { 2 };
- 
+
 struct X10 {
  long long int z:10;
 } s10 = { 2 };
 
-
 struct U32 {
   unsigned long z:32;
 } u32 = { -1 };
diff --git a/tests/value/bts1306.i b/tests/value/bts1306.i
index 81f9cc8f329ead372748ebd5eea97821b99bc0bd..d9e1e351994fb153ec8df0fa999b6ddbf620cb32 100644
--- a/tests/value/bts1306.i
+++ b/tests/value/bts1306.i
@@ -1,5 +1,6 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module from,inout,eva -constfold -eva-slevel 0 -eva @EVA_CONFIG@ -print -then -eva-slevel 10 -eva -print
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -constfold -eva-slevel 0 -eva @EVA_CONFIG@ -print -then -eva-slevel 10 -eva -print
    */
 
 void g(double x) { double y= x*x; }
diff --git a/tests/value/case_analysis.i b/tests/value/case_analysis.i
index 40be501257b9f1b5edca5e3a305db685148deb04..52c07928dbf9094f9167ae7cfd158cfa245716f8 100644
--- a/tests/value/case_analysis.i
+++ b/tests/value/case_analysis.i
@@ -1,6 +1,6 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -eva-slevel 30 -journal-disable -float-normal
-
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -eva-slevel 30 -float-normal
 */
 
 int sq,s;
diff --git a/tests/value/cond_integer_cast_of_float.i b/tests/value/cond_integer_cast_of_float.i
index 9d1350ea671348d2759998a9ec5b3f9a2473455b..4d45148d1817638006da5620d1f0eb6c4561f7cc 100644
--- a/tests/value/cond_integer_cast_of_float.i
+++ b/tests/value/cond_integer_cast_of_float.i
@@ -1,9 +1,9 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -eva-no-results -then -float-hex -main mainbis
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -eva-no-results -then -float-hex -main mainbis
 */
 typedef double D;
 typedef float F;
-
 int b;
 extern F f1, f2, f3, f4;
 extern D d1, d2, d3;
diff --git a/tests/value/const_typedef.i b/tests/value/const_typedef.i
index a2a0a3544f0c7304e5a2073be6bde7d35663e549..3fbf8a4b93486e12f3ccfcf89e442b8a3c2dba62 100644
--- a/tests/value/const_typedef.i
+++ b/tests/value/const_typedef.i
@@ -1,7 +1,7 @@
 /* run.config*
-  OPT: -machdep x86_32 -no-autoload-plugins -load-module inout,eva -print -then -eva @EVA_CONFIG@ -lib-entry -no-print
+ PLUGIN: @EVA_MAIN_PLUGINS@
+  OPT: -machdep x86_32 -print -then -eva @EVA_CONFIG@ -lib-entry -no-print
 */
-
 typedef int INT[3][3];
 typedef int INT2[][3];
 typedef int INT3[2][7];
diff --git a/tests/value/constarraystructlibentry.i b/tests/value/constarraystructlibentry.i
index 96049bcde852de75c8e5efabe6c11fa5d73aca84..6d0f14ef2932f0caf465b4536d66985eaac15254 100644
--- a/tests/value/constarraystructlibentry.i
+++ b/tests/value/constarraystructlibentry.i
@@ -1,7 +1,7 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -eva-initialization-padding-globals yes -then -eva-initialization-padding-globals no
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -lib-entry -eva-initialization-padding-globals yes -then -eva-initialization-padding-globals no
 */
-
 const int t[] = { 1, 2, 3, 4, 5 } ;
 
 const int t2[3][3] = { 1, 2, 3, 4, 5, 6, 7, 8, 9 } ;
diff --git a/tests/value/context_free.i b/tests/value/context_free.i
index cfc75576d264513eebd2a2d2bd9c37be34ba7322..34acfece1658df804eb072aeab7fc753bc0069e2 100644
--- a/tests/value/context_free.i
+++ b/tests/value/context_free.i
@@ -1,6 +1,6 @@
 /* run.config*
-   
-   OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -main f -absolute-valid-range 0x200-0x199 -eva-msg-key initial-state -journal-disable
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -lib-entry -main f -absolute-valid-range 0x200-0x199 -eva-msg-key initial-state
 */
 
 
diff --git a/tests/value/dead_inout.i b/tests/value/dead_inout.i
index 8cf0b0271e64bd950206a33e0f67093c1e6bc6c2..ced55e90b8b19df22a5b83c9a3f5834d079c96b7 100644
--- a/tests/value/dead_inout.i
+++ b/tests/value/dead_inout.i
@@ -1,7 +1,7 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -out -input -inout -inout -main main_all
+PLUGIN: @EVA_MAIN_PLUGINS@ inout
+   OPT: @EVA_CONFIG@ -out -input -inout -inout -main main_all
  */
-
 // This tests a potential imprecision with the computation of input and outputs if one forgets to test that a statement is dead
 int a, b;
 
diff --git a/tests/value/dead_statuses.i b/tests/value/dead_statuses.i
index e3233596af7078ab4303cd8a1d5b829e58ce1299..2a64874e2dffe31b15dfeea7389604c00462cfa3 100644
--- a/tests/value/dead_statuses.i
+++ b/tests/value/dead_statuses.i
@@ -1,7 +1,7 @@
 /* run.config*
-   STDOPT: +"-load-module report -then -report"
+ PLUGIN: @PTEST_PLUGIN@ report
+   STDOPT: +"-then -report"
 */
-
 //@ requires \true; assigns \nothing;
 void f(void);
 
diff --git a/tests/value/disjoint_status.i b/tests/value/disjoint_status.i
index 8ef72525727bd2c35c83c549d7fdcc35ee0be4ad..82e2db2a5a2baca5b2db2d9113c45c12d0ec0227 100644
--- a/tests/value/disjoint_status.i
+++ b/tests/value/disjoint_status.i
@@ -1,7 +1,7 @@
 /* run.config*
-   STDOPT: +"-then -load-module report -report"
+ PLUGIN: @PTEST_PLUGIN@ report
+   STDOPT: +" -report"
 */
-
 int x;
 //@ requires ReqTrue: \true; ensures PostTrue: \true; // Test printing of ACSL names
 void f(unsigned int c, unsigned int d) {
diff --git a/tests/value/fptr.i b/tests/value/fptr.i
index 1984eed4eee5dec75c10c60b1c4faed1567d9852..0df6d85d2077a6f0d221c4db0d34beb2af5a60ae 100644
--- a/tests/value/fptr.i
+++ b/tests/value/fptr.i
@@ -1,7 +1,7 @@
 /* run.config*
-   
-   OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -journal-disable -then -deps -out
-   OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -main main_uninit -journal-disable -then -deps -out
+ PLUGIN: @EVA_MAIN_PLUGINS@ from,inout
+   OPT: -eva @EVA_CONFIG@ -then -deps -out
+   OPT: -eva @EVA_CONFIG@ -main main_uninit -then -deps -out
 */
 int R=77; volatile int v; int n;
 
diff --git a/tests/value/from_call.i b/tests/value/from_call.i
index c510dd876084aec37a27264ef03de9b99b79a65f..7e979f0b83d058231cb0c433e14b7f9528d06077 100644
--- a/tests/value/from_call.i
+++ b/tests/value/from_call.i
@@ -1,10 +1,10 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module from,inout,users,eva -calldeps -eva @EVA_CONFIG@ -journal-disable -users -then -input
-   OPT: -no-autoload-plugins -load-module from,eva @EVA_CONFIG@ -deps -show-indirect-deps -journal-disable
+  PLUGIN: @EVA_MAIN_PLUGINS@ from,users
+   OPT: -calldeps -eva @EVA_CONFIG@ -users -then -input
+  PLUGIN: @EVA_MAIN_PLUGINS@ from
+   OPT: @EVA_CONFIG@ -deps -show-indirect-deps
 */
-int a,b,c,d;
-int x,y,z,t;
-
+int a,b,c,d, x,y,z,t;
 int g(int w)
 {
   return w + t;
diff --git a/tests/value/global_bug.i b/tests/value/global_bug.i
index f6c48882b9efde40cfcfc601d9065935ae75a435..d3acbecbae02ff5b5570e403986fd6668a4664a6 100644
--- a/tests/value/global_bug.i
+++ b/tests/value/global_bug.i
@@ -1,9 +1,9 @@
 /* run.config*
-   STDOPT: +"-load-module report -then -report"
+ PLUGIN: @PTEST_PLUGIN@ report
+   STDOPT: +"-report"
 */
-
 int i = 1;
-int G[2] = 
+int G[2] =
   {99<<63, 1};
 int j = 2;
 
diff --git a/tests/value/ilevel.i b/tests/value/ilevel.i
index 9cb65bf87964896f8b7a5eb3a95918842bd296e8..30aaf6a78b8fe2795a46249604b5e0e6f7028aa7 100644
--- a/tests/value/ilevel.i
+++ b/tests/value/ilevel.i
@@ -1,10 +1,10 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module inout,slicing,sparecode,eva -eva @EVA_CONFIG@ -slice-return main -then-on "Slicing export" -eva -eva-ilevel 16 -eva-show-progress -then-on "default" -eva-ilevel 17 -then -eva-ilevel 48
+ PLUGIN: @EVA_MAIN_PLUGINS@ inout,slicing
+   OPT: -eva @EVA_CONFIG@ -slice-return main -then-on "Slicing export" -eva -eva-ilevel 16 -eva-show-progress -then-on "default" -eva-ilevel 17 -then -eva-ilevel 48
 */
 // Test in particular that ilevel is by-project, even though it is an ocaml ref
 volatile int v;
 int i, j, k, l;
-
 int main () {
   do { i = v; }
   while (! (0 <= i && i < 8));
diff --git a/tests/value/incorrect_reduce_expr.i b/tests/value/incorrect_reduce_expr.i
index 0c7f22f6219efabde4f3dfd99e6eb8e74a44315c..48f7f83e12fc2b2e59dddeea3657f57f1250dfca 100644
--- a/tests/value/incorrect_reduce_expr.i
+++ b/tests/value/incorrect_reduce_expr.i
@@ -1,7 +1,7 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -absolute-valid-range 32-36
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -absolute-valid-range 32-36
 */
-
 char t[5];
 int *p;
 int x;
diff --git a/tests/value/init_const_guard.i b/tests/value/init_const_guard.i
index d97dd6d96f88cf3e73d3d6fbdc432a0118ada978..517c8278b6173200f7c93d86dbd098e0451cde83 100644
--- a/tests/value/init_const_guard.i
+++ b/tests/value/init_const_guard.i
@@ -1,7 +1,7 @@
 /*run.config*
-  STDOPT: +"-load-module report -main f -report -then -main g -then -lib-entry -main f -then -main g"
+ PLUGIN: @PTEST_PLUGIN@ report
+  STDOPT: +"-main f -report -then -main g -then -lib-entry -main f -then -main g"
 */
-
 /** Same test exists in WP tests. Please keep synchronized */
 
 
diff --git a/tests/value/inout.i b/tests/value/inout.i
index 847c21c656a0509ef7a57d55b5b9ff60d53997f8..3dd92638e0edfb92381e1443e37e63507e33c560 100644
--- a/tests/value/inout.i
+++ b/tests/value/inout.i
@@ -1,10 +1,10 @@
 /* run.config*
-   
-   OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main inout_11_0 -journal-disable
-   OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main inout_11_3 -journal-disable
-   OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main never_terminate -journal-disable
-   OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main may_not_terminate -journal-disable
-   OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -deps -main call_may_not_terminate -journal-disable
+PLUGIN: @EVA_MAIN_PLUGINS@ from,inout
+   OPT: @EVA_CONFIG@ -inout -deps -main inout_11_0
+   OPT: @EVA_CONFIG@ -inout -deps -main inout_11_3
+   OPT: @EVA_CONFIG@ -inout -deps -main never_terminate
+   OPT: @EVA_CONFIG@ -inout -deps -main may_not_terminate
+   OPT: @EVA_CONFIG@ -inout -deps -main call_may_not_terminate
 */
 
 int Xt, Xs, Xs_I, Ys, Ys_I, Z, I;
diff --git a/tests/value/inout_formals.i b/tests/value/inout_formals.i
index 96883b0436b0ba18a4cf72be2e6d664b4aabe98e..0add77d5252956a8a21599a3c4b8a6bbe3dd07e7 100644
--- a/tests/value/inout_formals.i
+++ b/tests/value/inout_formals.i
@@ -1,8 +1,8 @@
 /*run.config*
-  OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -input-with-formals  -inout-with-formals
+PLUGIN: @EVA_MAIN_PLUGINS@ inout
+  OPT: @EVA_CONFIG@ -inout -input-with-formals -inout-with-formals
 */
 int x, y;
-
 void main(int * const i) {
     *i=0;
     Frama_C_show_each(i);
diff --git a/tests/value/inout_proto.i b/tests/value/inout_proto.i
index 977b1591fed06b16f136349a8e77f54120595216..5e573ee3abfce63cecbad2b3e2d869b15fbcc125 100644
--- a/tests/value/inout_proto.i
+++ b/tests/value/inout_proto.i
@@ -1,7 +1,7 @@
 /*run.config*
-  OPT: -no-autoload-plugins -load-module from,inout @EVA_CONFIG@ -inout -input-with-formals  -inout-with-formals -main main_main
+PLUGIN: @EVA_MAIN_PLUGINS@ inout
+  OPT: @EVA_CONFIG@ -inout -input-with-formals -inout-with-formals -main main_main
 */
-
 typedef unsigned char   BYTE;
 typedef  BYTE *     MESSAGE_ADDR_TYPE;
 
diff --git a/tests/value/limits.c b/tests/value/limits.c
index 965d689d1099207749cd4e1caab99964a83a2d44..c8da28460996b8f66fe42b398790ec7e020e570d 100644
--- a/tests/value/limits.c
+++ b/tests/value/limits.c
@@ -1,7 +1,7 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -warn-signed-overflow
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -warn-signed-overflow
 */
-
 #include <limits.h>
 
 int cl, cu, ucu;
diff --git a/tests/value/local_slevel.i b/tests/value/local_slevel.i
index f8a28e1829933eca449024a9d5c635fb03a98f24..d40c3caf0477abdabcdbefad413537242c25ce91 100644
--- a/tests/value/local_slevel.i
+++ b/tests/value/local_slevel.i
@@ -1,7 +1,7 @@
 /* run.config*
-   STDOPT: +" -load-module frama-c-constant_propagation -eva-slevel-function main2:100000 -print -then -scf -then-on propagated -eva -eva-show-progress -no-scf"
+ PLUGIN: @EVA_MAIN_PLUGINS@ constant_propagation
+   STDOPT: +" -eva-slevel-function main2:100000 -print -then -scf -then-on propagated -eva -eva-show-progress -no-scf"
 */
-
 int *p;
 
 void main1() {
diff --git a/tests/value/logic_ptr_cast.i b/tests/value/logic_ptr_cast.i
index 64eb43489d69f0c135df3a29dda3d8eee22bb6c2..9120beca2e45a6dd113f6207c27794a8c8c53bf4 100644
--- a/tests/value/logic_ptr_cast.i
+++ b/tests/value/logic_ptr_cast.i
@@ -1,9 +1,9 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -print -journal-disable -eva-no-results
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -print -eva-no-results
 */
 int *p;
 int t[90];
-
 int main(){
   p = (int*) (((unsigned long)t + 7) & ~7UL);
   /*@ assert p == (int*)t || p == (int*)((char*)t+1) || 
diff --git a/tests/value/loop_test.i b/tests/value/loop_test.i
index 6b1e166139c0aad1abf2f61f4b99233d4639dba5..4ada1eb53646ed306e8825c76a34488443b8e0fb 100644
--- a/tests/value/loop_test.i
+++ b/tests/value/loop_test.i
@@ -1,9 +1,9 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -main test_onzes -journal-disable
-   OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -main test_cent_onzes -journal-disable
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -main test_onzes
+   OPT: -eva @EVA_CONFIG@ -main test_cent_onzes
 */
 
-
 /***************** var CMP cste **********************/
 int onze_0 (void) {
   int onze; for (onze=1000; onze >= 12 ; onze--) ; return onze ;
diff --git a/tests/value/loop_wvar.i b/tests/value/loop_wvar.i
index 341e446a0ad758d60a6c278b8609dc472a3ccf8b..892c3948c3b14d244e7ff27e122adeb37a1ed8ad 100644
--- a/tests/value/loop_wvar.i
+++ b/tests/value/loop_wvar.i
@@ -1,11 +1,11 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module eva,inout -no-annot -eva @EVA_CONFIG@ -then -kernel-warn-key=annot-error=active -annot -eva -journal-disable
-   OPT: -no-autoload-plugins -load-module from,inout,eva -kernel-warn-key=annot-error=active -eva @EVA_CONFIG@ -main main3 -journal-disable
-   OPT: -no-autoload-plugins -load-module eva,inout -kernel-warn-key=annot-error=active -eva @EVA_CONFIG@ -main main_err1 -journal-disable
-   OPT: -no-autoload-plugins -load-module eva,inout -kernel-warn-key=annot-error=active -eva @EVA_CONFIG@ -main main_err2 -journal-disable
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -no-annot -eva @EVA_CONFIG@ -then -kernel-warn-key=annot-error=active -annot -eva
+   OPT: -kernel-warn-key=annot-error=active -eva @EVA_CONFIG@ -main main3
+   OPT: -kernel-warn-key=annot-error=active -eva @EVA_CONFIG@ -main main_err1
+   OPT: -kernel-warn-key=annot-error=active -eva @EVA_CONFIG@ -main main_err2
 */
 
-
 void main(void)
 { int n = 13;
   int i,j;
diff --git a/tests/value/loopinv.c b/tests/value/loopinv.c
index 65683a6dc3f2b34a56ba55b85401f73079b53371..eb9adc45a75296c5c516c511e6ce0252c68ba875 100644
--- a/tests/value/loopinv.c
+++ b/tests/value/loopinv.c
@@ -1,7 +1,7 @@
 /* run.config* 
-OPT: @EVA_CONFIG@ -no-autoload-plugins -load-module from,inout,eva,report -eva-slevel-function main2:20 -pp-annot -eva -then -report
+PLUGIN: @EVA_MAIN_PLUGINS@ report
+  OPT: @EVA_CONFIG@ -eva-slevel-function main2:20 -pp-annot -eva -then -report
 */
-
 /*@ requires valid: \valid(&t[0..s-1]);
     requires c: 1 <= c < s; */
 void init (int *t, int c, int s) {
diff --git a/tests/value/machdep.c b/tests/value/machdep.c
index b901879416538caefa4fafda266ad349c17d7790..4c9f8816313be40f88fb2cdc46bd03a566c966f2 100644
--- a/tests/value/machdep.c
+++ b/tests/value/machdep.c
@@ -1,7 +1,7 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST"  -journal-disable -then -machdep x86_64 -then -machdep x86_16
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST"  -then -machdep x86_64 -then -machdep x86_16
 */
-
 #ifndef PTEST
 #include <stdio.h>
 #endif
diff --git a/tests/value/nested_struct_init.i b/tests/value/nested_struct_init.i
index f73a3e08021154c466c6ed2c8201e05a41043ace..67dd151b1c9fe7f87847383b30ece376e769a718 100644
--- a/tests/value/nested_struct_init.i
+++ b/tests/value/nested_struct_init.i
@@ -1,5 +1,6 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -then -eva-initialization-padding-globals no -then -eva-initialization-padding-globals maybe -then -lib-entry -then -eva-initialization-padding-globals no -then -eva-initialization-padding-globals yes
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -then -eva-initialization-padding-globals no -then -eva-initialization-padding-globals maybe -then -lib-entry -then -eva-initialization-padding-globals no -then -eva-initialization-padding-globals yes
 */
 
 typedef signed char int8_t;
diff --git a/tests/value/oracle/bts1306.res.oracle b/tests/value/oracle/bts1306.res.oracle
index f0036f751b5313034ee6be275ecd516dc6b0d154..18c9b265a6ef92421ac67746730b375a87fc602f 100644
--- a/tests/value/oracle/bts1306.res.oracle
+++ b/tests/value/oracle/bts1306.res.oracle
@@ -5,8 +5,8 @@
 [eva:initial-state] Values of globals at initialization
   
 [eva] computing for function g <- main.
-  Called from tests/value/bts1306.i:9.
-[eva:alarm] tests/value/bts1306.i:5: Warning: 
+  Called from tests/value/bts1306.i:10.
+[eva:alarm] tests/value/bts1306.i:6: Warning: 
   non-finite double value. assert \is_finite(\mul_double(x, x));
 [eva] Recording results for g
 [eva] Done for function g
@@ -40,8 +40,8 @@ int main(double x)
 [eva:initial-state] Values of globals at initialization
   
 [eva] computing for function g <- main.
-  Called from tests/value/bts1306.i:9.
-[eva:alarm] tests/value/bts1306.i:5: Warning: 
+  Called from tests/value/bts1306.i:10.
+[eva:alarm] tests/value/bts1306.i:6: Warning: 
   non-finite double value. assert \is_finite(\mul_double(x, x));
 [eva] Recording results for g
 [eva] Done for function g
diff --git a/tests/value/oracle/pointer_comparison.0.res.oracle b/tests/value/oracle/pointer_comparison.0.res.oracle
index 0202337ff61b091c94af6196bc605e43313ef656..24cd0a1cf29cc72506aa30fe1232cf729b33430c 100644
--- a/tests/value/oracle/pointer_comparison.0.res.oracle
+++ b/tests/value/oracle/pointer_comparison.0.res.oracle
@@ -6,33 +6,33 @@
   x ∈ {0}
   y ∈ {0}
   p ∈ {0}
-[eva] tests/value/pointer_comparison.c:8: Frama_C_show_each_1t: {{ &x + {4} }}
-[eva:pointer-comparison] tests/value/pointer_comparison.c:10: 
+[eva] tests/value/pointer_comparison.c:13: Frama_C_show_each_1t: {{ &x + {4} }}
+[eva:pointer-comparison] tests/value/pointer_comparison.c:15: 
   invalid pointer comparison: invalid pointer(s)
-[eva] tests/value/pointer_comparison.c:10: Frama_C_show_each_2: {{ &x + {8} }}
-[eva:pointer-comparison] tests/value/pointer_comparison.c:12: 
+[eva] tests/value/pointer_comparison.c:15: Frama_C_show_each_2: {{ &x + {8} }}
+[eva:pointer-comparison] tests/value/pointer_comparison.c:17: 
   invalid pointer comparison: invalid pointer(s)
-[eva] tests/value/pointer_comparison.c:12: Frama_C_show_each_3: {{ &x + {12} }}
-[eva:pointer-comparison] tests/value/pointer_comparison.c:14: 
+[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_3: {{ &x + {12} }}
+[eva:pointer-comparison] tests/value/pointer_comparison.c:19: 
   invalid pointer comparison: invalid pointer(s)
-[eva] tests/value/pointer_comparison.c:14: Frama_C_show_each_4: {{ &x + {16} }}
-[eva:pointer-comparison] tests/value/pointer_comparison.c:16: 
+[eva] tests/value/pointer_comparison.c:19: Frama_C_show_each_4: {{ &x + {16} }}
+[eva:pointer-comparison] tests/value/pointer_comparison.c:21: 
   invalid pointer comparison: invalid pointer(s)
-[eva:alarm] tests/value/pointer_comparison.c:16: Warning: 
+[eva:alarm] tests/value/pointer_comparison.c:21: Warning: 
   pointer downcast. assert (unsigned int)p ≤ 2147483647;
-[eva:alarm] tests/value/pointer_comparison.c:16: Warning: 
+[eva:alarm] tests/value/pointer_comparison.c:21: Warning: 
   pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
-[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
-[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_5e: {{ &x + {16} }}
-[eva:pointer-comparison] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:21: Frama_C_show_each_5: {{ &x + {16} }}
+[eva] tests/value/pointer_comparison.c:22: Frama_C_show_each_5e: {{ &x + {16} }}
+[eva:pointer-comparison] tests/value/pointer_comparison.c:23: 
   invalid pointer comparison: invalid pointer(s)
-[eva] tests/value/pointer_comparison.c:18: Frama_C_show_each_6: {{ &x + {20} }}
-[eva] tests/value/pointer_comparison.c:18: starting to merge loop iterations
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: Frama_C_show_each_6: {{ &x + {20} }}
+[eva] tests/value/pointer_comparison.c:23: starting to merge loop iterations
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + {20; 24} }}
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + {20; 24; 28} }}
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + [20..--],0%4 }}
 [eva] Recording results for main
 [eva] done for function main
@@ -57,10 +57,10 @@
 --- Properties of Function 'main'
 --------------------------------------------------------------------------------
 
-[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 21)
             assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
             tried with Eva.
-[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 21)
             assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
             tried with Eva.
 
@@ -77,38 +77,38 @@
   x ∈ {0}
   y ∈ {0}
   p ∈ {0}
-[eva] tests/value/pointer_comparison.c:8: Frama_C_show_each_1t: {{ &x + {4} }}
-[eva:alarm] tests/value/pointer_comparison.c:10: Warning: 
+[eva] tests/value/pointer_comparison.c:13: Frama_C_show_each_1t: {{ &x + {4} }}
+[eva:alarm] tests/value/pointer_comparison.c:15: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)tmp_0, (void *)(&y));
   (tmp_0 from p++)
-[eva] tests/value/pointer_comparison.c:10: Frama_C_show_each_2: {{ &x + {8} }}
-[eva:alarm] tests/value/pointer_comparison.c:12: Warning: 
+[eva] tests/value/pointer_comparison.c:15: Frama_C_show_each_2: {{ &x + {8} }}
+[eva:alarm] tests/value/pointer_comparison.c:17: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)tmp_1, (void *)(&y));
   (tmp_1 from p++)
-[eva] tests/value/pointer_comparison.c:12: Frama_C_show_each_3: {{ &x + {12} }}
-[eva:alarm] tests/value/pointer_comparison.c:14: Warning: 
+[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_3: {{ &x + {12} }}
+[eva:alarm] tests/value/pointer_comparison.c:19: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)tmp_2, (void *)(&y));
   (tmp_2 from p++)
-[eva] tests/value/pointer_comparison.c:14: Frama_C_show_each_4: {{ &x + {16} }}
-[eva:alarm] tests/value/pointer_comparison.c:16: Warning: 
+[eva] tests/value/pointer_comparison.c:19: Frama_C_show_each_4: {{ &x + {16} }}
+[eva:alarm] tests/value/pointer_comparison.c:21: Warning: 
   pointer downcast. assert (unsigned int)p ≤ 2147483647;
-[eva:alarm] tests/value/pointer_comparison.c:16: Warning: 
+[eva:alarm] tests/value/pointer_comparison.c:21: Warning: 
   pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
-[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
-[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_5e: {{ &x + {16} }}
-[eva:alarm] tests/value/pointer_comparison.c:18: Warning: 
+[eva] tests/value/pointer_comparison.c:21: Frama_C_show_each_5: {{ &x + {16} }}
+[eva] tests/value/pointer_comparison.c:22: Frama_C_show_each_5e: {{ &x + {16} }}
+[eva:alarm] tests/value/pointer_comparison.c:23: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)tmp_3, (void *)(&y));
   (tmp_3 from p++)
-[eva] tests/value/pointer_comparison.c:18: Frama_C_show_each_6: {{ &x + {20} }}
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: Frama_C_show_each_6: {{ &x + {20} }}
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + {20; 24} }}
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + {20; 24; 28} }}
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + [20..--],0%4 }}
 [eva] Recording results for main
 [eva] done for function main
@@ -133,28 +133,28 @@
 --- Properties of Function 'main'
 --------------------------------------------------------------------------------
 
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 10)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 15)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)tmp_0, (void *)(&y));
             tried with Eva.
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 12)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 17)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)tmp_1, (void *)(&y));
             tried with Eva.
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 14)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 19)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)tmp_2, (void *)(&y));
             tried with Eva.
-[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 21)
             assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
             tried with Eva.
-[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 21)
             assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
             tried with Eva.
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 18)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 23)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)tmp_3, (void *)(&y));
@@ -173,41 +173,41 @@
   x ∈ {0}
   y ∈ {0}
   p ∈ {0}
-[eva] tests/value/pointer_comparison.c:8: Frama_C_show_each_1t: {{ &x + {4} }}
-[eva:alarm] tests/value/pointer_comparison.c:10: Warning: 
+[eva] tests/value/pointer_comparison.c:13: Frama_C_show_each_1t: {{ &x + {4} }}
+[eva:alarm] tests/value/pointer_comparison.c:15: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)tmp_0, (void *)(&y));
   (tmp_0 from p++)
-[eva] tests/value/pointer_comparison.c:10: Frama_C_show_each_2: {{ &x + {8} }}
-[eva:alarm] tests/value/pointer_comparison.c:12: Warning: 
+[eva] tests/value/pointer_comparison.c:15: Frama_C_show_each_2: {{ &x + {8} }}
+[eva:alarm] tests/value/pointer_comparison.c:17: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)tmp_1, (void *)(&y));
   (tmp_1 from p++)
-[eva] tests/value/pointer_comparison.c:12: Frama_C_show_each_3: {{ &x + {12} }}
-[eva:alarm] tests/value/pointer_comparison.c:14: Warning: 
+[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_3: {{ &x + {12} }}
+[eva:alarm] tests/value/pointer_comparison.c:19: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)tmp_2, (void *)(&y));
   (tmp_2 from p++)
-[eva] tests/value/pointer_comparison.c:14: Frama_C_show_each_4: {{ &x + {16} }}
-[eva:alarm] tests/value/pointer_comparison.c:16: Warning: 
+[eva] tests/value/pointer_comparison.c:19: Frama_C_show_each_4: {{ &x + {16} }}
+[eva:alarm] tests/value/pointer_comparison.c:21: Warning: 
   pointer downcast. assert (unsigned int)p ≤ 2147483647;
-[eva:alarm] tests/value/pointer_comparison.c:16: Warning: 
+[eva:alarm] tests/value/pointer_comparison.c:21: Warning: 
   pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
-[eva:alarm] tests/value/pointer_comparison.c:16: Warning: 
+[eva:alarm] tests/value/pointer_comparison.c:21: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)((int)p), (void *)((int)(&y)));
-[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
-[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_5e: {{ &x + {16} }}
-[eva:alarm] tests/value/pointer_comparison.c:18: Warning: 
+[eva] tests/value/pointer_comparison.c:21: Frama_C_show_each_5: {{ &x + {16} }}
+[eva] tests/value/pointer_comparison.c:22: Frama_C_show_each_5e: {{ &x + {16} }}
+[eva:alarm] tests/value/pointer_comparison.c:23: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)tmp_3, (void *)(&y));
   (tmp_3 from p++)
-[eva] tests/value/pointer_comparison.c:18: Frama_C_show_each_6: {{ &x + {20} }}
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: Frama_C_show_each_6: {{ &x + {20} }}
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + {20; 24} }}
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + {20; 24; 28} }}
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + [20..--],0%4 }}
 [eva] Recording results for main
 [eva] done for function main
@@ -232,33 +232,33 @@
 --- Properties of Function 'main'
 --------------------------------------------------------------------------------
 
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 10)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 15)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)tmp_0, (void *)(&y));
             tried with Eva.
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 12)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 17)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)tmp_1, (void *)(&y));
             tried with Eva.
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 14)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 19)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)tmp_2, (void *)(&y));
             tried with Eva.
-[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 21)
             assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
             tried with Eva.
-[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 21)
             assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
             tried with Eva.
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 16)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 21)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)((int)p), (void *)((int)(&y)));
             tried with Eva.
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 18)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 23)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)tmp_3, (void *)(&y));
diff --git a/tests/value/oracle/pointer_comparison.1.res.oracle b/tests/value/oracle/pointer_comparison.1.res.oracle
index 0f48c4ee7e0a0f10c28b128a2b8f6ccc00f590cf..eea1599b423fb16430d10dc2727bea261a1b9ce1 100644
--- a/tests/value/oracle/pointer_comparison.1.res.oracle
+++ b/tests/value/oracle/pointer_comparison.1.res.oracle
@@ -6,52 +6,52 @@
   x ∈ {0}
   y ∈ {0}
   p ∈ {0}
-[eva] tests/value/pointer_comparison.c:8: Frama_C_show_each_1t: {{ &x + {4} }}
-[eva:pointer-comparison] tests/value/pointer_comparison.c:10: 
+[eva] tests/value/pointer_comparison.c:13: Frama_C_show_each_1t: {{ &x + {4} }}
+[eva:pointer-comparison] tests/value/pointer_comparison.c:15: 
   invalid pointer comparison: invalid pointer(s)
-[eva:pointer-comparison] tests/value/pointer_comparison.c:10: 
+[eva:pointer-comparison] tests/value/pointer_comparison.c:15: 
   evaluating condition to {0; 1} instead of {0} because of UPCPA
-[eva] tests/value/pointer_comparison.c:10: Frama_C_show_each_2: {{ &x + {8} }}
-[eva:pointer-comparison] tests/value/pointer_comparison.c:10: 
+[eva] tests/value/pointer_comparison.c:15: Frama_C_show_each_2: {{ &x + {8} }}
+[eva:pointer-comparison] tests/value/pointer_comparison.c:15: 
   evaluating condition to {0; 1} instead of {1} because of UPCPA
-[eva] tests/value/pointer_comparison.c:11: Frama_C_show_each_2e: {{ &x + {8} }}
-[eva:pointer-comparison] tests/value/pointer_comparison.c:12: 
+[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_2e: {{ &x + {8} }}
+[eva:pointer-comparison] tests/value/pointer_comparison.c:17: 
   invalid pointer comparison: invalid pointer(s)
-[eva:pointer-comparison] tests/value/pointer_comparison.c:12: 
+[eva:pointer-comparison] tests/value/pointer_comparison.c:17: 
   evaluating condition to {0; 1} instead of {0} because of UPCPA
-[eva] tests/value/pointer_comparison.c:12: Frama_C_show_each_3: {{ &x + {12} }}
-[eva:pointer-comparison] tests/value/pointer_comparison.c:12: 
+[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_3: {{ &x + {12} }}
+[eva:pointer-comparison] tests/value/pointer_comparison.c:17: 
   evaluating condition to {0; 1} instead of {1} because of UPCPA
-[eva] tests/value/pointer_comparison.c:13: Frama_C_show_each_3e: {{ &x + {12} }}
-[eva:pointer-comparison] tests/value/pointer_comparison.c:14: 
+[eva] tests/value/pointer_comparison.c:18: Frama_C_show_each_3e: {{ &x + {12} }}
+[eva:pointer-comparison] tests/value/pointer_comparison.c:19: 
   invalid pointer comparison: invalid pointer(s)
-[eva:pointer-comparison] tests/value/pointer_comparison.c:14: 
+[eva:pointer-comparison] tests/value/pointer_comparison.c:19: 
   evaluating condition to {0; 1} instead of {0} because of UPCPA
-[eva] tests/value/pointer_comparison.c:14: Frama_C_show_each_4: {{ &x + {16} }}
-[eva:pointer-comparison] tests/value/pointer_comparison.c:14: 
+[eva] tests/value/pointer_comparison.c:19: Frama_C_show_each_4: {{ &x + {16} }}
+[eva:pointer-comparison] tests/value/pointer_comparison.c:19: 
   evaluating condition to {0; 1} instead of {1} because of UPCPA
-[eva] tests/value/pointer_comparison.c:15: Frama_C_show_each_4e: {{ &x + {16} }}
-[eva:pointer-comparison] tests/value/pointer_comparison.c:16: 
+[eva] tests/value/pointer_comparison.c:20: Frama_C_show_each_4e: {{ &x + {16} }}
+[eva:pointer-comparison] tests/value/pointer_comparison.c:21: 
   invalid pointer comparison: invalid pointer(s)
-[eva:alarm] tests/value/pointer_comparison.c:16: Warning: 
+[eva:alarm] tests/value/pointer_comparison.c:21: Warning: 
   pointer downcast. assert (unsigned int)p ≤ 2147483647;
-[eva:alarm] tests/value/pointer_comparison.c:16: Warning: 
+[eva:alarm] tests/value/pointer_comparison.c:21: Warning: 
   pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
-[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
-[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_5e: {{ &x + {16} }}
-[eva:pointer-comparison] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:21: Frama_C_show_each_5: {{ &x + {16} }}
+[eva] tests/value/pointer_comparison.c:22: Frama_C_show_each_5e: {{ &x + {16} }}
+[eva:pointer-comparison] tests/value/pointer_comparison.c:23: 
   invalid pointer comparison: invalid pointer(s)
-[eva:pointer-comparison] tests/value/pointer_comparison.c:18: 
+[eva:pointer-comparison] tests/value/pointer_comparison.c:23: 
   evaluating condition to {0; 1} instead of {0} because of UPCPA
-[eva] tests/value/pointer_comparison.c:18: Frama_C_show_each_6: {{ &x + {20} }}
-[eva] tests/value/pointer_comparison.c:18: starting to merge loop iterations
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: Frama_C_show_each_6: {{ &x + {20} }}
+[eva] tests/value/pointer_comparison.c:23: starting to merge loop iterations
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + {20; 24} }}
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + {20; 24; 28} }}
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + [20..--],0%4 }}
-[eva:pointer-comparison] tests/value/pointer_comparison.c:18: 
+[eva:pointer-comparison] tests/value/pointer_comparison.c:23: 
   evaluating condition to {0; 1} instead of {1} because of UPCPA
 [eva] Recording results for main
 [eva] done for function main
@@ -77,10 +77,10 @@
 --- Properties of Function 'main'
 --------------------------------------------------------------------------------
 
-[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 21)
             assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
             tried with Eva.
-[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 21)
             assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
             tried with Eva.
 
@@ -97,41 +97,41 @@
   x ∈ {0}
   y ∈ {0}
   p ∈ {0}
-[eva] tests/value/pointer_comparison.c:8: Frama_C_show_each_1t: {{ &x + {4} }}
-[eva:alarm] tests/value/pointer_comparison.c:10: Warning: 
+[eva] tests/value/pointer_comparison.c:13: Frama_C_show_each_1t: {{ &x + {4} }}
+[eva:alarm] tests/value/pointer_comparison.c:15: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)tmp_0, (void *)(&y));
   (tmp_0 from p++)
-[eva] tests/value/pointer_comparison.c:10: Frama_C_show_each_2: {{ &x + {8} }}
-[eva] tests/value/pointer_comparison.c:11: Frama_C_show_each_2e: {{ &x + {8} }}
-[eva:alarm] tests/value/pointer_comparison.c:12: Warning: 
+[eva] tests/value/pointer_comparison.c:15: Frama_C_show_each_2: {{ &x + {8} }}
+[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_2e: {{ &x + {8} }}
+[eva:alarm] tests/value/pointer_comparison.c:17: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)tmp_1, (void *)(&y));
   (tmp_1 from p++)
-[eva] tests/value/pointer_comparison.c:12: Frama_C_show_each_3: {{ &x + {12} }}
-[eva] tests/value/pointer_comparison.c:13: Frama_C_show_each_3e: {{ &x + {12} }}
-[eva:alarm] tests/value/pointer_comparison.c:14: Warning: 
+[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_3: {{ &x + {12} }}
+[eva] tests/value/pointer_comparison.c:18: Frama_C_show_each_3e: {{ &x + {12} }}
+[eva:alarm] tests/value/pointer_comparison.c:19: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)tmp_2, (void *)(&y));
   (tmp_2 from p++)
-[eva] tests/value/pointer_comparison.c:14: Frama_C_show_each_4: {{ &x + {16} }}
-[eva] tests/value/pointer_comparison.c:15: Frama_C_show_each_4e: {{ &x + {16} }}
-[eva:alarm] tests/value/pointer_comparison.c:16: Warning: 
+[eva] tests/value/pointer_comparison.c:19: Frama_C_show_each_4: {{ &x + {16} }}
+[eva] tests/value/pointer_comparison.c:20: Frama_C_show_each_4e: {{ &x + {16} }}
+[eva:alarm] tests/value/pointer_comparison.c:21: Warning: 
   pointer downcast. assert (unsigned int)p ≤ 2147483647;
-[eva:alarm] tests/value/pointer_comparison.c:16: Warning: 
+[eva:alarm] tests/value/pointer_comparison.c:21: Warning: 
   pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
-[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
-[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_5e: {{ &x + {16} }}
-[eva:alarm] tests/value/pointer_comparison.c:18: Warning: 
+[eva] tests/value/pointer_comparison.c:21: Frama_C_show_each_5: {{ &x + {16} }}
+[eva] tests/value/pointer_comparison.c:22: Frama_C_show_each_5e: {{ &x + {16} }}
+[eva:alarm] tests/value/pointer_comparison.c:23: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)tmp_3, (void *)(&y));
   (tmp_3 from p++)
-[eva] tests/value/pointer_comparison.c:18: Frama_C_show_each_6: {{ &x + {20} }}
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: Frama_C_show_each_6: {{ &x + {20} }}
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + {20; 24} }}
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + {20; 24; 28} }}
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + [20..--],0%4 }}
 [eva] Recording results for main
 [eva] done for function main
@@ -157,28 +157,28 @@
 --- Properties of Function 'main'
 --------------------------------------------------------------------------------
 
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 10)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 15)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)tmp_0, (void *)(&y));
             tried with Eva.
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 12)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 17)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)tmp_1, (void *)(&y));
             tried with Eva.
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 14)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 19)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)tmp_2, (void *)(&y));
             tried with Eva.
-[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 21)
             assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
             tried with Eva.
-[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 21)
             assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
             tried with Eva.
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 18)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 23)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)tmp_3, (void *)(&y));
@@ -197,44 +197,44 @@
   x ∈ {0}
   y ∈ {0}
   p ∈ {0}
-[eva] tests/value/pointer_comparison.c:8: Frama_C_show_each_1t: {{ &x + {4} }}
-[eva:alarm] tests/value/pointer_comparison.c:10: Warning: 
+[eva] tests/value/pointer_comparison.c:13: Frama_C_show_each_1t: {{ &x + {4} }}
+[eva:alarm] tests/value/pointer_comparison.c:15: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)tmp_0, (void *)(&y));
   (tmp_0 from p++)
-[eva] tests/value/pointer_comparison.c:10: Frama_C_show_each_2: {{ &x + {8} }}
-[eva] tests/value/pointer_comparison.c:11: Frama_C_show_each_2e: {{ &x + {8} }}
-[eva:alarm] tests/value/pointer_comparison.c:12: Warning: 
+[eva] tests/value/pointer_comparison.c:15: Frama_C_show_each_2: {{ &x + {8} }}
+[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_2e: {{ &x + {8} }}
+[eva:alarm] tests/value/pointer_comparison.c:17: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)tmp_1, (void *)(&y));
   (tmp_1 from p++)
-[eva] tests/value/pointer_comparison.c:12: Frama_C_show_each_3: {{ &x + {12} }}
-[eva] tests/value/pointer_comparison.c:13: Frama_C_show_each_3e: {{ &x + {12} }}
-[eva:alarm] tests/value/pointer_comparison.c:14: Warning: 
+[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_3: {{ &x + {12} }}
+[eva] tests/value/pointer_comparison.c:18: Frama_C_show_each_3e: {{ &x + {12} }}
+[eva:alarm] tests/value/pointer_comparison.c:19: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)tmp_2, (void *)(&y));
   (tmp_2 from p++)
-[eva] tests/value/pointer_comparison.c:14: Frama_C_show_each_4: {{ &x + {16} }}
-[eva] tests/value/pointer_comparison.c:15: Frama_C_show_each_4e: {{ &x + {16} }}
-[eva:alarm] tests/value/pointer_comparison.c:16: Warning: 
+[eva] tests/value/pointer_comparison.c:19: Frama_C_show_each_4: {{ &x + {16} }}
+[eva] tests/value/pointer_comparison.c:20: Frama_C_show_each_4e: {{ &x + {16} }}
+[eva:alarm] tests/value/pointer_comparison.c:21: Warning: 
   pointer downcast. assert (unsigned int)p ≤ 2147483647;
-[eva:alarm] tests/value/pointer_comparison.c:16: Warning: 
+[eva:alarm] tests/value/pointer_comparison.c:21: Warning: 
   pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
-[eva:alarm] tests/value/pointer_comparison.c:16: Warning: 
+[eva:alarm] tests/value/pointer_comparison.c:21: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)((int)p), (void *)((int)(&y)));
-[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
-[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_5e: {{ &x + {16} }}
-[eva:alarm] tests/value/pointer_comparison.c:18: Warning: 
+[eva] tests/value/pointer_comparison.c:21: Frama_C_show_each_5: {{ &x + {16} }}
+[eva] tests/value/pointer_comparison.c:22: Frama_C_show_each_5e: {{ &x + {16} }}
+[eva:alarm] tests/value/pointer_comparison.c:23: Warning: 
   pointer comparison.
   assert \pointer_comparable((void *)tmp_3, (void *)(&y));
   (tmp_3 from p++)
-[eva] tests/value/pointer_comparison.c:18: Frama_C_show_each_6: {{ &x + {20} }}
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: Frama_C_show_each_6: {{ &x + {20} }}
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + {20; 24} }}
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + {20; 24; 28} }}
-[eva] tests/value/pointer_comparison.c:18: 
+[eva] tests/value/pointer_comparison.c:23: 
   Frama_C_show_each_6: {{ &x + [20..--],0%4 }}
 [eva] Recording results for main
 [eva] done for function main
@@ -260,33 +260,33 @@
 --- Properties of Function 'main'
 --------------------------------------------------------------------------------
 
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 10)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 15)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)tmp_0, (void *)(&y));
             tried with Eva.
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 12)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 17)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)tmp_1, (void *)(&y));
             tried with Eva.
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 14)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 19)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)tmp_2, (void *)(&y));
             tried with Eva.
-[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 21)
             assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
             tried with Eva.
-[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+[    -    ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 21)
             assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
             tried with Eva.
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 16)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 21)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)((int)p), (void *)((int)(&y)));
             tried with Eva.
-[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 18)
+[    -    ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 23)
             assert
             Eva: ptr_comparison:
               \pointer_comparable((void *)tmp_3, (void *)(&y));
diff --git a/tests/value/oracle/split_return.0.res.oracle b/tests/value/oracle/split_return.0.res.oracle
index 3c39daac7720985d50738ccf8f1157084f82ae0b..fb3bbb75a4b91c8b751a094ff5dd0ff772496b0a 100644
--- a/tests/value/oracle/split_return.0.res.oracle
+++ b/tests/value/oracle/split_return.0.res.oracle
@@ -19,109 +19,109 @@
   v7 ∈ {0}
   rand ∈ [--..--]
 [eva] computing for function main1 <- main.
-  Called from tests/value/split_return.i:207.
+  Called from tests/value/split_return.i:209.
 [eva] computing for function init <- main1 <- main.
-  Called from tests/value/split_return.i:20.
+  Called from tests/value/split_return.i:22.
 [eva] using specification for function init
 [eva] Done for function init
 [eva] Recording results for main1
 [eva] Done for function main1
 [eva] computing for function main2 <- main.
-  Called from tests/value/split_return.i:208.
+  Called from tests/value/split_return.i:210.
 [eva] computing for function f2 <- main2 <- main.
-  Called from tests/value/split_return.i:51.
+  Called from tests/value/split_return.i:53.
 [eva] Recording results for f2
 [eva] Done for function f2
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
-[eva] tests/value/split_return.i:54: assertion got status valid.
-[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5; 7}, {5}
-[eva] tests/value/split_return.i:57: assertion got status valid.
+[eva] tests/value/split_return.i:54: Frama_C_show_each_f2: {0}, {0}
+[eva] tests/value/split_return.i:54: Frama_C_show_each_f2: {5; 7}, {5}
+[eva] tests/value/split_return.i:56: assertion got status valid.
+[eva] tests/value/split_return.i:58: Frama_C_show_each_f2_2: {5; 7}, {5}
+[eva] tests/value/split_return.i:59: assertion got status valid.
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] computing for function main3 <- main.
-  Called from tests/value/split_return.i:209.
+  Called from tests/value/split_return.i:211.
 [eva] computing for function f3 <- main3 <- main.
-  Called from tests/value/split_return.i:76.
-[eva] tests/value/split_return.i:72: cannot properly split on \result == -2
+  Called from tests/value/split_return.i:78.
+[eva] tests/value/split_return.i:74: cannot properly split on \result == -2
 [eva] Recording results for f3
 [eva] Done for function f3
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2; 7}, {0; 5}
-[eva:alarm] tests/value/split_return.i:79: Warning: 
-  assertion got status unknown.
+[eva] tests/value/split_return.i:79: Frama_C_show_each_f3: {-2; 7}, {0; 5}
 [eva:alarm] tests/value/split_return.i:81: Warning: 
   assertion got status unknown.
+[eva:alarm] tests/value/split_return.i:83: Warning: 
+  assertion got status unknown.
 [eva] Recording results for main3
 [eva] Done for function main3
 [eva] computing for function main4 <- main.
-  Called from tests/value/split_return.i:210.
+  Called from tests/value/split_return.i:212.
 [eva] computing for function f4 <- main4 <- main.
-  Called from tests/value/split_return.i:97.
+  Called from tests/value/split_return.i:99.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4; 7}, {0; 5}
-[eva:alarm] tests/value/split_return.i:100: Warning: 
-  assertion got status unknown.
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {4; 7}, {0; 5}
 [eva:alarm] tests/value/split_return.i:102: Warning: 
   assertion got status unknown.
+[eva:alarm] tests/value/split_return.i:104: Warning: 
+  assertion got status unknown.
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main5 <- main.
-  Called from tests/value/split_return.i:211.
+  Called from tests/value/split_return.i:213.
 [eva] computing for function f5 <- main5 <- main.
-  Called from tests/value/split_return.i:120.
+  Called from tests/value/split_return.i:122.
 [eva] Recording results for f5
 [eva] Done for function f5
-[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
-[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
-[eva] tests/value/split_return.i:123: assertion got status valid.
+[eva] tests/value/split_return.i:123: Frama_C_show_each_f5: {-2}, {0}
+[eva] tests/value/split_return.i:123: Frama_C_show_each_f5: {7}, {5}
 [eva] tests/value/split_return.i:125: assertion got status valid.
+[eva] tests/value/split_return.i:127: assertion got status valid.
 [eva] Recording results for main5
 [eva] Done for function main5
 [eva] computing for function main6 <- main.
-  Called from tests/value/split_return.i:212.
+  Called from tests/value/split_return.i:214.
 [eva] computing for function f6 <- main6 <- main.
-  Called from tests/value/split_return.i:138.
-[eva:alarm] tests/value/split_return.i:133: Warning: 
+  Called from tests/value/split_return.i:140.
+[eva:alarm] tests/value/split_return.i:135: Warning: 
   assertion got status unknown.
 [eva] Recording results for f6
 [eva] Done for function f6
 [eva] Recording results for main6
 [eva] Done for function main6
 [eva] computing for function main7 <- main.
-  Called from tests/value/split_return.i:213.
+  Called from tests/value/split_return.i:215.
 [eva] computing for function f7 <- main7 <- main.
-  Called from tests/value/split_return.i:151.
+  Called from tests/value/split_return.i:153.
 [eva] Recording results for f7
 [eva] Done for function f7
-[eva] tests/value/split_return.i:156: 
+[eva] tests/value/split_return.i:158: 
   Frama_C_show_each_NULL: {{ NULL ; &v }}, {0; 1}
 [eva] Recording results for main7
 [eva] Done for function main7
 [eva] computing for function main8 <- main.
-  Called from tests/value/split_return.i:214.
+  Called from tests/value/split_return.i:216.
 [eva] computing for function f8 <- main8 <- main.
-  Called from tests/value/split_return.i:174.
+  Called from tests/value/split_return.i:176.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:175: 
+[eva] tests/value/split_return.i:177: 
   Frama_C_show_each_then8: {-1; 4}, {{ NULL ; &x }}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main9 <- main.
-  Called from tests/value/split_return.i:215.
+  Called from tests/value/split_return.i:217.
 [eva] computing for function uninit <- main9 <- main.
-  Called from tests/value/split_return.i:202.
+  Called from tests/value/split_return.i:204.
 [eva] Recording results for uninit
 [eva] Done for function uninit
 [eva] computing for function escaping <- main9 <- main.
-  Called from tests/value/split_return.i:203.
-[eva:locals-escaping] tests/value/split_return.i:195: Warning: 
+  Called from tests/value/split_return.i:205.
+[eva:locals-escaping] tests/value/split_return.i:197: Warning: 
   locals {x} escaping the scope of a block of escaping through p
 [eva] Recording results for escaping
 [eva] Done for function escaping
 [eva] computing for function escaping <- main9 <- main.
-  Called from tests/value/split_return.i:203.
+  Called from tests/value/split_return.i:205.
 [eva] Recording results for escaping
 [eva] Done for function escaping
 [eva] Recording results for main9
@@ -363,13 +363,13 @@
 --- Properties of Function 'init'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Post-condition (file tests/value/split_return.i, line 15)
+[ Extern  ] Post-condition (file tests/value/split_return.i, line 17)
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file tests/value/split_return.i, line 13)
+[ Extern  ] Assigns (file tests/value/split_return.i, line 15)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file tests/value/split_return.i, line 13)
+[ Extern  ] Froms (file tests/value/split_return.i, line 15)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file tests/value/split_return.i, line 14)
+[ Extern  ] Froms (file tests/value/split_return.i, line 16)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -378,54 +378,54 @@
 --- Properties of Function 'main1'
 --------------------------------------------------------------------------------
 
-[  Dead   ] Assertion (file tests/value/split_return.i, line 30)
+[  Dead   ] Assertion (file tests/value/split_return.i, line 32)
             Locally valid, but unreachable.
             By Eva because:
-             - Unreachable program point (file tests/value/split_return.i, line 30)
-[Unreachable] Unreachable program point (file tests/value/split_return.i, line 30)
+             - Unreachable program point (file tests/value/split_return.i, line 32)
+[Unreachable] Unreachable program point (file tests/value/split_return.i, line 32)
             by Eva.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'main2'
 --------------------------------------------------------------------------------
 
-[  Valid  ] Assertion (file tests/value/split_return.i, line 54)
+[  Valid  ] Assertion (file tests/value/split_return.i, line 56)
             by Eva.
-[  Valid  ] Assertion (file tests/value/split_return.i, line 57)
+[  Valid  ] Assertion (file tests/value/split_return.i, line 59)
             by Eva.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'main3'
 --------------------------------------------------------------------------------
 
-[    -    ] Assertion (file tests/value/split_return.i, line 79)
-            tried with Eva.
 [    -    ] Assertion (file tests/value/split_return.i, line 81)
             tried with Eva.
+[    -    ] Assertion (file tests/value/split_return.i, line 83)
+            tried with Eva.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'main4'
 --------------------------------------------------------------------------------
 
-[    -    ] Assertion (file tests/value/split_return.i, line 100)
-            tried with Eva.
 [    -    ] Assertion (file tests/value/split_return.i, line 102)
             tried with Eva.
+[    -    ] Assertion (file tests/value/split_return.i, line 104)
+            tried with Eva.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'main5'
 --------------------------------------------------------------------------------
 
-[  Valid  ] Assertion (file tests/value/split_return.i, line 123)
-            by Eva.
 [  Valid  ] Assertion (file tests/value/split_return.i, line 125)
             by Eva.
+[  Valid  ] Assertion (file tests/value/split_return.i, line 127)
+            by Eva.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'f6'
 --------------------------------------------------------------------------------
 
-[    -    ] Assertion (file tests/value/split_return.i, line 133)
+[    -    ] Assertion (file tests/value/split_return.i, line 135)
             tried with Eva.
 
 --------------------------------------------------------------------------------
diff --git a/tests/value/oracle/split_return.1.res.oracle b/tests/value/oracle/split_return.1.res.oracle
index e161e8a21148dd6de625f47fd1cd8b0935903ee8..650987ca8d9790b7abac32b439ec5f5d470fd2e0 100644
--- a/tests/value/oracle/split_return.1.res.oracle
+++ b/tests/value/oracle/split_return.1.res.oracle
@@ -21,102 +21,102 @@
   v7 ∈ {0}
   rand ∈ [--..--]
 [eva] computing for function main1 <- main.
-  Called from tests/value/split_return.i:207.
+  Called from tests/value/split_return.i:209.
 [eva] computing for function init <- main1 <- main.
-  Called from tests/value/split_return.i:20.
+  Called from tests/value/split_return.i:22.
 [eva] using specification for function init
 [eva] Done for function init
 [eva] Recording results for main1
 [eva] Done for function main1
 [eva] computing for function main2 <- main.
-  Called from tests/value/split_return.i:208.
+  Called from tests/value/split_return.i:210.
 [eva] computing for function f2 <- main2 <- main.
-  Called from tests/value/split_return.i:51.
+  Called from tests/value/split_return.i:53.
 [eva] Recording results for f2
 [eva] Done for function f2
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
-[eva] tests/value/split_return.i:54: assertion got status valid.
-[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5; 7}, {5}
-[eva] tests/value/split_return.i:57: assertion got status valid.
+[eva] tests/value/split_return.i:54: Frama_C_show_each_f2: {0}, {0}
+[eva] tests/value/split_return.i:54: Frama_C_show_each_f2: {5; 7}, {5}
+[eva] tests/value/split_return.i:56: assertion got status valid.
+[eva] tests/value/split_return.i:58: Frama_C_show_each_f2_2: {5; 7}, {5}
+[eva] tests/value/split_return.i:59: assertion got status valid.
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] computing for function main3 <- main.
-  Called from tests/value/split_return.i:209.
+  Called from tests/value/split_return.i:211.
 [eva] computing for function f3 <- main3 <- main.
-  Called from tests/value/split_return.i:76.
+  Called from tests/value/split_return.i:78.
 [eva] Recording results for f3
 [eva] Done for function f3
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
-[eva] tests/value/split_return.i:79: assertion got status valid.
+[eva] tests/value/split_return.i:79: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:79: Frama_C_show_each_f3: {7}, {5}
 [eva] tests/value/split_return.i:81: assertion got status valid.
+[eva] tests/value/split_return.i:83: assertion got status valid.
 [eva] Recording results for main3
 [eva] Done for function main3
 [eva] computing for function main4 <- main.
-  Called from tests/value/split_return.i:210.
+  Called from tests/value/split_return.i:212.
 [eva] computing for function f4 <- main4 <- main.
-  Called from tests/value/split_return.i:97.
+  Called from tests/value/split_return.i:99.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
-[eva] tests/value/split_return.i:100: assertion got status valid.
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {7}, {5}
 [eva] tests/value/split_return.i:102: assertion got status valid.
+[eva] tests/value/split_return.i:104: assertion got status valid.
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main5 <- main.
-  Called from tests/value/split_return.i:211.
+  Called from tests/value/split_return.i:213.
 [eva] computing for function f5 <- main5 <- main.
-  Called from tests/value/split_return.i:120.
+  Called from tests/value/split_return.i:122.
 [eva] Recording results for f5
 [eva] Done for function f5
-[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
-[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
-[eva] tests/value/split_return.i:123: assertion got status valid.
+[eva] tests/value/split_return.i:123: Frama_C_show_each_f5: {-2}, {0}
+[eva] tests/value/split_return.i:123: Frama_C_show_each_f5: {7}, {5}
 [eva] tests/value/split_return.i:125: assertion got status valid.
+[eva] tests/value/split_return.i:127: assertion got status valid.
 [eva] Recording results for main5
 [eva] Done for function main5
 [eva] computing for function main6 <- main.
-  Called from tests/value/split_return.i:212.
+  Called from tests/value/split_return.i:214.
 [eva] computing for function f6 <- main6 <- main.
-  Called from tests/value/split_return.i:138.
-[eva:alarm] tests/value/split_return.i:133: Warning: 
+  Called from tests/value/split_return.i:140.
+[eva:alarm] tests/value/split_return.i:135: Warning: 
   assertion got status unknown.
-[eva] tests/value/split_return.i:134: cannot properly split on \result == 0
+[eva] tests/value/split_return.i:136: cannot properly split on \result == 0
 [eva] Recording results for f6
 [eva] Done for function f6
 [eva] Recording results for main6
 [eva] Done for function main6
 [eva] computing for function main7 <- main.
-  Called from tests/value/split_return.i:213.
+  Called from tests/value/split_return.i:215.
 [eva] computing for function f7 <- main7 <- main.
-  Called from tests/value/split_return.i:151.
+  Called from tests/value/split_return.i:153.
 [eva] Recording results for f7
 [eva] Done for function f7
-[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {0}, {0}
-[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {{ &v }}, {1}
+[eva] tests/value/split_return.i:158: Frama_C_show_each_NULL: {0}, {0}
+[eva] tests/value/split_return.i:158: Frama_C_show_each_NULL: {{ &v }}, {1}
 [eva] Recording results for main7
 [eva] Done for function main7
 [eva] computing for function main8 <- main.
-  Called from tests/value/split_return.i:214.
+  Called from tests/value/split_return.i:216.
 [eva] computing for function f8 <- main8 <- main.
-  Called from tests/value/split_return.i:174.
+  Called from tests/value/split_return.i:176.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {4}, {{ &x }}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main9 <- main.
-  Called from tests/value/split_return.i:215.
+  Called from tests/value/split_return.i:217.
 [eva] computing for function uninit <- main9 <- main.
-  Called from tests/value/split_return.i:202.
+  Called from tests/value/split_return.i:204.
 [eva] Recording results for uninit
 [eva] Done for function uninit
 [eva] computing for function escaping <- main9 <- main.
-  Called from tests/value/split_return.i:203.
-[eva:locals-escaping] tests/value/split_return.i:195: Warning: 
+  Called from tests/value/split_return.i:205.
+[eva:locals-escaping] tests/value/split_return.i:197: Warning: 
   locals {x} escaping the scope of a block of escaping through p
 [eva] Recording results for escaping
 [eva] Done for function escaping
@@ -359,13 +359,13 @@
 --- Properties of Function 'init'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Post-condition (file tests/value/split_return.i, line 15)
+[ Extern  ] Post-condition (file tests/value/split_return.i, line 17)
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file tests/value/split_return.i, line 13)
+[ Extern  ] Assigns (file tests/value/split_return.i, line 15)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file tests/value/split_return.i, line 13)
+[ Extern  ] Froms (file tests/value/split_return.i, line 15)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file tests/value/split_return.i, line 14)
+[ Extern  ] Froms (file tests/value/split_return.i, line 16)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -374,54 +374,54 @@
 --- Properties of Function 'main1'
 --------------------------------------------------------------------------------
 
-[  Dead   ] Assertion (file tests/value/split_return.i, line 30)
+[  Dead   ] Assertion (file tests/value/split_return.i, line 32)
             Locally valid, but unreachable.
             By Eva because:
-             - Unreachable program point (file tests/value/split_return.i, line 30)
-[Unreachable] Unreachable program point (file tests/value/split_return.i, line 30)
+             - Unreachable program point (file tests/value/split_return.i, line 32)
+[Unreachable] Unreachable program point (file tests/value/split_return.i, line 32)
             by Eva.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'main2'
 --------------------------------------------------------------------------------
 
-[  Valid  ] Assertion (file tests/value/split_return.i, line 54)
+[  Valid  ] Assertion (file tests/value/split_return.i, line 56)
             by Eva.
-[  Valid  ] Assertion (file tests/value/split_return.i, line 57)
+[  Valid  ] Assertion (file tests/value/split_return.i, line 59)
             by Eva.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'main3'
 --------------------------------------------------------------------------------
 
-[  Valid  ] Assertion (file tests/value/split_return.i, line 79)
-            by Eva.
 [  Valid  ] Assertion (file tests/value/split_return.i, line 81)
             by Eva.
+[  Valid  ] Assertion (file tests/value/split_return.i, line 83)
+            by Eva.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'main4'
 --------------------------------------------------------------------------------
 
-[  Valid  ] Assertion (file tests/value/split_return.i, line 100)
-            by Eva.
 [  Valid  ] Assertion (file tests/value/split_return.i, line 102)
             by Eva.
+[  Valid  ] Assertion (file tests/value/split_return.i, line 104)
+            by Eva.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'main5'
 --------------------------------------------------------------------------------
 
-[  Valid  ] Assertion (file tests/value/split_return.i, line 123)
-            by Eva.
 [  Valid  ] Assertion (file tests/value/split_return.i, line 125)
             by Eva.
+[  Valid  ] Assertion (file tests/value/split_return.i, line 127)
+            by Eva.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'f6'
 --------------------------------------------------------------------------------
 
-[    -    ] Assertion (file tests/value/split_return.i, line 133)
+[    -    ] Assertion (file tests/value/split_return.i, line 135)
             tried with Eva.
 
 --------------------------------------------------------------------------------
diff --git a/tests/value/oracle/split_return.3.res.oracle b/tests/value/oracle/split_return.3.res.oracle
index 0efcd2430ce9e8239d2ac44023a3a3c42f36a4b1..47b6e1be4a8e3289d2173b14a8477a64e24164ff 100644
--- a/tests/value/oracle/split_return.3.res.oracle
+++ b/tests/value/oracle/split_return.3.res.oracle
@@ -13,196 +13,196 @@
   v7 ∈ {0}
   rand ∈ [--..--]
 [eva] computing for function main1 <- main.
-  Called from tests/value/split_return.i:207.
+  Called from tests/value/split_return.i:209.
 [eva] computing for function init <- main1 <- main.
-  Called from tests/value/split_return.i:20.
+  Called from tests/value/split_return.i:22.
 [eva] using specification for function init
 [eva] Done for function init
 [eva] Recording results for main1
 [eva] Done for function main1
 [eva] computing for function main2 <- main.
-  Called from tests/value/split_return.i:208.
+  Called from tests/value/split_return.i:210.
 [eva] computing for function f2 <- main2 <- main.
-  Called from tests/value/split_return.i:51.
+  Called from tests/value/split_return.i:53.
 [eva] Recording results for f2
 [eva] Done for function f2
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5}, {5}
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {7}, {5}
-[eva] tests/value/split_return.i:54: assertion got status valid.
-[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5}, {5}
-[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {7}, {5}
-[eva] tests/value/split_return.i:57: assertion got status valid.
+[eva] tests/value/split_return.i:54: Frama_C_show_each_f2: {0}, {0}
+[eva] tests/value/split_return.i:54: Frama_C_show_each_f2: {5}, {5}
+[eva] tests/value/split_return.i:54: Frama_C_show_each_f2: {7}, {5}
+[eva] tests/value/split_return.i:56: assertion got status valid.
+[eva] tests/value/split_return.i:58: Frama_C_show_each_f2_2: {5}, {5}
+[eva] tests/value/split_return.i:58: Frama_C_show_each_f2_2: {7}, {5}
+[eva] tests/value/split_return.i:59: assertion got status valid.
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] computing for function main3 <- main.
-  Called from tests/value/split_return.i:209.
+  Called from tests/value/split_return.i:211.
 [eva] computing for function f3 <- main3 <- main.
-  Called from tests/value/split_return.i:76.
+  Called from tests/value/split_return.i:78.
 [eva] Recording results for f3
 [eva] Done for function f3
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
-[eva] tests/value/split_return.i:79: assertion got status valid.
+[eva] tests/value/split_return.i:79: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:79: Frama_C_show_each_f3: {-2}, {0}
 [eva] tests/value/split_return.i:81: assertion got status valid.
+[eva] tests/value/split_return.i:83: assertion got status valid.
 [eva] Recording results for main3
 [eva] Done for function main3
 [eva] computing for function main3 <- main.
-  Called from tests/value/split_return.i:209.
+  Called from tests/value/split_return.i:211.
 [eva] computing for function f3 <- main3 <- main.
-  Called from tests/value/split_return.i:76.
+  Called from tests/value/split_return.i:78.
 [eva] Recording results for f3
 [eva] Done for function f3
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:79: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:79: Frama_C_show_each_f3: {-2}, {0}
 [eva] Recording results for main3
 [eva] Done for function main3
 [eva] computing for function main4 <- main.
-  Called from tests/value/split_return.i:210.
+  Called from tests/value/split_return.i:212.
 [eva] computing for function f4 <- main4 <- main.
-  Called from tests/value/split_return.i:97.
+  Called from tests/value/split_return.i:99.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
-[eva] tests/value/split_return.i:100: assertion got status valid.
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {7}, {5}
 [eva] tests/value/split_return.i:102: assertion got status valid.
+[eva] tests/value/split_return.i:104: assertion got status valid.
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main4 <- main.
-  Called from tests/value/split_return.i:210.
+  Called from tests/value/split_return.i:212.
 [eva] computing for function f4 <- main4 <- main.
-  Called from tests/value/split_return.i:97.
+  Called from tests/value/split_return.i:99.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {7}, {5}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main4 <- main.
-  Called from tests/value/split_return.i:210.
+  Called from tests/value/split_return.i:212.
 [eva] computing for function f4 <- main4 <- main.
-  Called from tests/value/split_return.i:97.
+  Called from tests/value/split_return.i:99.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {7}, {5}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main4 <- main.
-  Called from tests/value/split_return.i:210.
+  Called from tests/value/split_return.i:212.
 [eva] computing for function f4 <- main4 <- main.
-  Called from tests/value/split_return.i:97.
+  Called from tests/value/split_return.i:99.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {7}, {5}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main5 <- main.
-  Called from tests/value/split_return.i:211.
+  Called from tests/value/split_return.i:213.
 [eva] computing for function f5 <- main5 <- main.
-  Called from tests/value/split_return.i:120.
+  Called from tests/value/split_return.i:122.
 [eva] Recording results for f5
 [eva] Done for function f5
-[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
-[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
-[eva] tests/value/split_return.i:123: assertion got status valid.
+[eva] tests/value/split_return.i:123: Frama_C_show_each_f5: {7}, {5}
+[eva] tests/value/split_return.i:123: Frama_C_show_each_f5: {-2}, {0}
 [eva] tests/value/split_return.i:125: assertion got status valid.
+[eva] tests/value/split_return.i:127: assertion got status valid.
 [eva] Recording results for main5
 [eva] Done for function main5
 [eva] computing for function main6 <- main.
-  Called from tests/value/split_return.i:212.
+  Called from tests/value/split_return.i:214.
 [eva] computing for function f6 <- main6 <- main.
-  Called from tests/value/split_return.i:138.
-[eva:alarm] tests/value/split_return.i:133: Warning: 
+  Called from tests/value/split_return.i:140.
+[eva:alarm] tests/value/split_return.i:135: Warning: 
   assertion got status unknown.
 [eva] Recording results for f6
 [eva] Done for function f6
 [eva] Recording results for main6
 [eva] Done for function main6
 [eva] computing for function main6 <- main.
-  Called from tests/value/split_return.i:212.
+  Called from tests/value/split_return.i:214.
 [eva] computing for function f6 <- main6 <- main.
-  Called from tests/value/split_return.i:138.
+  Called from tests/value/split_return.i:140.
 [eva] Recording results for f6
 [eva] Done for function f6
 [eva] Recording results for main6
 [eva] Done for function main6
 [eva] computing for function main7 <- main.
-  Called from tests/value/split_return.i:213.
+  Called from tests/value/split_return.i:215.
 [eva] computing for function f7 <- main7 <- main.
-  Called from tests/value/split_return.i:151.
+  Called from tests/value/split_return.i:153.
 [eva] Recording results for f7
 [eva] Done for function f7
-[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {0}, {0}
-[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {{ &v }}, {1}
+[eva] tests/value/split_return.i:158: Frama_C_show_each_NULL: {0}, {0}
+[eva] tests/value/split_return.i:158: Frama_C_show_each_NULL: {{ &v }}, {1}
 [eva] Recording results for main7
 [eva] Done for function main7
 [eva] computing for function main7 <- main.
-  Called from tests/value/split_return.i:213.
+  Called from tests/value/split_return.i:215.
 [eva] computing for function f7 <- main7 <- main.
-  Called from tests/value/split_return.i:151.
+  Called from tests/value/split_return.i:153.
 [eva] Recording results for f7
 [eva] Done for function f7
-[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {0}, {0}
-[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {{ &v }}, {1}
+[eva] tests/value/split_return.i:158: Frama_C_show_each_NULL: {0}, {0}
+[eva] tests/value/split_return.i:158: Frama_C_show_each_NULL: {{ &v }}, {1}
 [eva] Recording results for main7
 [eva] Done for function main7
 [eva] computing for function main8 <- main.
-  Called from tests/value/split_return.i:214.
+  Called from tests/value/split_return.i:216.
 [eva] computing for function f8 <- main8 <- main.
-  Called from tests/value/split_return.i:174.
+  Called from tests/value/split_return.i:176.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {-1}, {0}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
-  Called from tests/value/split_return.i:214.
+  Called from tests/value/split_return.i:216.
 [eva] computing for function f8 <- main8 <- main.
-  Called from tests/value/split_return.i:174.
+  Called from tests/value/split_return.i:176.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {-1}, {0}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
-  Called from tests/value/split_return.i:214.
+  Called from tests/value/split_return.i:216.
 [eva] computing for function f8 <- main8 <- main.
-  Called from tests/value/split_return.i:174.
+  Called from tests/value/split_return.i:176.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {-1}, {0}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
-  Called from tests/value/split_return.i:214.
+  Called from tests/value/split_return.i:216.
 [eva] computing for function f8 <- main8 <- main.
-  Called from tests/value/split_return.i:174.
+  Called from tests/value/split_return.i:176.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {-1}, {0}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main9 <- main.
-  Called from tests/value/split_return.i:215.
+  Called from tests/value/split_return.i:217.
 [eva] computing for function uninit <- main9 <- main.
-  Called from tests/value/split_return.i:202.
+  Called from tests/value/split_return.i:204.
 [eva] Recording results for uninit
 [eva] Done for function uninit
 [eva] computing for function escaping <- main9 <- main.
-  Called from tests/value/split_return.i:203.
-[eva:locals-escaping] tests/value/split_return.i:195: Warning: 
+  Called from tests/value/split_return.i:205.
+[eva:locals-escaping] tests/value/split_return.i:197: Warning: 
   locals {x} escaping the scope of a block of escaping through p
 [eva] Recording results for escaping
 [eva] Done for function escaping
 [eva] computing for function escaping <- main9 <- main.
-  Called from tests/value/split_return.i:203.
+  Called from tests/value/split_return.i:205.
 [eva] Recording results for escaping
 [eva] Done for function escaping
 [eva] Recording results for main9
diff --git a/tests/value/oracle/split_return.4.res.oracle b/tests/value/oracle/split_return.4.res.oracle
index 9751f1d714782c4f4f5c41324c7050e3690dd387..0951639034e140b1835d8a952ddc442c4622ef40 100644
--- a/tests/value/oracle/split_return.4.res.oracle
+++ b/tests/value/oracle/split_return.4.res.oracle
@@ -16,196 +16,196 @@
   v7 ∈ {0}
   rand ∈ [--..--]
 [eva] computing for function main1 <- main.
-  Called from tests/value/split_return.i:207.
+  Called from tests/value/split_return.i:209.
 [eva] computing for function init <- main1 <- main.
-  Called from tests/value/split_return.i:20.
+  Called from tests/value/split_return.i:22.
 [eva] using specification for function init
 [eva] Done for function init
 [eva] Recording results for main1
 [eva] Done for function main1
 [eva] computing for function main2 <- main.
-  Called from tests/value/split_return.i:208.
+  Called from tests/value/split_return.i:210.
 [eva] computing for function f2 <- main2 <- main.
-  Called from tests/value/split_return.i:51.
+  Called from tests/value/split_return.i:53.
 [eva] Recording results for f2
 [eva] Done for function f2
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5}, {5}
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {7}, {5}
-[eva] tests/value/split_return.i:54: assertion got status valid.
-[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5}, {5}
-[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {7}, {5}
-[eva] tests/value/split_return.i:57: assertion got status valid.
+[eva] tests/value/split_return.i:54: Frama_C_show_each_f2: {0}, {0}
+[eva] tests/value/split_return.i:54: Frama_C_show_each_f2: {5}, {5}
+[eva] tests/value/split_return.i:54: Frama_C_show_each_f2: {7}, {5}
+[eva] tests/value/split_return.i:56: assertion got status valid.
+[eva] tests/value/split_return.i:58: Frama_C_show_each_f2_2: {5}, {5}
+[eva] tests/value/split_return.i:58: Frama_C_show_each_f2_2: {7}, {5}
+[eva] tests/value/split_return.i:59: assertion got status valid.
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] computing for function main3 <- main.
-  Called from tests/value/split_return.i:209.
+  Called from tests/value/split_return.i:211.
 [eva] computing for function f3 <- main3 <- main.
-  Called from tests/value/split_return.i:76.
+  Called from tests/value/split_return.i:78.
 [eva] Recording results for f3
 [eva] Done for function f3
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
-[eva] tests/value/split_return.i:79: assertion got status valid.
+[eva] tests/value/split_return.i:79: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:79: Frama_C_show_each_f3: {-2}, {0}
 [eva] tests/value/split_return.i:81: assertion got status valid.
+[eva] tests/value/split_return.i:83: assertion got status valid.
 [eva] Recording results for main3
 [eva] Done for function main3
 [eva] computing for function main3 <- main.
-  Called from tests/value/split_return.i:209.
+  Called from tests/value/split_return.i:211.
 [eva] computing for function f3 <- main3 <- main.
-  Called from tests/value/split_return.i:76.
+  Called from tests/value/split_return.i:78.
 [eva] Recording results for f3
 [eva] Done for function f3
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:79: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:79: Frama_C_show_each_f3: {-2}, {0}
 [eva] Recording results for main3
 [eva] Done for function main3
 [eva] computing for function main4 <- main.
-  Called from tests/value/split_return.i:210.
+  Called from tests/value/split_return.i:212.
 [eva] computing for function f4 <- main4 <- main.
-  Called from tests/value/split_return.i:97.
+  Called from tests/value/split_return.i:99.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
-[eva] tests/value/split_return.i:100: assertion got status valid.
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {7}, {5}
 [eva] tests/value/split_return.i:102: assertion got status valid.
+[eva] tests/value/split_return.i:104: assertion got status valid.
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main4 <- main.
-  Called from tests/value/split_return.i:210.
+  Called from tests/value/split_return.i:212.
 [eva] computing for function f4 <- main4 <- main.
-  Called from tests/value/split_return.i:97.
+  Called from tests/value/split_return.i:99.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {7}, {5}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main4 <- main.
-  Called from tests/value/split_return.i:210.
+  Called from tests/value/split_return.i:212.
 [eva] computing for function f4 <- main4 <- main.
-  Called from tests/value/split_return.i:97.
+  Called from tests/value/split_return.i:99.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {7}, {5}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main4 <- main.
-  Called from tests/value/split_return.i:210.
+  Called from tests/value/split_return.i:212.
 [eva] computing for function f4 <- main4 <- main.
-  Called from tests/value/split_return.i:97.
+  Called from tests/value/split_return.i:99.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {7}, {5}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main5 <- main.
-  Called from tests/value/split_return.i:211.
+  Called from tests/value/split_return.i:213.
 [eva] computing for function f5 <- main5 <- main.
-  Called from tests/value/split_return.i:120.
+  Called from tests/value/split_return.i:122.
 [eva] Recording results for f5
 [eva] Done for function f5
-[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
-[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
-[eva] tests/value/split_return.i:123: assertion got status valid.
+[eva] tests/value/split_return.i:123: Frama_C_show_each_f5: {7}, {5}
+[eva] tests/value/split_return.i:123: Frama_C_show_each_f5: {-2}, {0}
 [eva] tests/value/split_return.i:125: assertion got status valid.
+[eva] tests/value/split_return.i:127: assertion got status valid.
 [eva] Recording results for main5
 [eva] Done for function main5
 [eva] computing for function main6 <- main.
-  Called from tests/value/split_return.i:212.
+  Called from tests/value/split_return.i:214.
 [eva] computing for function f6 <- main6 <- main.
-  Called from tests/value/split_return.i:138.
-[eva:alarm] tests/value/split_return.i:133: Warning: 
+  Called from tests/value/split_return.i:140.
+[eva:alarm] tests/value/split_return.i:135: Warning: 
   assertion got status unknown.
 [eva] Recording results for f6
 [eva] Done for function f6
 [eva] Recording results for main6
 [eva] Done for function main6
 [eva] computing for function main6 <- main.
-  Called from tests/value/split_return.i:212.
+  Called from tests/value/split_return.i:214.
 [eva] computing for function f6 <- main6 <- main.
-  Called from tests/value/split_return.i:138.
+  Called from tests/value/split_return.i:140.
 [eva] Recording results for f6
 [eva] Done for function f6
 [eva] Recording results for main6
 [eva] Done for function main6
 [eva] computing for function main7 <- main.
-  Called from tests/value/split_return.i:213.
+  Called from tests/value/split_return.i:215.
 [eva] computing for function f7 <- main7 <- main.
-  Called from tests/value/split_return.i:151.
+  Called from tests/value/split_return.i:153.
 [eva] Recording results for f7
 [eva] Done for function f7
-[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {0}, {0}
-[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {{ &v }}, {1}
+[eva] tests/value/split_return.i:158: Frama_C_show_each_NULL: {0}, {0}
+[eva] tests/value/split_return.i:158: Frama_C_show_each_NULL: {{ &v }}, {1}
 [eva] Recording results for main7
 [eva] Done for function main7
 [eva] computing for function main7 <- main.
-  Called from tests/value/split_return.i:213.
+  Called from tests/value/split_return.i:215.
 [eva] computing for function f7 <- main7 <- main.
-  Called from tests/value/split_return.i:151.
+  Called from tests/value/split_return.i:153.
 [eva] Recording results for f7
 [eva] Done for function f7
-[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {0}, {0}
-[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {{ &v }}, {1}
+[eva] tests/value/split_return.i:158: Frama_C_show_each_NULL: {0}, {0}
+[eva] tests/value/split_return.i:158: Frama_C_show_each_NULL: {{ &v }}, {1}
 [eva] Recording results for main7
 [eva] Done for function main7
 [eva] computing for function main8 <- main.
-  Called from tests/value/split_return.i:214.
+  Called from tests/value/split_return.i:216.
 [eva] computing for function f8 <- main8 <- main.
-  Called from tests/value/split_return.i:174.
+  Called from tests/value/split_return.i:176.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {-1}, {0}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
-  Called from tests/value/split_return.i:214.
+  Called from tests/value/split_return.i:216.
 [eva] computing for function f8 <- main8 <- main.
-  Called from tests/value/split_return.i:174.
+  Called from tests/value/split_return.i:176.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {-1}, {0}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
-  Called from tests/value/split_return.i:214.
+  Called from tests/value/split_return.i:216.
 [eva] computing for function f8 <- main8 <- main.
-  Called from tests/value/split_return.i:174.
+  Called from tests/value/split_return.i:176.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {-1}, {0}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
-  Called from tests/value/split_return.i:214.
+  Called from tests/value/split_return.i:216.
 [eva] computing for function f8 <- main8 <- main.
-  Called from tests/value/split_return.i:174.
+  Called from tests/value/split_return.i:176.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {-1}, {0}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main9 <- main.
-  Called from tests/value/split_return.i:215.
+  Called from tests/value/split_return.i:217.
 [eva] computing for function uninit <- main9 <- main.
-  Called from tests/value/split_return.i:202.
+  Called from tests/value/split_return.i:204.
 [eva] Recording results for uninit
 [eva] Done for function uninit
 [eva] computing for function escaping <- main9 <- main.
-  Called from tests/value/split_return.i:203.
-[eva:locals-escaping] tests/value/split_return.i:195: Warning: 
+  Called from tests/value/split_return.i:205.
+[eva:locals-escaping] tests/value/split_return.i:197: Warning: 
   locals {x} escaping the scope of a block of escaping through p
 [eva] Recording results for escaping
 [eva] Done for function escaping
 [eva] computing for function escaping <- main9 <- main.
-  Called from tests/value/split_return.i:203.
+  Called from tests/value/split_return.i:205.
 [eva] Recording results for escaping
 [eva] Done for function escaping
 [eva] Recording results for main9
@@ -460,181 +460,181 @@
   v7 ∈ {0}
   rand ∈ [--..--]
 [eva] computing for function main1 <- main.
-  Called from tests/value/split_return.i:207.
+  Called from tests/value/split_return.i:209.
 [eva] computing for function init <- main1 <- main.
-  Called from tests/value/split_return.i:20.
+  Called from tests/value/split_return.i:22.
 [eva] Done for function init
 [eva] Recording results for main1
 [eva] Done for function main1
 [eva] computing for function main2 <- main.
-  Called from tests/value/split_return.i:208.
+  Called from tests/value/split_return.i:210.
 [eva] computing for function f2 <- main2 <- main.
-  Called from tests/value/split_return.i:51.
+  Called from tests/value/split_return.i:53.
 [eva] Recording results for f2
 [eva] Done for function f2
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
-[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5; 7}, {5}
+[eva] tests/value/split_return.i:54: Frama_C_show_each_f2: {0}, {0}
+[eva] tests/value/split_return.i:54: Frama_C_show_each_f2: {5; 7}, {5}
+[eva] tests/value/split_return.i:58: Frama_C_show_each_f2_2: {5; 7}, {5}
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] computing for function main3 <- main.
-  Called from tests/value/split_return.i:209.
+  Called from tests/value/split_return.i:211.
 [eva] computing for function f3 <- main3 <- main.
-  Called from tests/value/split_return.i:76.
+  Called from tests/value/split_return.i:78.
 [eva] Recording results for f3
 [eva] Done for function f3
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:79: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:79: Frama_C_show_each_f3: {-2}, {0}
 [eva] Recording results for main3
 [eva] Done for function main3
 [eva] computing for function main3 <- main.
-  Called from tests/value/split_return.i:209.
+  Called from tests/value/split_return.i:211.
 [eva] computing for function f3 <- main3 <- main.
-  Called from tests/value/split_return.i:76.
+  Called from tests/value/split_return.i:78.
 [eva] Recording results for f3
 [eva] Done for function f3
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:79: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:79: Frama_C_show_each_f3: {-2}, {0}
 [eva] Recording results for main3
 [eva] Done for function main3
 [eva] computing for function main4 <- main.
-  Called from tests/value/split_return.i:210.
+  Called from tests/value/split_return.i:212.
 [eva] computing for function f4 <- main4 <- main.
-  Called from tests/value/split_return.i:97.
+  Called from tests/value/split_return.i:99.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {7}, {5}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main4 <- main.
-  Called from tests/value/split_return.i:210.
+  Called from tests/value/split_return.i:212.
 [eva] computing for function f4 <- main4 <- main.
-  Called from tests/value/split_return.i:97.
+  Called from tests/value/split_return.i:99.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {7}, {5}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main4 <- main.
-  Called from tests/value/split_return.i:210.
+  Called from tests/value/split_return.i:212.
 [eva] computing for function f4 <- main4 <- main.
-  Called from tests/value/split_return.i:97.
+  Called from tests/value/split_return.i:99.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {7}, {5}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main4 <- main.
-  Called from tests/value/split_return.i:210.
+  Called from tests/value/split_return.i:212.
 [eva] computing for function f4 <- main4 <- main.
-  Called from tests/value/split_return.i:97.
+  Called from tests/value/split_return.i:99.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:100: Frama_C_show_each_f4: {7}, {5}
 [eva] Recording results for main4
 [eva] Done for function main4
 [eva] computing for function main5 <- main.
-  Called from tests/value/split_return.i:211.
+  Called from tests/value/split_return.i:213.
 [eva] computing for function f5 <- main5 <- main.
-  Called from tests/value/split_return.i:120.
+  Called from tests/value/split_return.i:122.
 [eva] Recording results for f5
 [eva] Done for function f5
-[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
-[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
+[eva] tests/value/split_return.i:123: Frama_C_show_each_f5: {7}, {5}
+[eva] tests/value/split_return.i:123: Frama_C_show_each_f5: {-2}, {0}
 [eva] Recording results for main5
 [eva] Done for function main5
 [eva] computing for function main6 <- main.
-  Called from tests/value/split_return.i:212.
+  Called from tests/value/split_return.i:214.
 [eva] computing for function f6 <- main6 <- main.
-  Called from tests/value/split_return.i:138.
+  Called from tests/value/split_return.i:140.
 [eva] Recording results for f6
 [eva] Done for function f6
 [eva] Recording results for main6
 [eva] Done for function main6
 [eva] computing for function main6 <- main.
-  Called from tests/value/split_return.i:212.
+  Called from tests/value/split_return.i:214.
 [eva] computing for function f6 <- main6 <- main.
-  Called from tests/value/split_return.i:138.
+  Called from tests/value/split_return.i:140.
 [eva] Recording results for f6
 [eva] Done for function f6
 [eva] Recording results for main6
 [eva] Done for function main6
 [eva] computing for function main7 <- main.
-  Called from tests/value/split_return.i:213.
+  Called from tests/value/split_return.i:215.
 [eva] computing for function f7 <- main7 <- main.
-  Called from tests/value/split_return.i:151.
+  Called from tests/value/split_return.i:153.
 [eva] Recording results for f7
 [eva] Done for function f7
-[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {0}, {0}
-[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {{ &v }}, {1}
+[eva] tests/value/split_return.i:158: Frama_C_show_each_NULL: {0}, {0}
+[eva] tests/value/split_return.i:158: Frama_C_show_each_NULL: {{ &v }}, {1}
 [eva] Recording results for main7
 [eva] Done for function main7
 [eva] computing for function main7 <- main.
-  Called from tests/value/split_return.i:213.
+  Called from tests/value/split_return.i:215.
 [eva] computing for function f7 <- main7 <- main.
-  Called from tests/value/split_return.i:151.
+  Called from tests/value/split_return.i:153.
 [eva] Recording results for f7
 [eva] Done for function f7
-[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {0}, {0}
-[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {{ &v }}, {1}
+[eva] tests/value/split_return.i:158: Frama_C_show_each_NULL: {0}, {0}
+[eva] tests/value/split_return.i:158: Frama_C_show_each_NULL: {{ &v }}, {1}
 [eva] Recording results for main7
 [eva] Done for function main7
 [eva] computing for function main8 <- main.
-  Called from tests/value/split_return.i:214.
+  Called from tests/value/split_return.i:216.
 [eva] computing for function f8 <- main8 <- main.
-  Called from tests/value/split_return.i:174.
+  Called from tests/value/split_return.i:176.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {-1}, {0}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
-  Called from tests/value/split_return.i:214.
+  Called from tests/value/split_return.i:216.
 [eva] computing for function f8 <- main8 <- main.
-  Called from tests/value/split_return.i:174.
+  Called from tests/value/split_return.i:176.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {-1}, {0}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
-  Called from tests/value/split_return.i:214.
+  Called from tests/value/split_return.i:216.
 [eva] computing for function f8 <- main8 <- main.
-  Called from tests/value/split_return.i:174.
+  Called from tests/value/split_return.i:176.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {-1}, {0}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main8 <- main.
-  Called from tests/value/split_return.i:214.
+  Called from tests/value/split_return.i:216.
 [eva] computing for function f8 <- main8 <- main.
-  Called from tests/value/split_return.i:174.
+  Called from tests/value/split_return.i:176.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:177: Frama_C_show_each_then8: {-1}, {0}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main9 <- main.
-  Called from tests/value/split_return.i:215.
+  Called from tests/value/split_return.i:217.
 [eva] computing for function uninit <- main9 <- main.
-  Called from tests/value/split_return.i:202.
+  Called from tests/value/split_return.i:204.
 [eva] Recording results for uninit
 [eva] Done for function uninit
 [eva] computing for function escaping <- main9 <- main.
-  Called from tests/value/split_return.i:203.
+  Called from tests/value/split_return.i:205.
 [eva] Recording results for escaping
 [eva] Done for function escaping
 [eva] computing for function escaping <- main9 <- main.
-  Called from tests/value/split_return.i:203.
+  Called from tests/value/split_return.i:205.
 [eva] Recording results for escaping
 [eva] Done for function escaping
 [eva] Recording results for main9
diff --git a/tests/value/oracle/use_spec.0.res.oracle b/tests/value/oracle/use_spec.0.res.oracle
index 473f5c28774e85d3c07a0650f0853708a8c07b47..f919f266c6c3385772cec013449032dd0d85669e 100644
--- a/tests/value/oracle/use_spec.0.res.oracle
+++ b/tests/value/oracle/use_spec.0.res.oracle
@@ -2,7 +2,7 @@
 [eva] User Error: no assigns specified for function 'f', for which a builtin
   or the specification will be used. Potential unsoundness.
 [eva] Warning: Generating potentially incorrect assigns for function 'f' for which option -eva-use-spec is set
-[kernel:annot:missing-spec] tests/value/use_spec.i:7: Warning: 
+[kernel:annot:missing-spec] tests/value/use_spec.i:10: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
@@ -13,21 +13,21 @@
   y ∈ {0}
   z ∈ {0}
 [eva] computing for function f <- main.
-  Called from tests/value/use_spec.i:22.
+  Called from tests/value/use_spec.i:25.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] computing for function g <- main.
-  Called from tests/value/use_spec.i:23.
-[kernel:annot:missing-spec] tests/value/use_spec.i:23: Warning: 
+  Called from tests/value/use_spec.i:26.
+[kernel:annot:missing-spec] tests/value/use_spec.i:26: Warning: 
   Neither code nor specification for function g, generating default assigns from the prototype
 [eva] using specification for function g
 [eva] Done for function g
 [eva] computing for function h <- main.
-  Called from tests/value/use_spec.i:24.
+  Called from tests/value/use_spec.i:27.
 [eva] using specification for function h
 [eva] Done for function h
 [eva] computing for function i <- main.
-  Called from tests/value/use_spec.i:25.
+  Called from tests/value/use_spec.i:28.
 [eva] using specification for function i
 [eva] Done for function i
 [eva] Recording results for main
@@ -41,13 +41,13 @@
   y ∈ [--..--]
   z ∈ [--..--]
 [from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to f at tests/value/use_spec.i:22 (by main):
+[from] call to f at tests/value/use_spec.i:25 (by main):
   x FROM x (and SELF)
-[from] call to g at tests/value/use_spec.i:23 (by main):
+[from] call to g at tests/value/use_spec.i:26 (by main):
   y FROM y (and SELF)
-[from] call to h at tests/value/use_spec.i:24 (by main):
+[from] call to h at tests/value/use_spec.i:27 (by main):
   z FROM \nothing
-[from] call to i at tests/value/use_spec.i:25 (by main):
+[from] call to i at tests/value/use_spec.i:28 (by main):
   w FROM \nothing
 [from] entry point:
   w FROM \nothing
diff --git a/tests/value/oracle/use_spec.1.res.oracle b/tests/value/oracle/use_spec.1.res.oracle
index caebc27ff6d6acaf84a35f7c375e41bdb1adc841..0aa0d76d877484b6fcf0c9b12e851abb6c91a284 100644
--- a/tests/value/oracle/use_spec.1.res.oracle
+++ b/tests/value/oracle/use_spec.1.res.oracle
@@ -2,7 +2,7 @@
 [eva] User Error: no assigns specified for function 'f', for which a builtin
   or the specification will be used. Potential unsoundness.
 [eva] Warning: Generating potentially incorrect assigns for function 'f' for which option -eva-use-spec is set
-[kernel:annot:missing-spec] tests/value/use_spec.i:7: Warning: 
+[kernel:annot:missing-spec] tests/value/use_spec.i:10: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
@@ -13,21 +13,21 @@
   y ∈ {0}
   z ∈ {0}
 [eva] computing for function f <- main.
-  Called from tests/value/use_spec.i:22.
+  Called from tests/value/use_spec.i:25.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] computing for function g <- main.
-  Called from tests/value/use_spec.i:23.
-[kernel:annot:missing-spec] tests/value/use_spec.i:23: Warning: 
+  Called from tests/value/use_spec.i:26.
+[kernel:annot:missing-spec] tests/value/use_spec.i:26: Warning: 
   Neither code nor specification for function g, generating default assigns from the prototype
 [eva] using specification for function g
 [eva] Done for function g
 [eva] computing for function h <- main.
-  Called from tests/value/use_spec.i:24.
+  Called from tests/value/use_spec.i:27.
 [eva] using specification for function h
 [eva] Done for function h
 [eva] computing for function i <- main.
-  Called from tests/value/use_spec.i:25.
+  Called from tests/value/use_spec.i:28.
 [eva] using specification for function i
 [eva] Done for function i
 [eva] Recording results for main
@@ -41,13 +41,13 @@
   y ∈ [--..--]
   z ∈ [--..--]
 [from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to f at tests/value/use_spec.i:22 (by main):
+[from] call to f at tests/value/use_spec.i:25 (by main):
   x FROM direct: x (and SELF)
-[from] call to g at tests/value/use_spec.i:23 (by main):
+[from] call to g at tests/value/use_spec.i:26 (by main):
   y FROM direct: y (and SELF)
-[from] call to h at tests/value/use_spec.i:24 (by main):
+[from] call to h at tests/value/use_spec.i:27 (by main):
   z FROM \nothing
-[from] call to i at tests/value/use_spec.i:25 (by main):
+[from] call to i at tests/value/use_spec.i:28 (by main):
   w FROM \nothing
 [from] entry point:
   w FROM \nothing
diff --git a/tests/value/origin.i b/tests/value/origin.i
index 3146eb3f46ab38c22461e2880e799bb66af52b67..cd5d3c1c4c28178e57acdedd89077dfff0b0d9c3 100644
--- a/tests/value/origin.i
+++ b/tests/value/origin.i
@@ -1,7 +1,7 @@
 /* run.config*
-   
-   OPT: -no-autoload-plugins -load-module from,inout,eva @EVA_CONFIG@ -eva -eva-warn-copy-indeterminate=-origin_misalign_2,-main -main main -journal-disable -then -out -deps
-   OPT: -no-autoload-plugins -load-module from,inout,eva @EVA_CONFIG@ -eva -eva-warn-copy-indeterminate=-origin_misalign_2,-origin -main origin -journal-disable -then -out -deps
+ PLUGIN: @EVA_MAIN_PLUGINS@ inout,from
+   OPT: @EVA_CONFIG@ -eva -eva-warn-copy-indeterminate=-origin_misalign_2,-main -main main -then -out -deps
+   OPT: @EVA_CONFIG@ -eva -eva-warn-copy-indeterminate=-origin_misalign_2,-origin -main origin -then -out -deps
 
 */
 char f(void);
diff --git a/tests/value/pointer_comparison.c b/tests/value/pointer_comparison.c
index 40717af44c5547544a81941d440e3e5673642187..5b5d341d0c4075647c4c3ce52f73a1c978a53616 100644
--- a/tests/value/pointer_comparison.c
+++ b/tests/value/pointer_comparison.c
@@ -1,8 +1,13 @@
 /* run.config*
-   STDOPT: +" -load-module report -report-print-properties -eva-warn-undefined-pointer-comparison none -eva-msg-key pointer-comparison -then -report -then -eva-warn-undefined-pointer-comparison pointer -then -report -then -eva-warn-undefined-pointer-comparison all -then -report"
-   STDOPT: +" -load-module report -report-print-properties -eva-undefined-pointer-comparison-propagate-all -eva-warn-undefined-pointer-comparison none -eva-msg-key pointer-comparison -then -report -then -eva-warn-undefined-pointer-comparison pointer -then -report -then -eva-warn-undefined-pointer-comparison all -then -report"
+ PLUGIN: @PTEST_PLUGIN@ report
+   STDOPT: +" -report-print-properties -eva-warn-undefined-pointer-comparison none -eva-msg-key pointer-comparison -then -report -then -eva-warn-undefined-pointer-comparison pointer -then -report -then -eva-warn-undefined-pointer-comparison all -then -report"
+   STDOPT: +" -report-print-properties -eva-undefined-pointer-comparison-propagate-all -eva-warn-undefined-pointer-comparison none -eva-msg-key pointer-comparison -then -report -then -eva-warn-undefined-pointer-comparison pointer -then -report -then -eva-warn-undefined-pointer-comparison all -then -report"
+
 */
+
+
 int x,y,*p;
+
 int main(){
   p = &x;
   if (p++ != &y) Frama_C_show_each_1t(p);
diff --git a/tests/value/postcond_leaf.c b/tests/value/postcond_leaf.c
index 37b99f53706ca6690608d4df5d780720fb0afa04..5716b272b950ae7e0f926e8da33215d9f4b50028 100644
--- a/tests/value/postcond_leaf.c
+++ b/tests/value/postcond_leaf.c
@@ -1,5 +1,6 @@
 /* run.config* 
-OPT: -no-autoload-plugins @EVA_CONFIG@ -load-module eva,inout,report -eva-no-show-progress -eva -eva-use-spec g1,g2,g3 -then -report
+ PLUGIN: @EVA_MAIN_PLUGINS@ report
+   OPT: @EVA_CONFIG@ -eva-no-show-progress -eva -eva-use-spec g1,g2,g3 -then -report
 */
 
 /* Test what is printed when Value evaluates a post-condition:
@@ -15,7 +16,6 @@ OPT: -no-autoload-plugins @EVA_CONFIG@ -load-module eva,inout,report -eva-no-sho
      warning is too distracting otherwise)
 */
 
-
 extern int i;
 
 //@ ensures 0 == 1;
diff --git a/tests/value/precise_locations.i b/tests/value/precise_locations.i
index 942739895819533255887b5f61ec8f7e124fd806..4c66a8257edcbc1d18e9f84c2b4dc711deef5254 100644
--- a/tests/value/precise_locations.i
+++ b/tests/value/precise_locations.i
@@ -1,7 +1,7 @@
 /* run.config*
-   STDOPT: +"-eva-widening-period 3 -then -inout -load-module report -report -then -eva-plevel 250"
+ PLUGIN: @PTEST_PLUGIN@ report
+   STDOPT: +"-eva-widening-period 3 -then -inout -report -then -eva-plevel 250"
 */
-
 struct s {
   int f1[5];
   int f_inter[5];
diff --git a/tests/value/precond.c b/tests/value/precond.c
index a8c73729935defb33716cd1688cef3fb929786fa..adf9cc9c33b40e95b8503dd0c13e128285e9a800 100644
--- a/tests/value/precond.c
+++ b/tests/value/precond.c
@@ -1,8 +1,8 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module from,inout,eva,report -lib-entry -eva @EVA_CONFIG@ -then -report -report-print-properties -then -report-no-specialized
+ PLUGIN: @EVA_MAIN_PLUGINS@ report
+   OPT: -lib-entry -eva @EVA_CONFIG@ -then -report -report-print-properties -then -report-no-specialized
 */
 
-
 int x;
 
 /*@ requires i_plus_one: i+1 >= 0;
diff --git a/tests/value/precond2.c b/tests/value/precond2.c
index d5c8cf126ac1479a370de2b8533dcb292e9530e3..a9b51cc52f71e9f157a5f51d1ff1f67c04af1fab 100644
--- a/tests/value/precond2.c
+++ b/tests/value/precond2.c
@@ -1,5 +1,5 @@
 /* run.config*
-PLUGIN: @PTEST_PLUGIN@ report rtegen
+PLUGIN: @EVA_MAIN_PLUGINS@ report rtegen
    OPT: -machdep x86_32 @RTE_TEST@ -then -eva @EVA_CONFIG@ -then -report -report-print-properties
    OPT: -machdep x86_32 -eva @EVA_CONFIG@ -then @RTE_TEST@  -then -report -report-print-properties
 */
diff --git a/tests/value/protomain.i b/tests/value/protomain.i
index ff7e47cb0b4932e85d8ffb3a341b0e4f19e3c604..b9018d4e5dac5e76924982102895c81f572eb4d9 100644
--- a/tests/value/protomain.i
+++ b/tests/value/protomain.i
@@ -1,4 +1,5 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@
 */
 int main(int c, char **);
diff --git a/tests/value/recol.c b/tests/value/recol.c
index 46f6de92f5ab375b405205aee08f18c3c344ddcf..afddafdc2a795bb6d13a37f4cd5c31a460d59e93 100644
--- a/tests/value/recol.c
+++ b/tests/value/recol.c
@@ -1,8 +1,8 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -eva-slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -no-warn-signed-overflow
-   OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -eva-slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -machdep ppc_32 -no-warn-signed-overflow
+PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -eva-slevel 100 -cpp-extra-args="-DPTEST " -no-warn-signed-overflow
+   OPT: -eva @EVA_CONFIG@ -eva-slevel 100 -cpp-extra-args="-DPTEST " -machdep ppc_32 -no-warn-signed-overflow
 */
-
 #ifndef PTEST
 #include <stdio.h>
 #endif
diff --git a/tests/value/redundant_alarms.c b/tests/value/redundant_alarms.c
index a6b1785cd3d19a218c1a13b55ca62b8bda5344d0..1009eafff78a6b6e4c778ce62ce41d192e621084 100644
--- a/tests/value/redundant_alarms.c
+++ b/tests/value/redundant_alarms.c
@@ -1,7 +1,7 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module inout,scope,slicing,sparecode @EVA_CONFIG@ -eva-warn-copy-indeterminate=-@all,main3 -scope-msg-key rm_asserts -scope-verbose 2 -eva-remove-redundant-alarms -print -slice-threat main1 -then-on 'Slicing export' -print
+ PLUGIN: inout,scope,slicing,sparecode
+   OPT: @EVA_CONFIG@ -eva-warn-copy-indeterminate=-@all,main3 -scope-msg-key rm_asserts -scope-verbose 2 -eva-remove-redundant-alarms -print -slice-threat main1 -then-on 'Slicing export' -print
  **/
-
 volatile int v;
 
 void main1(int c) {
diff --git a/tests/value/reevaluate_alarms.i b/tests/value/reevaluate_alarms.i
index 9085a0a7185533f1b36bbf543d4b94b45f86db36..649ac3850284a94a358a0e59d74118f116802d6a 100644
--- a/tests/value/reevaluate_alarms.i
+++ b/tests/value/reevaluate_alarms.i
@@ -1,8 +1,8 @@
 /* run.config*
-   STDOPT: +"-load-module report -report -then -eva-slevel 10"
+ PLUGIN: @PTEST_PLUGIN@ report
+   STDOPT: +"-report -then -eva-slevel 10"
 */
 
-
 int S=0;
 int T[5];
 int n = 1;
diff --git a/tests/value/replace_by_show_each.c b/tests/value/replace_by_show_each.c
index 51592b67f44fd1c183ee2478a67dc16468c4ed9f..832a73028a0081dc7c2719cb7ce9d6e9925872b0 100644
--- a/tests/value/replace_by_show_each.c
+++ b/tests/value/replace_by_show_each.c
@@ -1,7 +1,7 @@
 /* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -inout -calldeps
+ PLUGIN: @EVA_MAIN_PLUGINS@ from,inout
+   OPT: -eva @EVA_CONFIG@ -inout -calldeps
 */
-
 #define show_each_1 Frama_C_show_each_1
 #define show_each_2 Frama_C_show_each_2
 
diff --git a/tests/value/sign_of_bitfiled_int.c b/tests/value/sign_of_bitfiled_int.c
index b69aa28c06baafceb1534387dc5b661cbbb20ab1..f26d8b248cd884cb6fd20182c89adbb4eed4f2f2 100644
--- a/tests/value/sign_of_bitfiled_int.c
+++ b/tests/value/sign_of_bitfiled_int.c
@@ -1,9 +1,9 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST"  -journal-disable
-   OPT: -no-autoload-plugins -load-module eva,inout -machdep ppc_32 -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST" -journal-disable
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST"
+   OPT: -machdep ppc_32 -eva @EVA_CONFIG@ -cpp-extra-args="-DPTEST"
 */
 
-
 #ifndef PTEST
 #include <stdio.h>
 #endif
diff --git a/tests/value/simplify_cfg.i b/tests/value/simplify_cfg.i
index 5c1b0f1d7193e23bfa1bcbc04740b3aacbd5b681..f10fb7cbcd5f6f32751990df583c0ba302825b69 100644
--- a/tests/value/simplify_cfg.i
+++ b/tests/value/simplify_cfg.i
@@ -1,8 +1,8 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module eva,inout -simplify-cfg -keep-switch -eva @EVA_CONFIG@ -journal-disable
-   OPT: -no-autoload-plugins -load-module eva,inout -simplify-cfg -eva @EVA_CONFIG@ -journal-disable
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -simplify-cfg -keep-switch -eva @EVA_CONFIG@
+   OPT: -simplify-cfg -eva @EVA_CONFIG@
 */
-
 int main(int x, int y) {
   int z = 0;
   char c = 'c';
diff --git a/tests/value/split_return.i b/tests/value/split_return.i
index df9fbcbdada17c3366d1da87a6b948f454b8129e..08b7e3e2ea7e4d22cfa1b736084949d33a47ce4e 100644
--- a/tests/value/split_return.i
+++ b/tests/value/split_return.i
@@ -1,12 +1,14 @@
 /* run.config*
-   STDOPT: +"-deterministic -eva-no-memexec -eva-slevel-function init:3,main1:3,f2:4,main2:4,f4:3,main5:3,uninit:2,main9:2 -eva-split-return-function f2:0,f3:-2:-4,f4:4,f5:-2,NON_EXISTING:4,uninit:0,escaping:0 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -permissive -then -load-module report -report"
-   STDOPT: +"-deterministic -eva-no-memexec -eva -journal-disable -out -input -deps -eva-slevel 6 -eva-split-return auto -eva-split-return-function f7:0:3 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -then -load-module report -report"
+ PLUGIN: @PTEST_PLUGIN@ report
+   STDOPT: +"-deterministic -eva-no-memexec -eva-slevel-function init:3,main1:3,f2:4,main2:4,f4:3,main5:3,uninit:2,main9:2 -eva-split-return-function f2:0,f3:-2:-4,f4:4,f5:-2,NON_EXISTING:4,uninit:0,escaping:0 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -permissive -then -report"
+   STDOPT: +"-deterministic -eva-no-memexec -eva-slevel 6 -eva-split-return auto -eva-split-return-function f7:0:3 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -then -report"
+ PLUGIN: @EVA_PLUGINS@
  EXIT:1
    COMMENT: below command must fail, as -permissive is not set
-   STDOPT: +"-deterministic -eva-no-memexec -eva -eva-slevel-function NON_EXISTING:4 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9"
+   STDOPT: +"-deterministic -eva-no-memexec -eva-slevel-function NON_EXISTING:4 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9"
  EXIT:0
-   STDOPT: +"-deterministic -eva-no-memexec -eva -journal-disable -out -input -deps -eva-slevel 6 -eva-split-return full -eva-warn-copy-indeterminate=-uninit,-escaping,-main9"
-   STDOPT: +"-deterministic -eva-no-memexec -eva -journal-disable -out -input -deps -eva-slevel 6 -eva-split-return full -eva-split-return-function f7:0:3 -eva-split-return-function f2:full -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -then -eva-split-return-function f2:auto"
+   STDOPT: +"-deterministic -eva-no-memexec -eva-slevel 6 -eva-split-return full -eva-warn-copy-indeterminate=-uninit,-escaping,-main9"
+   STDOPT: +"-deterministic -eva-no-memexec -eva-slevel 6 -eva-split-return full -eva-split-return-function f7:0:3 -eva-split-return-function f2:full -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -then -eva-split-return-function f2:auto"
  */
 
 
diff --git a/tests/value/ulongvslonglong.i b/tests/value/ulongvslonglong.i
index c945f20f8813505c233ddf76b4df42533726d3bc..6de591f1cbcfa4fad682d832e564e234621c009b 100644
--- a/tests/value/ulongvslonglong.i
+++ b/tests/value/ulongvslonglong.i
@@ -1,8 +1,8 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -journal-disable -machdep x86_64
-   OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -journal-disable
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -machdep x86_64
+   OPT: -eva @EVA_CONFIG@
 */
-
 int x;
 long x2;
 unsigned long x9[6][2];
diff --git a/tests/value/uninit_callstack.i b/tests/value/uninit_callstack.i
index 6adb7e5120047524db8d21d776a7d7f5d76c9abc..8ee2bed040ae9d010226ded9ee9ddf6883fe8985 100644
--- a/tests/value/uninit_callstack.i
+++ b/tests/value/uninit_callstack.i
@@ -1,8 +1,8 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -eva-no-show-progress -eva-print-callstacks -journal-disable -eva-no-results
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@ -eva-no-show-progress -eva-print-callstacks -eva-no-results
 */
 int *p, x;
-
 void f(void)
 {
   if (*p) x = 1;
diff --git a/tests/value/unknown_sizeof.i b/tests/value/unknown_sizeof.i
index 94e88f03ca2aaa60f0b99312ef0a1c2dbc9868b0..40b7487daa78839926f4004ada6b81924d513109 100644
--- a/tests/value/unknown_sizeof.i
+++ b/tests/value/unknown_sizeof.i
@@ -1,10 +1,10 @@
 /* run.config*
  EXIT: 1
-   OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -main main1
-   OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -main main2
+ PLUGIN: eva
+   OPT: -eva @EVA_CONFIG@ -main main1
+   OPT: -eva @EVA_CONFIG@ -main main2
 */
 struct s;
-
 struct s s;
 
 void f(struct s) { // Argument has unknown size
diff --git a/tests/value/use_spec.i b/tests/value/use_spec.i
index 3097dcc25cb54367cd22fe2bc77aa23d5cfea43c..ebbe2977bbf3c0194c0255b63c553e79321976de 100644
--- a/tests/value/use_spec.i
+++ b/tests/value/use_spec.i
@@ -1,9 +1,12 @@
 /* run.config*
+ PLUGIN: @EVA_MAIN_PLUGINS@ from,inout
  EXIT: 1
-   OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @EVA_CONFIG@ -inout -calldeps
-   OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @EVA_CONFIG@ -inout -calldeps -show-indirect-deps
+   OPT: -eva-use-spec f,h -eva @EVA_CONFIG@ -inout -calldeps
+   OPT: -eva-use-spec f,h -eva @EVA_CONFIG@ -inout -calldeps -show-indirect-deps
 */
 
+
+
 void f(int *x) {
 }
 
diff --git a/tests/value/volatile2.i b/tests/value/volatile2.i
index f1088a88553a2248945e46d4bbb132348729c74f..0a4a86e76ec0dd4f4f2cf93b6965cbd22f806c0a 100644
--- a/tests/value/volatile2.i
+++ b/tests/value/volatile2.i
@@ -1,8 +1,8 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module from,inout,eva -print -eva @EVA_CONFIG@ -machdep x86_16
+  PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -print -eva @EVA_CONFIG@ -machdep x86_16
 */
 
-
 volatile unsigned char t[10];
 struct u { unsigned char f1; unsigned char f2;};
 volatile struct u u;
diff --git a/tests/value/widen_overflow.i b/tests/value/widen_overflow.i
index 9bf6480e8085454da2b1e8bacec7f77ba184285a..97168423354269637c70f4b978402c47ed3f4ec8 100644
--- a/tests/value/widen_overflow.i
+++ b/tests/value/widen_overflow.i
@@ -1,7 +1,7 @@
 /* run.config*
-   OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@
+ PLUGIN: @EVA_MAIN_PLUGINS@
+   OPT: -eva @EVA_CONFIG@
 */
-
 int main() {
   Frama_C_show_each(sizeof(unsigned int));