diff --git a/src/plugins/e-acsl/gcc_bts.sh b/src/plugins/e-acsl/gcc_bts.sh
new file mode 100755
index 0000000000000000000000000000000000000000..2cdb3e49a1e682a855bfbc36d08b87b9a8587885
--- /dev/null
+++ b/src/plugins/e-acsl/gcc_bts.sh
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+./gcc_test.sh bts $@
diff --git a/src/plugins/e-acsl/gcc_runtime.sh b/src/plugins/e-acsl/gcc_runtime.sh
new file mode 100755
index 0000000000000000000000000000000000000000..b6794c4fd873bd4f01c72ccee4218a142720d4a3
--- /dev/null
+++ b/src/plugins/e-acsl/gcc_runtime.sh
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+./gcc_test.sh e-acsl-runtime $@
diff --git a/src/plugins/e-acsl/gcc_test.sh b/src/plugins/e-acsl/gcc_test.sh
index 20dc759894c03f5ae9b2434c016b07c9d6c09fc7..069a66c227661016e7302c4147569f405cd52d23 100755
--- a/src/plugins/e-acsl/gcc_test.sh
+++ b/src/plugins/e-acsl/gcc_test.sh
@@ -1,16 +1,19 @@
 #!/bin/sh
-IN=$1
-if [ $# -gt 1 ]; then
-    shift;
+
+DIR=$1
+IN=$2
+if [ $# -gt 2 ]; then
+    shift
+    shift
     BUILTIN=$1
     shift;
     ARGS=$@
 fi
 
-gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/e-acsl-runtime/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_bittree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$IN.c -lgmp && ./tests/e-acsl-runtime/result/gen_$IN.out $ARGS
+gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/$DIR/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_bittree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/$DIR/result/gen_$IN.c -lgmp && ./tests/$DIR/result/gen_$IN.out $ARGS
 
-gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/e-acsl-runtime/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_list.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$IN.c -lgmp && ./tests/e-acsl-runtime/result/gen_$IN.out $ARGS
+gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/$DIR/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_list.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/$DIR/result/gen_$IN.c -lgmp && ./tests/$DIR/result/gen_$IN.out $ARGS
 
-gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/e-acsl-runtime/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_splay_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$IN.c -lgmp && ./tests/e-acsl-runtime/result/gen_$IN.out $ARGS
+gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/$DIR/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_splay_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/$DIR/result/gen_$IN.c -lgmp && ./tests/$DIR/result/gen_$IN.out $ARGS
 
-gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/e-acsl-runtime/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$IN.c -lgmp && ./tests/e-acsl-runtime/result/gen_$IN.out $ARGS
+gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/$DIR/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/$DIR/result/gen_$IN.c -lgmp && ./tests/$DIR/result/gen_$IN.out $ARGS
diff --git a/src/plugins/e-acsl/tests/bts/bts1304.i b/src/plugins/e-acsl/tests/bts/bts1304.i
index ef6a48c1e39ee1d75ea0085bd0034f75c16dcc6f..a32a26d4b84c6348d0f3edcfb9eb2926e96ba97e 100644
--- a/src/plugins/e-acsl/tests/bts/bts1304.i
+++ b/src/plugins/e-acsl/tests/bts/bts1304.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: argument of functions must be kept, so keep its parameter
-   EXECNOW: LOG gen_bts1304.c BIN gen_bts1304.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1304.i -constfold -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1304.c > /dev/null && ./gcc_test.sh bts1304
-   EXECNOW: LOG gen_bts13042.c BIN gen_bts13042.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1304.i -constfold -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13042.c > /dev/null && ./gcc_test.sh bts13042
+   EXECNOW: LOG gen_bts1304.c BIN gen_bts1304.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1304.i -constfold -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1304.c > /dev/null && ./gcc_bts.sh bts1304
+   EXECNOW: LOG gen_bts13042.c BIN gen_bts13042.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1304.i -constfold -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13042.c > /dev/null && ./gcc_bts.sh bts13042
 */
 
 struct msgA { int type; int a[2]; };
diff --git a/src/plugins/e-acsl/tests/bts/bts1307.i b/src/plugins/e-acsl/tests/bts/bts1307.i
index 12968768efdae58bf99a7ec7ca80b5d88d753330..2e3cabdd70b0874b3c368204b85ea05edd0694ae 100644
--- a/src/plugins/e-acsl/tests/bts/bts1307.i
+++ b/src/plugins/e-acsl/tests/bts/bts1307.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: spec with floats and reals
-   EXECNOW: LOG gen_bts1307.c BIN gen_bts1307.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1307.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1307.c > /dev/null && ./gcc_test.sh bts1307
-   EXECNOW: LOG gen_bts13072.c BIN gen_bts13072.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1307.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13072.c > /dev/null && ./gcc_test.sh bts13072
+   EXECNOW: LOG gen_bts1307.c BIN gen_bts1307.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1307.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1307.c > /dev/null && ./gcc_bts.sh bts1307
+   EXECNOW: LOG gen_bts13072.c BIN gen_bts13072.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1307.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13072.c > /dev/null && ./gcc_bts.sh bts13072
 */
 
 /*@ requires \valid(Mtmax_in);
diff --git a/src/plugins/e-acsl/tests/bts/bts1324.i b/src/plugins/e-acsl/tests/bts/bts1324.i
index 1aa509718181d6e615f6eeb479d48d1822c7fe0b..9b444f126b0cd79eb5b48ff5ab60e82b8b220dcb 100644
--- a/src/plugins/e-acsl/tests/bts/bts1324.i
+++ b/src/plugins/e-acsl/tests/bts/bts1324.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: fixed bug with typing of universal quantification
-   EXECNOW: LOG gen_bts1324.c BIN gen_bts1324.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1324.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1324.c > /dev/null && ./gcc_test.sh bts1324
-   EXECNOW: LOG gen_bts13242.c BIN gen_bts13242.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1324.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13242.c > /dev/null && ./gcc_test.sh bts13242
+   EXECNOW: LOG gen_bts1324.c BIN gen_bts1324.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1324.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1324.c > /dev/null && ./gcc_bts.sh bts1324
+   EXECNOW: LOG gen_bts13242.c BIN gen_bts13242.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1324.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13242.c > /dev/null && ./gcc_bts.sh bts13242
 */
 
 /*@ behavior yes:
diff --git a/src/plugins/e-acsl/tests/bts/bts1326.i b/src/plugins/e-acsl/tests/bts/bts1326.i
index 63412190fcabeaa061909b8c3911bbad7ff1b585..b18101c3d1017c34fda38cdc5abb67bdfa4d3b36 100644
--- a/src/plugins/e-acsl/tests/bts/bts1326.i
+++ b/src/plugins/e-acsl/tests/bts/bts1326.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: complex term left-values
-   EXECNOW: LOG gen_bts1326.c BIN gen_bts1326.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1326.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1326.c > /dev/null && ./gcc_test.sh bts1326
-   EXECNOW: LOG gen_bts13262.c BIN gen_bts13262.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1326.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13262.c > /dev/null && ./gcc_test.sh bts13262
+   EXECNOW: LOG gen_bts1326.c BIN gen_bts1326.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1326.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1326.c > /dev/null && ./gcc_bts.sh bts1326
+   EXECNOW: LOG gen_bts13262.c BIN gen_bts13262.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1326.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13262.c > /dev/null && ./gcc_bts.sh bts13262
 */
 
 typedef int ArrayInt[5];
diff --git a/src/plugins/e-acsl/tests/bts/bts1390.c b/src/plugins/e-acsl/tests/bts/bts1390.c
index 0d203d313aff62eac7e75e677c925e2051eea79f..5ff6dc147983e8f9ad5de360a38460fb786a3325 100644
--- a/src/plugins/e-acsl/tests/bts/bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/bts1390.c
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: bts #1390, issue with typing of quantified variables
    STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
-   EXECNOW: LOG gen_bts1390.c BIN gen_bts1390.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1390.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1390.c > /dev/null && ./gcc_test.sh bts1390
-   EXECNOW: LOG gen_bts13902.c BIN gen_bts13902.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1390.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13902.c > /dev/null && ./gcc_test.sh bts13902
+   EXECNOW: LOG gen_bts1390.c BIN gen_bts1390.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1390.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1390.c > /dev/null && ./gcc_bts.sh bts1390
+   EXECNOW: LOG gen_bts13902.c BIN gen_bts13902.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1390.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13902.c > /dev/null && ./gcc_bts.sh bts13902
 */
 
 #include "stdlib.h"
diff --git a/src/plugins/e-acsl/tests/bts/bts1398.c b/src/plugins/e-acsl/tests/bts/bts1398.c
index c1480633d8262409de24a37362e6d53a37f16275..d02bb8faa91f9272d7cb386afdb6c6b63a8b8de3 100644
--- a/src/plugins/e-acsl/tests/bts/bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/bts1398.c
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: variadic function call
    STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
-   EXECNOW: LOG gen_bts1398.c BIN gen_bts1398.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1398.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1398.c > /dev/null && ./gcc_test.sh bts1398 > /dev/null
-   EXECNOW: LOG gen_bts13982.c BIN gen_bts13982.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1398.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13982.c > /dev/null && ./gcc_test.sh bts13982 > /dev/null
+   EXECNOW: LOG gen_bts1398.c BIN gen_bts1398.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1398.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1398.c > /dev/null && ./gcc_bts.sh bts1398 > /dev/null
+   EXECNOW: LOG gen_bts13982.c BIN gen_bts13982.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1398.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13982.c > /dev/null && ./gcc_bts.sh bts13982 > /dev/null
 */
 
 #include "stdio.h"
diff --git a/src/plugins/e-acsl/tests/bts/bts1399.c b/src/plugins/e-acsl/tests/bts/bts1399.c
index c246d7acc6b147307f5e093da9e1d0534dfd9d36..43300c93834cf06f063649d63505a1b7356941d8 100644
--- a/src/plugins/e-acsl/tests/bts/bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/bts1399.c
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: complex fields and indexes + potential RTE in \initialized
    STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
-   EXECNOW: LOG gen_bts1399.c BIN gen_bts1399.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1399.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1399.c > /dev/null && ./gcc_test.sh bts1399
-   EXECNOW: LOG gen_bts13992.c BIN gen_bts13992.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1399.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13992.c > /dev/null && ./gcc_test.sh bts13992
+   EXECNOW: LOG gen_bts1399.c BIN gen_bts1399.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1399.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1399.c > /dev/null && ./gcc_bts.sh bts1399
+   EXECNOW: LOG gen_bts13992.c BIN gen_bts13992.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1399.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13992.c > /dev/null && ./gcc_bts.sh bts13992
 */
 
 #include "stdlib.h"
diff --git a/src/plugins/e-acsl/tests/bts/bts1478.c b/src/plugins/e-acsl/tests/bts/bts1478.c
index a5fadbe4dd5f0ea348e44748bb4aef1b2633dc40..9b1bcd88bda4e4194f19b1c80af61dc9597eb1df 100644
--- a/src/plugins/e-acsl/tests/bts/bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/bts1478.c
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: bts #1478 about wrong detection of initializers in pre-analysis
-   EXECNOW: LOG gen_bts1478.c BIN gen_bts1478.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1478.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1478.c > /dev/null && ./gcc_test.sh bts1478
-   EXECNOW: LOG gen_bts14782.c BIN gen_bts14782.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1478.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts14782.c > /dev/null && ./gcc_test.sh bts14782
+   EXECNOW: LOG gen_bts1478.c BIN gen_bts1478.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1478.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1478.c > /dev/null && ./gcc_bts.sh bts1478
+   EXECNOW: LOG gen_bts14782.c BIN gen_bts14782.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1478.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts14782.c > /dev/null && ./gcc_bts.sh bts14782
 */
 
 int global_i;
diff --git a/src/plugins/e-acsl/tests/bts/bts1700.i b/src/plugins/e-acsl/tests/bts/bts1700.i
index b76adfe91c3666dffe9b209e020a8e59835d8f2d..2534d1f1be441af6e5db9bcf7421015577fcb7f6 100644
--- a/src/plugins/e-acsl/tests/bts/bts1700.i
+++ b/src/plugins/e-acsl/tests/bts/bts1700.i
@@ -1,6 +1,6 @@
 /* run.config
    COMMENT: pointer to an empty struct
-   EXECNOW: LOG gen_bts1700.c BIN gen_bts1700.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1700.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1700.c > /dev/null && ./gcc_test.sh bts1700
+   EXECNOW: LOG gen_bts1700.c BIN gen_bts1700.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1700.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1700.c > /dev/null && ./gcc_bts.sh bts1700
 */
 
 struct toto {};
diff --git a/src/plugins/e-acsl/tests/bts/bts1717.i b/src/plugins/e-acsl/tests/bts/bts1717.i
index 3164300f7513db10b5f25d0639b687a38bccb0f8..99925f479ec5671173faae23491e201bd96db244 100644
--- a/src/plugins/e-acsl/tests/bts/bts1717.i
+++ b/src/plugins/e-acsl/tests/bts/bts1717.i
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: bts #1717, issue with labels on memory-related statements
    STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
-   EXECNOW: LOG gen_bts1717.c BIN gen_bts1717.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1717.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1717.c > /dev/null && ./gcc_test.sh bts1717
-   EXECNOW: LOG gen_bts17172.c BIN gen_bts17172.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1717.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts17172.c > /dev/null && ./gcc_test.sh bts17172
+   EXECNOW: LOG gen_bts1717.c BIN gen_bts1717.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1717.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1717.c > /dev/null && ./gcc_bts.sh bts1717
+   EXECNOW: LOG gen_bts17172.c BIN gen_bts17172.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1717.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts17172.c > /dev/null && ./gcc_bts.sh bts17172
 */
 
 int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i b/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i
index 8436ac41c09c9e3c4fb74bee6d628e517b7d2d2a..42c611babba9204a641953030ec827f30a0b9acf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: addrOf
-   EXECNOW: LOG gen_addrOf.c BIN gen_addrOf.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/addrOf.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf.c > /dev/null && ./gcc_test.sh addrOf
-   EXECNOW: LOG gen_addrOf2.c BIN gen_addrOf2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/addrOf.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf2.c > /dev/null && ./gcc_test.sh addrOf2
+   EXECNOW: LOG gen_addrOf.c BIN gen_addrOf.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/addrOf.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf.c > /dev/null && ./gcc_runtime.sh addrOf
+   EXECNOW: LOG gen_addrOf2.c BIN gen_addrOf2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/addrOf.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf2.c > /dev/null && ./gcc_runtime.sh addrOf2
 */
 
 void f(){
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/alias.i b/src/plugins/e-acsl/tests/e-acsl-runtime/alias.i
index 3f796bc98551c874f0226a135b605c7c11f7df04..9919f2a34439f0e9ff1d15d6a0a1cf728666435e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/alias.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/alias.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: alias
-   EXECNOW: LOG gen_alias.c BIN gen_alias.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/alias.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_alias.c > /dev/null && ./gcc_test.sh alias
-   EXECNOW: LOG gen_alias2.c BIN gen_alias2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/alias.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_alias2.c > /dev/null && ./gcc_test.sh alias2
+   EXECNOW: LOG gen_alias.c BIN gen_alias.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/alias.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_alias.c > /dev/null && ./gcc_runtime.sh alias
+   EXECNOW: LOG gen_alias2.c BIN gen_alias2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/alias.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_alias2.c > /dev/null && ./gcc_runtime.sh alias2
 */
 
 void f(int* dest, int val)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i b/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
index f502b4e2d5363cec47f2911aff3b41d02e2771cb..793007db3ac6e1863a80df6ebc0fdd375bf5774b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: arithmetic operations
    COMMENT: add the last assertion when fixing BTS #751
-   EXECNOW: LOG gen_arith.c BIN gen_arith.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/arith.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_arith.c > /dev/null && ./gcc_test.sh arith
-   EXECNOW: LOG gen_arith2.c BIN gen_arith2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/arith.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_arith2.c > /dev/null && ./gcc_test.sh arith2
+   EXECNOW: LOG gen_arith.c BIN gen_arith.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/arith.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_arith.c > /dev/null && ./gcc_runtime.sh arith
+   EXECNOW: LOG gen_arith2.c BIN gen_arith2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/arith.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_arith2.c > /dev/null && ./gcc_runtime.sh arith2
 */
 
 int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/array.i b/src/plugins/e-acsl/tests/e-acsl-runtime/array.i
index 26079f087b3376b01ab9eb251f1a236631364556..e6e805f9ad1705add962747265355dff1b5b4f15 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/array.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/array.i
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: arrays
    STDOPT: #"-slevel 5"
-   EXECNOW: LOG gen_array.c BIN gen_array.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/array.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_array.c > /dev/null && ./gcc_test.sh array
-   EXECNOW: LOG gen_array2.c BIN gen_array2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/array.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_array2.c > /dev/null && ./gcc_test.sh array2
+   EXECNOW: LOG gen_array.c BIN gen_array.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/array.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_array.c > /dev/null && ./gcc_runtime.sh array
+   EXECNOW: LOG gen_array2.c BIN gen_array2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/array.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_array2.c > /dev/null && ./gcc_runtime.sh array2
 */
 
 int T1[3],T2[4];
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/at.i b/src/plugins/e-acsl/tests/e-acsl-runtime/at.i
index 33eff5ba2876fae7b07194fcda201dc1adc2df8d..6c4e69866e4f1a293a98cadd68daf50ec4497e8a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/at.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/at.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: \at
-   EXECNOW: LOG gen_at.c BIN gen_at.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/at.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_at.c > /dev/null && ./gcc_test.sh at -Wno-unused-label
-   EXECNOW: LOG gen_at2.c BIN gen_at2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/at.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_at2.c > /dev/null && ./gcc_test.sh at2 -Wno-unused-label
+   EXECNOW: LOG gen_at.c BIN gen_at.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/at.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_at.c > /dev/null && ./gcc_runtime.sh at -Wno-unused-label
+   EXECNOW: LOG gen_at2.c BIN gen_at2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/at.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_at2.c > /dev/null && ./gcc_runtime.sh at2 -Wno-unused-label
 */
 
 int A = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/call.c b/src/plugins/e-acsl/tests/e-acsl-runtime/call.c
index ead459fbf85399c7c4bf2da924d1211cb13ece83..053d17c39d22f4e4e1b1388c1e7595c18a9b1b09 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/call.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/call.c
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: function call
    STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
-   EXECNOW: LOG gen_call.c BIN gen_call.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/call.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_call.c > /dev/null && ./gcc_test.sh call
-   EXECNOW: LOG gen_call2.c BIN gen_call2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/call.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_call2.c > /dev/null && ./gcc_test.sh call2
+   EXECNOW: LOG gen_call.c BIN gen_call.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/call.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_call.c > /dev/null && ./gcc_runtime.sh call
+   EXECNOW: LOG gen_call2.c BIN gen_call2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/call.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_call2.c > /dev/null && ./gcc_runtime.sh call2
 */
 
 #include <stdlib.h>
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i b/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i
index 960020de72daf8d66361381ad1ba9635afa38e16..b5f005b2ed4d11c5d521d2f3de00877ca4b00748 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: cast
    STDOPT: #"-no-warn-signed-downcast" #"-no-warn-unsigned-downcast"
-   EXECNOW: LOG gen_cast.c BIN gen_cast.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/cast.i -e-acsl -no-warn-signed-downcast -no-warn-unsigned-downcast -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_cast.c > /dev/null && ./gcc_test.sh cast
-   EXECNOW: LOG gen_cast2.c BIN gen_cast2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/cast.i -e-acsl-gmp-only -no-warn-signed-downcast -no-warn-unsigned-downcast -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_cast2.c > /dev/null && ./gcc_test.sh cast2
+   EXECNOW: LOG gen_cast.c BIN gen_cast.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/cast.i -e-acsl -no-warn-signed-downcast -no-warn-unsigned-downcast -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_cast.c > /dev/null && ./gcc_runtime.sh cast
+   EXECNOW: LOG gen_cast2.c BIN gen_cast2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/cast.i -e-acsl-gmp-only -no-warn-signed-downcast -no-warn-unsigned-downcast -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_cast2.c > /dev/null && ./gcc_runtime.sh cast2
 */
 
 int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i b/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
index cfb2f91ab4c2c38ecce168f5c7964d9439fbb4c8..3bae6308b5844ada219b99a3a15cdfaee9c0ee9a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: comparison operators
-   EXECNOW: LOG gen_comparison.c BIN gen_comparison.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/comparison.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_comparison.c > /dev/null && ./gcc_test.sh comparison
-   EXECNOW: LOG gen_comparison2.c BIN gen_comparison2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/comparison.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_comparison2.c > /dev/null && ./gcc_test.sh comparison2
+   EXECNOW: LOG gen_comparison.c BIN gen_comparison.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/comparison.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_comparison.c > /dev/null && ./gcc_runtime.sh comparison
+   EXECNOW: LOG gen_comparison2.c BIN gen_comparison2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/comparison.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_comparison2.c > /dev/null && ./gcc_runtime.sh comparison2
 */
 
 int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/false.i b/src/plugins/e-acsl/tests/e-acsl-runtime/false.i
index ddd9fdf50932f9814ebaef5a599501678f4d2165..4b551d0f45b00b45e73181cff0a15d7fa4e5d0d1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/false.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/false.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: assert \false
-   EXECNOW: LOG gen_false.c BIN gen_false.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/false.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_false.c > /dev/null && ./gcc_test.sh false
-   EXECNOW: LOG gen_false2.c BIN gen_false2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/false.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_false2.c > /dev/null && ./gcc_test.sh false2
+   EXECNOW: LOG gen_false.c BIN gen_false.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/false.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_false.c > /dev/null && ./gcc_runtime.sh false
+   EXECNOW: LOG gen_false2.c BIN gen_false2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/false.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_false2.c > /dev/null && ./gcc_runtime.sh false2
 */
 int main(void) {
   int x = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i b/src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i
index 0d5c159a5b4fa4d713226ab96db183c03a8b9e8f..c8e5ee4ee2441b609ffd34fb659312dff5c5e939 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: function contract
-   EXECNOW: LOG gen_function_contract.c BIN gen_function_contract.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/function_contract.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract.c > /dev/null && ./gcc_test.sh function_contract
-   EXECNOW: LOG gen_function_contract2.c BIN gen_function_contract2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/function_contract.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract2.c > /dev/null && ./gcc_test.sh function_contract2
+   EXECNOW: LOG gen_function_contract.c BIN gen_function_contract.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/function_contract.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract.c > /dev/null && ./gcc_runtime.sh function_contract
+   EXECNOW: LOG gen_function_contract2.c BIN gen_function_contract2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/function_contract.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract2.c > /dev/null && ./gcc_runtime.sh function_contract2
 */
 
 int X = 0, Y = 2;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/ghost.i b/src/plugins/e-acsl/tests/e-acsl-runtime/ghost.i
index 97b15b773adfd78d60c87d20936b9f9ae91f1192..85357b70a200dd68580b6a199d4e098dc46b1681 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/ghost.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/ghost.i
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: ghost code
    STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
-   EXECNOW: LOG gen_ghost.c BIN gen_ghost.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/ghost.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ghost.c > /dev/null && ./gcc_test.sh ghost
-   EXECNOW: LOG gen_ghost2.c BIN gen_ghost2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/ghost.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ghost2.c > /dev/null && ./gcc_test.sh ghost2
+   EXECNOW: LOG gen_ghost.c BIN gen_ghost.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/ghost.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ghost.c > /dev/null && ./gcc_runtime.sh ghost
+   EXECNOW: LOG gen_ghost2.c BIN gen_ghost2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/ghost.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ghost2.c > /dev/null && ./gcc_runtime.sh ghost2
 */
 
 /*@ ghost int G = 0; */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/init.c
index e7a5a17ddbb6c85997ea761ae6f789b4757d35cf..2a6e3753ef9cc436126342a0ba874b558759cb1a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/init.c
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: initialization of globals (bts #1818)
-   EXECNOW: LOG gen_init.c BIN gen_init.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/init.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_init.c > /dev/null && ./gcc_test.sh init
-   EXECNOW: LOG gen_init2.c BIN gen_init2.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/init.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_init2.c > /dev/null && ./gcc_test.sh init2
+   EXECNOW: LOG gen_init.c BIN gen_init.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/init.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_init.c > /dev/null && ./gcc_runtime.sh init
+   EXECNOW: LOG gen_init2.c BIN gen_init2.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/init.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_init2.c > /dev/null && ./gcc_runtime.sh init2
 */
 
 int a = 0, b;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i b/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
index 6086959108b1a8e8029d56591f7aaa3c1ae226b6..41a8312b6aadf3a13ac0285109cae2d67366c642 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: integer constant + a stmt after the assertion
-   EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/integer_constant.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && ./gcc_test.sh integer_constant
-   EXECNOW: LOG gen_integer_constant2.c BIN gen_integer_constant2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/integer_constant.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant2.c > /dev/null && ./gcc_test.sh integer_constant2
+   EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/integer_constant.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && ./gcc_runtime.sh integer_constant
+   EXECNOW: LOG gen_integer_constant2.c BIN gen_integer_constant2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/integer_constant.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant2.c > /dev/null && ./gcc_runtime.sh integer_constant2
 */
 int main(void) {
   int x;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/invariant.i b/src/plugins/e-acsl/tests/e-acsl-runtime/invariant.i
index 3fef9625f7efe1bce234f66f7f4d2803d879915b..46b75dad8a9a74291bf97b8d28a94ecc8bfc0da4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/invariant.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/invariant.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: invariant
-   EXECNOW: LOG gen_invariant.c BIN gen_invariant.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/invariant.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_invariant.c > /dev/null && ./gcc_test.sh invariant
-   EXECNOW: LOG gen_invariant2.c BIN gen_invariant2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/invariant.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_invariant2.c > /dev/null && ./gcc_test.sh invariant2
+   EXECNOW: LOG gen_invariant.c BIN gen_invariant.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/invariant.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_invariant.c > /dev/null && ./gcc_runtime.sh invariant
+   EXECNOW: LOG gen_invariant2.c BIN gen_invariant2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/invariant.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_invariant2.c > /dev/null && ./gcc_runtime.sh invariant2
 */
 int main(void) {
   int x = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/labeled_stmt.i b/src/plugins/e-acsl/tests/e-acsl-runtime/labeled_stmt.i
index bdf237a110155440ea8f8142e68e292a1cd84294..f5db6c5fe9db8e2be714fa96409a167bf4623c3c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/labeled_stmt.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/labeled_stmt.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: labeled stmt and gotos
-   EXECNOW: LOG gen_labeled_stmt.c BIN gen_labeled_stmt.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/labeled_stmt.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_labeled_stmt.c > /dev/null && ./gcc_test.sh labeled_stmt
-   EXECNOW: LOG gen_labeled_stmt2.c BIN gen_labeled_stmt2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/labeled_stmt.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_labeled_stmt2.c > /dev/null && ./gcc_test.sh labeled_stmt2
+   EXECNOW: LOG gen_labeled_stmt.c BIN gen_labeled_stmt.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/labeled_stmt.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_labeled_stmt.c > /dev/null && ./gcc_runtime.sh labeled_stmt
+   EXECNOW: LOG gen_labeled_stmt2.c BIN gen_labeled_stmt2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/labeled_stmt.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_labeled_stmt2.c > /dev/null && ./gcc_runtime.sh labeled_stmt2
 */
 
 int X = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i b/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i
index 03088a0de66aaf95323899bb2e2a28ffeb33e396..2f93252af577a73247496eda732fea632737a2e3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: terms and predicates using lazy operators
-   EXECNOW: LOG gen_lazy.c BIN gen_lazy.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/lazy.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_lazy.c > /dev/null && ./gcc_test.sh lazy -Wno-div-by-zero
-   EXECNOW: LOG gen_lazy2.c BIN gen_lazy2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/lazy.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_lazy2.c > /dev/null && ./gcc_test.sh lazy2
+   EXECNOW: LOG gen_lazy.c BIN gen_lazy.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/lazy.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_lazy.c > /dev/null && ./gcc_runtime.sh lazy -Wno-div-by-zero
+   EXECNOW: LOG gen_lazy2.c BIN gen_lazy2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/lazy.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_lazy2.c > /dev/null && ./gcc_runtime.sh lazy2
 */
 
 int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i b/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i
index 00899cadc065621580f8067f32614daec77654ee..4f72855791d3a54ddfbcff322451890de1db1df6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: linear search (example of the SAC'13 article)
-   EXECNOW: LOG gen_linear_search.c BIN gen_linear_search.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/linear_search.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_linear_search.c > /dev/null && ./gcc_test.sh linear_search
-   EXECNOW: LOG gen_linear_search2.c BIN gen_linear_search2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/linear_search.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_linear_search2.c > /dev/null && ./gcc_test.sh linear_search2
+   EXECNOW: LOG gen_linear_search.c BIN gen_linear_search.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/linear_search.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_linear_search.c > /dev/null && ./gcc_runtime.sh linear_search
+   EXECNOW: LOG gen_linear_search2.c BIN gen_linear_search2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/linear_search.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_linear_search2.c > /dev/null && ./gcc_runtime.sh linear_search2
 */
 
 int A[10];
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/literal_string.i b/src/plugins/e-acsl/tests/e-acsl-runtime/literal_string.i
index f697c02499be8e0f18cff2a776e2763a4bcf83b0..a089360b58b03e52eda81887cd11a2efbc572ec5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/literal_string.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/literal_string.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: literal string
-   EXECNOW: LOG gen_literal_string.c BIN gen_literal_string.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/literal_string.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_literal_string.c > /dev/null && ./gcc_test.sh literal_string
-   EXECNOW: LOG gen_literal_string2.c BIN gen_literal_string2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/literal_string.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_literal_string2.c > /dev/null && ./gcc_test.sh literal_string2
+   EXECNOW: LOG gen_literal_string.c BIN gen_literal_string.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/literal_string.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_literal_string.c > /dev/null && ./gcc_runtime.sh literal_string
+   EXECNOW: LOG gen_literal_string2.c BIN gen_literal_string2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/literal_string.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_literal_string2.c > /dev/null && ./gcc_runtime.sh literal_string2
 */
 
 int main(void);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c
index 02904fa622218ad0f9e1db8b1e3eafd97e0b2a8d..24d11e3ff91525c99c955a5d8bc7b39a7fa5ec0f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: allocation and de-allocation of local variables
    STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
-   EXECNOW: LOG gen_localvar.c BIN gen_localvar.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/localvar.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_localvar.c > /dev/null && ./gcc_test.sh localvar
-   EXECNOW: LOG gen_localvar2.c BIN gen_localvar2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/localvar.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_localvar2.c > /dev/null && ./gcc_test.sh localvar2
+   EXECNOW: LOG gen_localvar.c BIN gen_localvar.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/localvar.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_localvar.c > /dev/null && ./gcc_runtime.sh localvar
+   EXECNOW: LOG gen_localvar2.c BIN gen_localvar2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/localvar.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_localvar2.c > /dev/null && ./gcc_runtime.sh localvar2
 */
 
 #include <stdlib.h>
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/longlong.i b/src/plugins/e-acsl/tests/e-acsl-runtime/longlong.i
index ddd020a83a05c5b0ddc86a3a105726154b6f7d84..ae2b3343a9667d29683806083254b85615b41bb9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/longlong.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/longlong.i
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: upgrading longlong to GMP
    STDOPT: +"-val-ignore-recursive-calls"
-   EXECNOW: LOG gen_longlong.c BIN gen_longlong.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/longlong.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_longlong.c > /dev/null && ./gcc_test.sh longlong
-   EXECNOW: LOG gen_longlong2.c BIN gen_longlong2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/longlong.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_longlong2.c > /dev/null && ./gcc_test.sh longlong2
+   EXECNOW: LOG gen_longlong.c BIN gen_longlong.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/longlong.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_longlong.c > /dev/null && ./gcc_runtime.sh longlong
+   EXECNOW: LOG gen_longlong2.c BIN gen_longlong2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/longlong.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_longlong2.c > /dev/null && ./gcc_runtime.sh longlong2
 */
 
 unsigned long long my_pow(unsigned int x, unsigned int n) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/loop.i b/src/plugins/e-acsl/tests/e-acsl-runtime/loop.i
index 62362a20271bb320f927450f682020eee6dace10..85ed22b976cf08caf129b09bc4cd15fc1d5bed72 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/loop.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/loop.i
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: loop invariants
    STDOPT: +"-slevel 160"
-   EXECNOW: LOG gen_loop.c BIN gen_loop.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/loop.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_loop.c > /dev/null && ./gcc_test.sh loop
-   EXECNOW: LOG gen_loop2.c BIN gen_loop2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/loop.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_loop2.c > /dev/null && ./gcc_test.sh loop2
+   EXECNOW: LOG gen_loop.c BIN gen_loop.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/loop.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_loop.c > /dev/null && ./gcc_runtime.sh loop
+   EXECNOW: LOG gen_loop2.c BIN gen_loop2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/loop.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_loop2.c > /dev/null && ./gcc_runtime.sh loop2
 */
 
 void simple_loop() {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.c b/src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.c
index 3a4801a487cc7fba78f9fa718a888b79217f02d9..7f57e55df1d5e8c51e201154ae1eac7f2e187860 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.c
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: the contents of argv should be valid
-   EXECNOW: LOG gen_mainargs.c BIN gen_mainargs.out @frama-c@ -machdep x86_64 -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/mainargs.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_mainargs.c > /dev/null && ./gcc_test.sh mainargs "" bar baz
-   EXECNOW: LOG gen_mainargs2.c BIN gen_mainargs2.out @frama-c@ -machdep x86_64 -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/mainargs.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_mainargs2.c > /dev/null && ./gcc_test.sh mainargs2 "" bar baz
+   EXECNOW: LOG gen_mainargs.c BIN gen_mainargs.out @frama-c@ -machdep x86_64 -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/mainargs.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_mainargs.c > /dev/null && ./gcc_runtime.sh mainargs "" bar baz
+   EXECNOW: LOG gen_mainargs2.c BIN gen_mainargs2.out @frama-c@ -machdep x86_64 -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/mainargs.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_mainargs2.c > /dev/null && ./gcc_runtime.sh mainargs2 "" bar baz
 */
 
 #include <string.h>
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/nested_code_annot.i b/src/plugins/e-acsl/tests/e-acsl-runtime/nested_code_annot.i
index f8d57792aff9b74b78235ff0880ada573bc72294..ccb46a1f663f3d5b941f94e5c01467ba9e9a8fcf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/nested_code_annot.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/nested_code_annot.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: structured stmt with several code annotations inside
-   EXECNOW: LOG gen_nested_code_annot.c BIN gen_nested_code_annot.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/nested_code_annot.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_nested_code_annot.c > /dev/null && ./gcc_test.sh nested_code_annot
-   EXECNOW: LOG gen_nested_code_annot2.c BIN gen_nested_code_annot2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/nested_code_annot.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_nested_code_annot2.c > /dev/null && ./gcc_test.sh nested_code_annot2
+   EXECNOW: LOG gen_nested_code_annot.c BIN gen_nested_code_annot.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/nested_code_annot.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_nested_code_annot.c > /dev/null && ./gcc_runtime.sh nested_code_annot
+   EXECNOW: LOG gen_nested_code_annot2.c BIN gen_nested_code_annot2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/nested_code_annot.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_nested_code_annot2.c > /dev/null && ./gcc_runtime.sh nested_code_annot2
 */
 
 int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/not.i b/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
index 046a6c3cdad356d7432b4c9a9af929b97ba660a6..96476d72b09808d0793c56fde0a03f4c5f78a9e0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: predicate [!p]
-   EXECNOW: LOG gen_not.c BIN gen_not.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/not.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_not.c > /dev/null && ./gcc_test.sh not
-   EXECNOW: LOG gen_not2.c BIN gen_not2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/not.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_not2.c > /dev/null && ./gcc_test.sh not2
+   EXECNOW: LOG gen_not.c BIN gen_not.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/not.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_not.c > /dev/null && ./gcc_runtime.sh not
+   EXECNOW: LOG gen_not2.c BIN gen_not2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/not.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_not2.c > /dev/null && ./gcc_runtime.sh not2
 */
 int main(void) {
   int x = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/null.i b/src/plugins/e-acsl/tests/e-acsl-runtime/null.i
index f2606546a1738666c9806b1f7b7bf2b0b9a64be1..ff0a29e637cfecf3f31e05bd39f0353a5ec5fd2f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/null.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/null.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: assert \null == 0
-   EXECNOW: LOG gen_null.c BIN gen_null.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/null.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_null.c > /dev/null && ./gcc_test.sh null
-   EXECNOW: LOG gen_null2.c BIN gen_null2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/null.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_null2.c > /dev/null && ./gcc_test.sh null2
+   EXECNOW: LOG gen_null.c BIN gen_null.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/null.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_null.c > /dev/null && ./gcc_runtime.sh null
+   EXECNOW: LOG gen_null2.c BIN gen_null2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/null.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_null2.c > /dev/null && ./gcc_runtime.sh null2
 */
 
 int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/other_constants.i b/src/plugins/e-acsl/tests/e-acsl-runtime/other_constants.i
index 84ae5db6f06cb9967414cf47dab30f08fe032501..86759b11e3156fdbf7d8908034e1e744c7779fbb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/other_constants.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/other_constants.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: non integer constants
-   EXECNOW: LOG gen_other_constants.c BIN gen_other_constants.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/other_constants.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_other_constants.c > /dev/null && ./gcc_test.sh other_constants
-   EXECNOW: LOG gen_other_constants2.c BIN gen_other_constants2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/other_constants.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_other_constants2.c > /dev/null && ./gcc_test.sh other_constants2
+   EXECNOW: LOG gen_other_constants.c BIN gen_other_constants.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/other_constants.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_other_constants.c > /dev/null && ./gcc_runtime.sh other_constants
+   EXECNOW: LOG gen_other_constants2.c BIN gen_other_constants2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/other_constants.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_other_constants2.c > /dev/null && ./gcc_runtime.sh other_constants2
 */
 
 enum bool { false, true };
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/ptr.i b/src/plugins/e-acsl/tests/e-acsl-runtime/ptr.i
index 442dea94bc32347dfd72b4a66c002e8f9e77f6d3..1a25c90c0aea1b8263d6cf1fd5c9761337318a15 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/ptr.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/ptr.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: pointers and pointer arithmetic
-   EXECNOW: LOG gen_ptr.c BIN gen_ptr.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/ptr.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ptr.c > /dev/null && ./gcc_test.sh ptr
-   EXECNOW: LOG gen_ptr2.c BIN gen_ptr2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/ptr.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ptr2.c > /dev/null && ./gcc_test.sh ptr2
+   EXECNOW: LOG gen_ptr.c BIN gen_ptr.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/ptr.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ptr.c > /dev/null && ./gcc_runtime.sh ptr
+   EXECNOW: LOG gen_ptr2.c BIN gen_ptr2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/ptr.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ptr2.c > /dev/null && ./gcc_runtime.sh ptr2
 */
 
 int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/ptr_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/ptr_init.c
index 90576a4b9df26a3b88b53adb3c28b63f5b920202..60163f51c1e9181454e9ca99cdb23a6c715246e0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/ptr_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/ptr_init.c
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: initialized and function calls
    STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
-   EXECNOW: LOG gen_ptr_init.c BIN gen_ptr_init.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/ptr_init.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ptr_init.c > /dev/null && ./gcc_test.sh ptr_init
-   EXECNOW: LOG gen_ptr_init2.c BIN gen_ptr_init2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/ptr_init.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ptr_init2.c > /dev/null && ./gcc_test.sh ptr_init2
+   EXECNOW: LOG gen_ptr_init.c BIN gen_ptr_init.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/ptr_init.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ptr_init.c > /dev/null && ./gcc_runtime.sh ptr_init
+   EXECNOW: LOG gen_ptr_init2.c BIN gen_ptr_init2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/ptr_init.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ptr_init2.c > /dev/null && ./gcc_runtime.sh ptr_init2
 */
 
 #include "stdlib.h"
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/quantif.i b/src/plugins/e-acsl/tests/e-acsl-runtime/quantif.i
index 638d1e486fbf44992860242e2baf7500a68c37fa..069060d8d2e20395114f559792aa3678dcc0b2b8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/quantif.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/quantif.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: quantifiers
-   EXECNOW: LOG gen_quantif.c BIN gen_quantif.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/quantif.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_quantif.c > /dev/null && ./gcc_test.sh quantif
-   EXECNOW: LOG gen_quantif2.c BIN gen_quantif2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/quantif.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_quantif2.c > /dev/null && ./gcc_test.sh quantif2
+   EXECNOW: LOG gen_quantif.c BIN gen_quantif.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/quantif.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_quantif.c > /dev/null && ./gcc_runtime.sh quantif
+   EXECNOW: LOG gen_quantif2.c BIN gen_quantif2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/quantif.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_quantif2.c > /dev/null && ./gcc_runtime.sh quantif2
 */
 
 int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/result.i b/src/plugins/e-acsl/tests/e-acsl-runtime/result.i
index c714ac7815da7fd6fb7e07c4cbb3369d7d50101e..12f04ceec132415a4a447d86f0d8ba0e5f7aac14 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/result.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/result.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: \result
-   EXECNOW: LOG gen_result.c BIN gen_result.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/result.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_result.c > /dev/null && ./gcc_test.sh result
-   EXECNOW: LOG gen_result2.c BIN gen_result2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/result.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_result2.c > /dev/null && ./gcc_test.sh result2 -Wno-unused-but-set-variable
+   EXECNOW: LOG gen_result.c BIN gen_result.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/result.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_result.c > /dev/null && ./gcc_runtime.sh result
+   EXECNOW: LOG gen_result2.c BIN gen_result2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/result.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_result2.c > /dev/null && ./gcc_runtime.sh result2 -Wno-unused-but-set-variable
 */
 
 /*@ ensures \result == (int)(x - x); */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/sizeof.i b/src/plugins/e-acsl/tests/e-acsl-runtime/sizeof.i
index 631b542d7a190f5f7e573ccffeb47870b34288f9..59dc3db917257e50bf82f60eba06d199e5e8d2ab 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/sizeof.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/sizeof.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: sizeof
-   EXECNOW: LOG gen_sizeof.c BIN gen_sizeof.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/sizeof.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_sizeof.c > /dev/null && ./gcc_test.sh sizeof
-   EXECNOW: LOG gen_sizeof2.c BIN gen_sizeof2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/sizeof.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_sizeof2.c > /dev/null && ./gcc_test.sh sizeof2
+   EXECNOW: LOG gen_sizeof.c BIN gen_sizeof.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/sizeof.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_sizeof.c > /dev/null && ./gcc_runtime.sh sizeof
+   EXECNOW: LOG gen_sizeof2.c BIN gen_sizeof2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/sizeof.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_sizeof2.c > /dev/null && ./gcc_runtime.sh sizeof2
 */
 
 int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/stdout.c b/src/plugins/e-acsl/tests/e-acsl-runtime/stdout.c
index 7078d0e56a746f0c6476dca4c76c612dfd7d82fe..21c3e08bf613048ca416e089855c99d7988ab969 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/stdout.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/stdout.c
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: __fc_stdout
    STDOPT: #"-pp-annot"
-   EXECNOW: LOG gen_stdout.c BIN gen_stdout.out @frama-c@ -machdep x86_64 -pp-annot -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/stdout.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_stdout.c > /dev/null && ./gcc_test.sh stdout
-   EXECNOW: LOG gen_stdout2.c BIN gen_stdout2.out @frama-c@ -machdep x86_64 -pp-annot -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/stdout.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_stdout2.c > /dev/null && ./gcc_test.sh stdout2
+   EXECNOW: LOG gen_stdout.c BIN gen_stdout.out @frama-c@ -machdep x86_64 -pp-annot -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/stdout.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_stdout.c > /dev/null && ./gcc_runtime.sh stdout
+   EXECNOW: LOG gen_stdout2.c BIN gen_stdout2.out @frama-c@ -machdep x86_64 -pp-annot -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/stdout.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_stdout2.c > /dev/null && ./gcc_runtime.sh stdout2
 */
 
 #include<stdio.h>
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/stmt_contract.i b/src/plugins/e-acsl/tests/e-acsl-runtime/stmt_contract.i
index e96864c8455dad790d77c19671c55cdd589e92be..9c0cd4bd9bd63294e80fc8763a44932f8dc1f16e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/stmt_contract.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/stmt_contract.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: stmt contract
-   EXECNOW: LOG gen_stmt_contract.c BIN gen_stmt_contract.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/stmt_contract.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_stmt_contract.c > /dev/null && ./gcc_test.sh stmt_contract
-   EXECNOW: LOG gen_stmt_contract2.c BIN gen_stmt_contract2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/stmt_contract.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_stmt_contract2.c > /dev/null && ./gcc_test.sh stmt_contract2
+   EXECNOW: LOG gen_stmt_contract.c BIN gen_stmt_contract.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/stmt_contract.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_stmt_contract.c > /dev/null && ./gcc_runtime.sh stmt_contract
+   EXECNOW: LOG gen_stmt_contract2.c BIN gen_stmt_contract2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/stmt_contract.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_stmt_contract2.c > /dev/null && ./gcc_runtime.sh stmt_contract2
 */
 int main(void) {
   int x = 0, y = 2;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/true.i b/src/plugins/e-acsl/tests/e-acsl-runtime/true.i
index b6fb95c2e9439c40069e1c41da6f75591d82339b..1e7b96ed15cb3c4f88e426696e3aaf5285d7b474 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/true.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/true.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: assert \true
-   EXECNOW: LOG gen_true.c BIN gen_true.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/true.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_true.c > /dev/null && ./gcc_test.sh true
-   EXECNOW: LOG gen_true2.c BIN gen_true2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/true.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_true2.c > /dev/null && ./gcc_test.sh true2
+   EXECNOW: LOG gen_true.c BIN gen_true.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/true.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_true.c > /dev/null && ./gcc_runtime.sh true
+   EXECNOW: LOG gen_true2.c BIN gen_true2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/true.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_true2.c > /dev/null && ./gcc_runtime.sh true2
 */
 int main(void) {
   int x = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/typedef.i b/src/plugins/e-acsl/tests/e-acsl-runtime/typedef.i
index 7ff2a61a67634e50b70c337dd8fd093988d4385d..67dec6370db44c230a587712078e2bbd35693588 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/typedef.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/typedef.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: typedef (from a Bernard's bug report)
-   EXECNOW: LOG gen_typedef.c BIN gen_typedef.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/typedef.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_typedef.c > /dev/null && ./gcc_test.sh typedef
-   EXECNOW: LOG gen_typedef2.c BIN gen_typedef2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/typedef.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_typedef2.c > /dev/null && ./gcc_test.sh typedef2
+   EXECNOW: LOG gen_typedef.c BIN gen_typedef.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/typedef.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_typedef.c > /dev/null && ./gcc_runtime.sh typedef
+   EXECNOW: LOG gen_typedef2.c BIN gen_typedef2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/typedef.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_typedef2.c > /dev/null && ./gcc_runtime.sh typedef2
 */
 
 typedef unsigned char uint8;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
index aabd0f4977a265d148250a543f5f8d61dbe575c5..db9e09a076b76b7fd9566d8c8f5a886b6d6250f7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: \valid
    STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
-   EXECNOW: LOG gen_valid.c BIN gen_valid.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid.c > /dev/null && ./gcc_test.sh valid
-   EXECNOW: LOG gen_valid2.c BIN gen_valid2.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid2.c > /dev/null && ./gcc_test.sh valid2
+   EXECNOW: LOG gen_valid.c BIN gen_valid.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid.c > /dev/null && ./gcc_runtime.sh valid
+   EXECNOW: LOG gen_valid2.c BIN gen_valid2.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid2.c > /dev/null && ./gcc_runtime.sh valid2
 */
 
 #include "stdlib.h"
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c
index 169d13778611d3b8883663c50ab2a11794b6799d..b1f71d717ffe3839c4b9e8ff04ec446888bf1629 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: \valid in presence of aliasing
    STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
-   EXECNOW: LOG gen_valid_alias.c BIN gen_valid_alias.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_alias.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_alias.c > /dev/null && ./gcc_test.sh valid_alias
-   EXECNOW: LOG gen_valid_alias2.c BIN gen_valid_alias2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_alias.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_alias2.c > /dev/null && ./gcc_test.sh valid_alias2
+   EXECNOW: LOG gen_valid_alias.c BIN gen_valid_alias.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_alias.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_alias.c > /dev/null && ./gcc_runtime.sh valid_alias
+   EXECNOW: LOG gen_valid_alias2.c BIN gen_valid_alias2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_alias.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_alias2.c > /dev/null && ./gcc_runtime.sh valid_alias2
 */
 
 #include "stdlib.h"
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c
index dd9f7243e284359417fd7133faaa5906edd06cda..0d9017f796fac19ea2488261c1b22c0717e2eb73 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: function contract involving \valid
    STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
-   EXECNOW: LOG gen_valid_in_contract.c BIN gen_valid_in_contract.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_in_contract.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_in_contract.c > /dev/null && ./gcc_test.sh valid_in_contract
-   EXECNOW: LOG gen_valid_in_contract2.c BIN gen_valid_in_contract2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_in_contract.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_in_contract2.c > /dev/null && ./gcc_test.sh valid_in_contract2
+   EXECNOW: LOG gen_valid_in_contract.c BIN gen_valid_in_contract.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_in_contract.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_in_contract.c > /dev/null && ./gcc_runtime.sh valid_in_contract
+   EXECNOW: LOG gen_valid_in_contract2.c BIN gen_valid_in_contract2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_in_contract.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_in_contract2.c > /dev/null && ./gcc_runtime.sh valid_in_contract2
 */
 
 #include <stdlib.h>
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c
index d86ef57b989320be2d4c754d7a373a14fc15e93e..dcbcd63f998039beccdeaea000e573fcaa92b200 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: function call + initialized
    STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
-   EXECNOW: LOG gen_vector.c BIN gen_vector.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/vector.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_vector.c > /dev/null && ./gcc_test.sh vector
-   EXECNOW: LOG gen_vector2.c BIN gen_vector2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/vector.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_vector2.c > /dev/null && ./gcc_test.sh vector2
+   EXECNOW: LOG gen_vector.c BIN gen_vector.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/vector.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_vector.c > /dev/null && ./gcc_runtime.sh vector
+   EXECNOW: LOG gen_vector2.c BIN gen_vector2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/vector.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_vector2.c > /dev/null && ./gcc_runtime.sh vector2
 */
 
 #include<stdlib.h>