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 42c611babba9204a641953030ec827f30a0b9acf..d3b99cab2bae3ff9b297c3f3cd21d568f1941012 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i
@@ -1,6 +1,6 @@
/* 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_runtime.sh addrOf
+ COMMENT: no diff
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
*/
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 9919f2a34439f0e9ff1d15d6a0a1cf728666435e..f0e62abe25d44718e7425f175caaa96c73a0bf67 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/alias.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/alias.i
@@ -1,6 +1,6 @@
/* 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_runtime.sh alias
+ COMMENT: no diff
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
*/
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 793007db3ac6e1863a80df6ebc0fdd375bf5774b..91954d6142dbba12e1cb847ce2b3588d4df79e9a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/arith.i
@@ -1,7 +1,7 @@
/* 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_runtime.sh arith
+ COMMENT: no diff
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
*/
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 e6e805f9ad1705add962747265355dff1b5b4f15..2bd785a61358906e21937a63fa69b60f28752c26 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/array.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/array.i
@@ -1,7 +1,7 @@
/* 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_runtime.sh array
+ COMMENT: no diff
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
*/
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 6c4e69866e4f1a293a98cadd68daf50ec4497e8a..45d8548caec24ad8ba987cf0d9058df925a643b6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/at.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/at.i
@@ -1,6 +1,6 @@
/* 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_runtime.sh at -Wno-unused-label
+ COMMENT: no diff
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
*/
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 053d17c39d22f4e4e1b1388c1e7595c18a9b1b09..0d4fe90d0cdafd31a2f9c43e0d943b9f65c20966 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/call.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/call.c
@@ -1,13 +1,13 @@
/* 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_runtime.sh call
+ STDOPT: +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
+ COMMENT: no diff
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>
-extern void *malloc(unsigned int size);
+//extern void *malloc(unsigned int size);
/*@ ensures \valid(\result); */
int *f(int *x, int *y) {
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 b5f005b2ed4d11c5d521d2f3de00877ca4b00748..7e4c94d3a8ae2977ad5e464847d5995c8c0011e7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/cast.i
@@ -1,7 +1,7 @@
/* 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_runtime.sh cast
+ COMMENT: no diff
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
*/
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 3bae6308b5844ada219b99a3a15cdfaee9c0ee9a..9ee270ac380137148390a1583b7cb95769ae08f7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
@@ -1,6 +1,6 @@
/* 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_runtime.sh comparison
+ COMMENT: no diff
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
*/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/compound_initializers.c b/src/plugins/e-acsl/tests/e-acsl-runtime/compound_initializers.c
index c83b3eb4eff1bcd7dcd75889e050f0d26e044f61..6ef66ddcf55d4d9310964c894ae570253be1d779 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/compound_initializers.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/compound_initializers.c
@@ -1,6 +1,6 @@
/* run.config
COMMENT: Compound initializers
- EXECNOW: LOG gen_compound_initializers.c BIN gen_compound_initializers.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/compound_initializers.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_compound_initializers.c > /dev/null && ./gcc_runtime.sh compound_initializers
+ COMMENT: no diff
EXECNOW: LOG gen_compound_initializers2.c BIN gen_compound_initializers2.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/compound_initializers.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_compound_initializers2.c > /dev/null && ./gcc_runtime.sh compound_initializers2
*/
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 4b551d0f45b00b45e73181cff0a15d7fa4e5d0d1..f281753c78c0b7695b575938efad740289ff6f8a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/false.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/false.i
@@ -1,6 +1,6 @@
/* 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_runtime.sh false
+ COMMENT: no diff
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) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/freeable.c b/src/plugins/e-acsl/tests/e-acsl-runtime/freeable.c
index c5b020ec82962791d740c0e7d57134f1209c63ca..473a4f5928f72ecddbb07c56d19f036c9676d8e6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/freeable.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/freeable.c
@@ -1,7 +1,7 @@
/* run.config
COMMENT: \freeable
STDOPT: +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
- EXECNOW: LOG gen_freeable.c BIN gen_freeable.out @frama-c@ -machdep gcc_x86_64 -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/freeable.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_freeable.c > /dev/null && ./gcc_runtime.sh freeable
+ COMMENT: no diff
EXECNOW: LOG gen_freeable2.c BIN gen_freeable2.out @frama-c@ -machdep gcc_x86_64 -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/freeable.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_freeable2.c > /dev/null && ./gcc_runtime.sh freeable2
*/
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 c8e5ee4ee2441b609ffd34fb659312dff5c5e939..f027d045d7c9171e9a7c2b09abcf927cc17193d6 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,6 +1,6 @@
/* 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_runtime.sh function_contract
+ COMMENT: no diff
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
*/
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 85357b70a200dd68580b6a199d4e098dc46b1681..b4f36ed0ce6f29890266627919a106232f6ba035 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/ghost.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/ghost.i
@@ -1,7 +1,7 @@
/* 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_runtime.sh ghost
+ COMMENT: no diff
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
*/
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 2a6e3753ef9cc436126342a0ba874b558759cb1a..e2564d5c428d54ea49e9f441ae50667a7af43568 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/init.c
@@ -1,6 +1,6 @@
/* 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_runtime.sh init
+ COMMENT: no diff
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
*/
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 41a8312b6aadf3a13ac0285109cae2d67366c642..08c82dcb45fd314f6633b52f098cab4308fdfe18 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,6 +1,6 @@
/* 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_runtime.sh integer_constant
+ COMMENT: no diff
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) {
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 46b75dad8a9a74291bf97b8d28a94ecc8bfc0da4..71c48b93f550f2d962b30fe1cdae1d6906a852e3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/invariant.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/invariant.i
@@ -1,6 +1,6 @@
/* 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_runtime.sh invariant
+ STDOPT: +"-slevel 11"
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) {
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 f5db6c5fe9db8e2be714fa96409a167bf4623c3c..5047e5c57a0f9acaec0d0b524efaa95b8c2fc3e8 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,6 +1,6 @@
/* 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_runtime.sh labeled_stmt
+ COMMENT: no diff
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
*/
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 2f93252af577a73247496eda732fea632737a2e3..4b1e28a3ceb7d7b61ba2d323d37a5f636445b283 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i
@@ -1,6 +1,6 @@
/* 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_runtime.sh lazy -Wno-div-by-zero
+ COMMENT: no diff
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
*/
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 f0324f6405dc1d5800fb571a2439291f4085ee97..474fcf35d387469c6472331b28a785e58e3660ff 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,6 +1,6 @@
/* run.config
COMMENT: linear search (example from 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_runtime.sh linear_search
+ COMMENT: no diff
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
*/
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 a089360b58b03e52eda81887cd11a2efbc572ec5..281037444fecd15f3202bcfa48b4444406c4407b 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,6 +1,6 @@
/* 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_runtime.sh literal_string
+ COMMENT: no diff
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
*/
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 24d11e3ff91525c99c955a5d8bc7b39a7fa5ec0f..2cf19baf2246ab1211c08e53238070edc530aa0d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c
@@ -1,7 +1,7 @@
/* 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_runtime.sh localvar
+ COMMENT: no diff
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
*/
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 061276f4f38897578768573330ae281e37daa4ab..b1e87e04fbf7431e6d5d181f90e81de0f58bc6b3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/longlong.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/longlong.i
@@ -1,7 +1,7 @@
/* run.config
COMMENT: upgrading longlong to GMP
STDOPT: +"-no-eva -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_runtime.sh longlong
+ COMMENT: no diff
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
*/
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 85ed22b976cf08caf129b09bc4cd15fc1d5bed72..613c9161ef4b8449c46100fb0feca7ac99425456 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/loop.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/loop.i
@@ -1,7 +1,7 @@
/* 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_runtime.sh loop
+ COMMENT: no diff
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
*/
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 ea74ed80131302ec454c10cbe897db32239bf897..7b5a74dbacf319041bb11a5b0e3db85580b7b0bd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.c
@@ -1,6 +1,6 @@
/* 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 e-acsl-runtime mainargs "" bar baz
+ COMMENT: no diff
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 e-acsl-runtime mainargs2 "" bar baz
*/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/memsize.c b/src/plugins/e-acsl/tests/e-acsl-runtime/memsize.c
index 1d630e2aaaf89d6702f8fddc863e07b13eb16385..b4a9ee7cf2ffdf41d3f5f0784f7ab1224e695415 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/memsize.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/memsize.c
@@ -1,6 +1,6 @@
/* run.config
COMMENT: Checking heap memory size
- EXECNOW: LOG gen_memsize.c BIN gen_memsize.out @frama-c@ -machdep=gcc_x86_$(getconf LONG_BIT) -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/memsize.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_memsize.c > /dev/null && ./gcc_runtime.sh memsize
+ COMMENT: no diff
EXECNOW: LOG gen_memsize2.c BIN gen_memsize2.out @frama-c@ -machdep=gcc_x86_$(getconf LONG_BIT) -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/memsize.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_memsize2.c > /dev/null && ./gcc_runtime.sh memsize2
*/
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 ccb46a1f663f3d5b941f94e5c01467ba9e9a8fcf..4fa8d4b823e638a3503b6a5e22156a2389537eb6 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,6 +1,6 @@
/* 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_runtime.sh nested_code_annot
+ COMMENT: no diff
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
*/
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 96476d72b09808d0793c56fde0a03f4c5f78a9e0..ceb89ce41c9f67936f0e13a3e086e748bfe9b7c5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
@@ -1,6 +1,6 @@
/* 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_runtime.sh not
+ COMMENT: no diff
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) {
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 ff0a29e637cfecf3f31e05bd39f0353a5ec5fd2f..e342967ab54ce872bda4ef517b6a881bf4dd2733 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/null.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/null.i
@@ -1,6 +1,6 @@
/* 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_runtime.sh null
+ COMMENT: no diff
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
*/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle
index 22916af593bc51d099f1c9fbd3f61d3bc28369bf..2f92ef23f38a548b115f2586e2418e1eeeb38bff 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle
@@ -20,8 +20,10 @@
_E ∈ {44}
_G[0].str ∈ {{ "First" }}
[0].num ∈ {99}
+ [0].[bits 96 to 127] ∈ {0}
[1].str ∈ {{ "Second" }}
[1].num ∈ {147}
+ [1].[bits 96 to 127] ∈ {0}
__e_acsl_literal_string ∈ {0}
__e_acsl_literal_string_2 ∈ {0}
__e_acsl_literal_string_3 ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
index af4f3a3fd81e6a12e44cc40821871b136e2071d0..8518275cf6a97eee4492d4517ac1b3fde14716b1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -69,9 +69,9 @@ void f(void)
int m;
int *u;
int *p;
- __store_block((void *)(& p),4U);
- __store_block((void *)(& u),4U);
- __store_block((void *)(& m),4U);
+ __store_block((void *)(& p),8UL);
+ __store_block((void *)(& u),8UL);
+ __store_block((void *)(& m),4UL);
__full_init((void *)(& u));
u = & m;
__full_init((void *)(& p));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
index 2fde55817581fc8c604cb479e9dd71e9ee66fcb7..d76fcc5daf8c18e9693b747e247435fabdc1a174 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -71,8 +71,8 @@ predicate diffSize{L1, L2}(ℤ i) =
void f(int *dest, int val)
{
int *ptr;
- __store_block((void *)(& ptr),4U);
- __store_block((void *)(& dest),4U);
+ __store_block((void *)(& ptr),8UL);
+ __store_block((void *)(& dest),8UL);
__full_init((void *)(& ptr));
ptr = dest;
__initialize((void *)ptr,sizeof(int));
@@ -86,7 +86,7 @@ int main(void)
{
int __retres;
int i;
- __store_block((void *)(& i),4U);
+ __store_block((void *)(& i),4UL);
f(& i,255);
/*@ assert \initialized(&i); */
{
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
index 5514e19c20ca70b21b61efa166a1da16452842e4..a9c8583c31816d86f3a4bee64849263017612d31 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -56,14 +56,14 @@ int main(void)
e_acsl_assert(0 != ~ 0,(char *)"Assertion",(char *)"main",
(char *)"0 != ~0",14);
/*@ assert x+1 ≡ -2; */
- e_acsl_assert((long long)x + (long long)1 == (long long)(-2),
- (char *)"Assertion",(char *)"main",(char *)"x+1 == -2",16);
+ e_acsl_assert((long)x + (long)1 == (long)(-2),(char *)"Assertion",
+ (char *)"main",(char *)"x+1 == -2",16);
/*@ assert x-1 ≡ -4; */
- e_acsl_assert((long long)x - (long long)1 == (long long)(-4),
- (char *)"Assertion",(char *)"main",(char *)"x-1 == -4",17);
+ e_acsl_assert((long)x - (long)1 == (long)(-4),(char *)"Assertion",
+ (char *)"main",(char *)"x-1 == -4",17);
/*@ assert x*3 ≡ -9; */
- e_acsl_assert((long long)x * (long long)3 == (long long)(-9),
- (char *)"Assertion",(char *)"main",(char *)"x*3 == -9",18);
+ e_acsl_assert((long)x * (long)3 == (long)(-9),(char *)"Assertion",
+ (char *)"main",(char *)"x*3 == -9",18);
/*@ assert x/3 ≡ -1; */
e_acsl_assert(x / 3 == -1,(char *)"Assertion",(char *)"main",
(char *)"x/3 == -1",19);
@@ -80,10 +80,9 @@ int main(void)
e_acsl_assert(3 % -2 == 1,(char *)"Assertion",(char *)"main",
(char *)"3%-2 == 1",23);
/*@ assert ((x*2+(3+y))-4)+(x-y) ≡ -10; */
- e_acsl_assert((((long long)x * (long long)2 + ((long long)3 + (long long)y)) - (long long)4) + (
- (long long)x - (long long)y) == (long long)(-10),
- (char *)"Assertion",(char *)"main",
- (char *)"((x*2+(3+y))-4)+(x-y) == -10",25);
+ e_acsl_assert((((long)x * (long)2 + ((long)3 + (long)y)) - (long)4) + (
+ (long)x - (long)y) == (long)(-10),(char *)"Assertion",
+ (char *)"main",(char *)"((x*2+(3+y))-4)+(x-y) == -10",25);
/*@ assert (0≡1) ≡ !(0≡0); */
e_acsl_assert((0 == 1) == ! (0 == 0),(char *)"Assertion",(char *)"main",
(char *)"(0==1) == !(0==0)",27);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
index 35a2e76b508a8b21d03bd4bea1672e66d7dbb609..3cd3958c97934e1f2c1e4a037f18ab883065ef10 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
index 1d784f2cdacd7b24f031d181da7b793b91d7223c..51fe71d604b629cf5083def17d291706f2f0f340 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -114,8 +114,8 @@ void g(int *p, int *q)
int __e_acsl_at_3;
int __e_acsl_at_2;
int __e_acsl_at;
- __store_block((void *)(& p),4U);
- __store_block((void *)(& q),4U);
+ __store_block((void *)(& p),8UL);
+ __store_block((void *)(& q),8UL);
__initialize((void *)p,sizeof(int));
*p = 0;
__initialize((void *)(p + 1),sizeof(int));
@@ -128,7 +128,7 @@ void g(int *p, int *q)
__e_acsl_valid_read_3 = __valid_read((void *)q,sizeof(int));
e_acsl_assert(__e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(q)",34);
- __store_block((void *)(& __e_acsl_at_3),4U);
+ __store_block((void *)(& __e_acsl_at_3),4UL);
__e_acsl_at_3 = *q;
}
{
@@ -136,7 +136,7 @@ void g(int *p, int *q)
__e_acsl_valid_read = __valid_read((void *)q,sizeof(int));
e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(q)",32);
- __store_block((void *)(& __e_acsl_at),4U);
+ __store_block((void *)(& __e_acsl_at),4UL);
__e_acsl_at = *q;
}
__initialize((void *)p,sizeof(int));
@@ -152,7 +152,7 @@ void g(int *p, int *q)
sizeof(int));
e_acsl_assert(__e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(p+__e_acsl_at)",32);
- __store_block((void *)(& __e_acsl_at_2),4U);
+ __store_block((void *)(& __e_acsl_at_2),4UL);
__e_acsl_at_2 = *(p + __e_acsl_at);
}
A = 4;
@@ -179,7 +179,7 @@ void g(int *p, int *q)
/*@ ensures \result ≡ \old(x); */
int h(int x)
{
- __store_block((void *)(& x),4U);
+ __store_block((void *)(& x),4UL);
__delete_block((void *)(& x));
return x;
}
@@ -189,9 +189,9 @@ int __e_acsl_h(int x)
{
int __e_acsl_at;
int __retres;
- __store_block((void *)(& __retres),4U);
- __store_block((void *)(& x),4U);
- __store_block((void *)(& __e_acsl_at),4U);
+ __store_block((void *)(& __retres),4UL);
+ __store_block((void *)(& x),4UL);
+ __store_block((void *)(& __e_acsl_at),4UL);
__e_acsl_at = x;
__retres = h(x);
e_acsl_assert(__retres == __e_acsl_at,(char *)"Postcondition",(char *)"h",
@@ -204,21 +204,21 @@ int __e_acsl_h(int x)
int main(void)
{
int __e_acsl_at_3;
- long long __e_acsl_at_2;
+ long __e_acsl_at_2;
int __e_acsl_at;
int __retres;
int x;
int t[2];
- __store_block((void *)(t),8U);
- __store_block((void *)(& x),4U);
+ __store_block((void *)(t),8UL);
+ __store_block((void *)(& x),4UL);
__full_init((void *)(& x));
x = __e_acsl_h(0);
L:
- __store_block((void *)(& __e_acsl_at_3),4U);
+ __store_block((void *)(& __e_acsl_at_3),4UL);
__e_acsl_at_3 = x;
- __store_block((void *)(& __e_acsl_at_2),8U);
- __e_acsl_at_2 = (long long)x + (long long)1;
- __store_block((void *)(& __e_acsl_at),4U);
+ __store_block((void *)(& __e_acsl_at_2),8UL);
+ __e_acsl_at_2 = (long)x + (long)1;
+ __store_block((void *)(& __e_acsl_at),4UL);
__e_acsl_at = x;
/*@ assert x ≡ 0; */
e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",
@@ -232,12 +232,11 @@ int main(void)
e_acsl_assert(__e_acsl_at == 0,(char *)"Assertion",(char *)"main",
(char *)"\\at(x,L) == 0",53);
/*@ assert \at(x+1,L) ≡ 1; */
- e_acsl_assert(__e_acsl_at_2 == (long long)1,(char *)"Assertion",
- (char *)"main",(char *)"\\at(x+1,L) == 1",54);
+ e_acsl_assert(__e_acsl_at_2 == (long)1,(char *)"Assertion",(char *)"main",
+ (char *)"\\at(x+1,L) == 1",54);
/*@ assert \at(x,L)+1 ≡ 1; */
- e_acsl_assert((long long)__e_acsl_at_3 + (long long)1 == (long long)1,
- (char *)"Assertion",(char *)"main",
- (char *)"\\at(x,L)+1 == 1",55);
+ e_acsl_assert((long)__e_acsl_at_3 + (long)1 == (long)1,(char *)"Assertion",
+ (char *)"main",(char *)"\\at(x,L)+1 == 1",55);
g(t,& x);
__retres = 0;
__delete_block((void *)(t));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
index d8e01ffbb5d49b1671cfb6ccb5b22e510d764449..c9da637c446c2e771e4ecdce556f210ac53b9821 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -89,7 +89,7 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
- __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& __retres),8UL);
__retres = __malloc(size);
__delete_block((void *)(& __retres));
return __retres;
@@ -103,8 +103,8 @@ predicate diffSize{L1, L2}(ℤ i) =
/*@ ensures \valid(\result); */
int *f(int *x, int *y)
{
- __store_block((void *)(& x),4U);
- __store_block((void *)(& y),4U);
+ __store_block((void *)(& x),8UL);
+ __store_block((void *)(& y),8UL);
__initialize((void *)y,sizeof(int));
*y = 1;
__delete_block((void *)(& x));
@@ -116,9 +116,9 @@ int *f(int *x, int *y)
int *__e_acsl_f(int *x, int *y)
{
int *__retres;
- __store_block((void *)(& __retres),4U);
- __store_block((void *)(& x),4U);
- __store_block((void *)(& y),4U);
+ __store_block((void *)(& __retres),8UL);
+ __store_block((void *)(& x),8UL);
+ __store_block((void *)(& y),8UL);
__retres = f(x,y);
{
int __e_acsl_valid;
@@ -139,9 +139,9 @@ int main(void)
int *p;
int *q;
int *r;
- __store_block((void *)(& q),4U);
- __store_block((void *)(& p),4U);
- __store_block((void *)(& x),4U);
+ __store_block((void *)(& q),8UL);
+ __store_block((void *)(& p),8UL);
+ __store_block((void *)(& x),4UL);
__full_init((void *)(& x));
x = 0;
__full_init((void *)(& q));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
index 7ec7966af9338cf83a608049790b593c869f8dc4..b85ea90ad71c9bcf5497a77a2fe1996805586fd4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
index 3c38363e2138b328ca217fce8322bf5eab60bcc3..e286cdd283474517624ec5a6cd71f1931e8c9058 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
index f5f1034d24985c3bc201e90dc70fce0b443b0396..094195b28480bdc59a52592e07b2017b603e8d7e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
index a0f898886369d8a7f219edc1c72767a2d653b952..31d34663edeaa3a5749630ec7a6179db183a0c6e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
@@ -144,6 +144,7 @@ int main(void)
/*@ assert ¬\freeable(p); */
{
int __e_acsl_freeable;
+ /*@ assert Value: initialisation: \initialized(&p); */
__e_acsl_freeable = __freeable((void *)p);
e_acsl_assert(! __e_acsl_freeable,(char *)"Assertion",(char *)"main",
(char *)"!\\freeable(p)",15);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
index 02887746306ca35fc5d113bf4058dd65d33bcc52..d6b11cb3dc24caa1edc323a76aff077fd99b4e21 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -141,15 +141,15 @@ void __e_acsl_j(void)
{
e_acsl_assert(X == 5,(char *)"Precondition",(char *)"j",(char *)"X == 5",
29);
- e_acsl_assert((long long)X == (long long)3 + (long long)Y,
- (char *)"Precondition",(char *)"j",(char *)"X == 3+Y",32);
+ e_acsl_assert((long)X == (long)3 + (long)Y,(char *)"Precondition",
+ (char *)"j",(char *)"X == 3+Y",32);
e_acsl_assert(Y == 2,(char *)"Precondition",(char *)"j",(char *)"Y == 2",
33);
j();
e_acsl_assert(X == 3,(char *)"Postcondition",(char *)"j",(char *)"X == 3",
30);
- e_acsl_assert((long long)X == (long long)Y + (long long)1,
- (char *)"Postcondition",(char *)"j",(char *)"X == Y+1",34);
+ e_acsl_assert((long)X == (long)Y + (long)1,(char *)"Postcondition",
+ (char *)"j",(char *)"X == Y+1",34);
return;
}
@@ -197,7 +197,7 @@ void __e_acsl_k(void)
(char *)"X == 3 && Y == 2 ==> X == 3",44);
if (X == 3) __e_acsl_and_2 = Y == 2; else __e_acsl_and_2 = 0;
if (! __e_acsl_and_2) __e_acsl_implies_3 = 1;
- else __e_acsl_implies_3 = (long long)X + (long long)Y == (long long)5;
+ else __e_acsl_implies_3 = (long)X + (long)Y == (long)5;
e_acsl_assert(__e_acsl_implies_3,(char *)"Precondition",(char *)"k",
(char *)"X == 3 && Y == 2 ==> X+Y == 5",45);
k();
@@ -280,7 +280,7 @@ void __e_acsl_m(void)
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",(char *)"m",
(char *)"\\old(X == 5 && Y == 2) ==> X == 7",62);
if (! __e_acsl_at_3) __e_acsl_implies_3 = 1;
- else __e_acsl_implies_3 = (long long)X == (long long)__e_acsl_at_4 + (long long)Y;
+ else __e_acsl_implies_3 = (long)X == (long)__e_acsl_at_4 + (long)Y;
e_acsl_assert(__e_acsl_implies_3,(char *)"Postcondition",(char *)"m",
(char *)"\\old(X == 5 && Y == 2) ==> X == \\old(X)+Y",63);
return;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
index 7f0e671807c13441f13ca02fe5467a8326202627..dfded95706b3b15ce0397cba416a1a73e6bf5c11 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -88,9 +88,9 @@ int G = 0;
int *P;
void __e_acsl_memory_init(void)
{
- __store_block((void *)(& P),4U);
+ __store_block((void *)(& P),8UL);
__full_init((void *)(& P));
- __store_block((void *)(& G),4U);
+ __store_block((void *)(& G),4UL);
__full_init((void *)(& G));
return;
}
@@ -100,7 +100,7 @@ int main(void)
int __retres;
int *q;
__e_acsl_memory_init();
- __store_block((void *)(& q),4U);
+ __store_block((void *)(& q),8UL);
P = & G;
__full_init((void *)(& q));
q = P;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
index e817129f94b57a869ba8ddb422a7ff1911cb369e..19b3b6686d010108a7c5f994cc09ae150070dde6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
index 17edc7547d30849fc7fef2f5e0ab3023b91e59cd..edf5feae8bc38e4e03dc09e3611848c4ccaf0ea3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
index f9514e7699f98b9668297940f078ea39bbd6c5be..1f6cbd953ce861efb5867c7ca19f3fa9bb4bc973 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
index d3ce4ce6b8b7fa706b49dfb59460cc5c265a0fa0..61cb4b498e449087f296e51e1dbb8b2260901281 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
index 50947884763a4351ee0d1210b054de77acbe3179..d623377c687add3b9ceaf38bf7d206be18a32f35 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
index ec689d560787bfd68d91ecffbbb85fc06b802764..b4affde831db7c25829f211772f2ef1e32ab3d62 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
@@ -10,7 +10,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -129,11 +129,11 @@ void __e_acsl_memory_init(void)
__store_block((void *)__e_acsl_literal_string_2,sizeof("bar"));
__full_init((void *)__e_acsl_literal_string_2);
__literal_string((void *)__e_acsl_literal_string_2);
- __store_block((void *)(& S2),4U);
+ __store_block((void *)(& S2),8UL);
__full_init((void *)(& S2));
- __store_block((void *)(& S),4U);
+ __store_block((void *)(& S),8UL);
__full_init((void *)(& S));
- __store_block((void *)(& T),4U);
+ __store_block((void *)(& T),8UL);
__full_init((void *)(& T));
return;
}
@@ -143,7 +143,7 @@ int main(void)
int __retres;
char *SS;
__e_acsl_memory_init();
- __store_block((void *)(& SS),4U);
+ __store_block((void *)(& SS),8UL);
__full_init((void *)(& SS));
SS = (char *)__e_acsl_literal_string;
/*@ assert *(S+G2) ≡ 'o'; */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
index b012a7b28ffba5907f3d64e925207111a6b06b32..65eecad07e2f8703a6b7536b4cc61050b10b0237 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
struct list {
int element ;
struct list *next ;
@@ -102,7 +102,7 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
- __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& __retres),8UL);
__retres = __malloc(size);
__delete_block((void *)(& __retres));
return __retres;
@@ -116,8 +116,8 @@ predicate diffSize{L1, L2}(ℤ i) =
struct list *add(struct list *l, int i)
{
struct list *new;
- __store_block((void *)(& new),4U);
- __store_block((void *)(& l),4U);
+ __store_block((void *)(& new),8UL);
+ __store_block((void *)(& l),8UL);
__full_init((void *)(& new));
new = (struct list *)__e_acsl_malloc(sizeof(struct list));
/*@ assert \valid(new); */
@@ -148,7 +148,7 @@ int main(void)
{
int __retres;
struct list *l;
- __store_block((void *)(& l),4U);
+ __store_block((void *)(& l),8UL);
__full_init((void *)(& l));
l = (struct list *)0;
__full_init((void *)(& l));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
index acac3c564bb909bb30466ba9847de8fe3d767f20..fa24c65cd1814497095417e8725d0aae1151b0eb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -131,6 +131,8 @@ unsigned long long my_pow(unsigned int x, unsigned int n)
tmp_0 = my_pow(x,n / (unsigned int)2);
tmp = (int)tmp_0;
}
+ /*@ assert Value: signed_overflow: -2147483648 ≤ tmp*tmp; */
+ /*@ assert Value: signed_overflow: tmp*tmp ≤ 2147483647; */
tmp *= tmp;
if (n % (unsigned int)2 == (unsigned int)0) {
__retres = (unsigned long long)tmp;
@@ -158,7 +160,7 @@ int main(void)
unsigned long __e_acsl_4;
__gmpz_init_set_si(__e_acsl,(long)2);
__gmpz_init(__e_acsl_x);
- __gmpz_import(__e_acsl_x,1U,1,8U,0,0U,(void const *)(& x));
+ __gmpz_import(__e_acsl_x,1UL,1,8UL,0,0UL,(void const *)(& x));
__gmpz_init(__e_acsl_mul);
__gmpz_mul(__e_acsl_mul,(__mpz_struct const *)(__e_acsl),
(__mpz_struct const *)(__e_acsl_x));
@@ -176,6 +178,10 @@ int main(void)
__gmpz_tdiv_r(__e_acsl_mod,(__mpz_struct const *)(__e_acsl_add),
(__mpz_struct const *)(__e_acsl));
__e_acsl_4 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_mod));
+ /*@ assert
+ Value: ptr_comparison:
+ \pointer_comparable((void *)__e_acsl_4, (void *)1);
+ */
e_acsl_assert(__e_acsl_4 == 1,(char *)"Assertion",(char *)"main",
(char *)"(2*x+1)%2 == 1",19);
__gmpz_clear(__e_acsl);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
index 017d65d08d5ca775270cf50198ba6e46e306687e..bccbc7f1974197d2de40b74e8433c7a34c730363 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -106,7 +106,7 @@ void nested_loops(void)
e_acsl_assert(0 <= __e_acsl_k,(char *)"RTE",
(char *)"nested_loops",
(char *)"index_bound: 0 <= __e_acsl_k",21);
- if ((long long)t[__e_acsl_k][__e_acsl_l] == (long long)__e_acsl_k * (long long)__e_acsl_l)
+ if ((long)t[__e_acsl_k][__e_acsl_l] == (long)__e_acsl_k * (long)__e_acsl_l)
;
else {
__e_acsl_forall = 0;
@@ -159,7 +159,11 @@ void nested_loops(void)
e_acsl_assert(0 <= __e_acsl_k_2,(char *)"RTE",
(char *)"nested_loops",
(char *)"index_bound: 0 <= __e_acsl_k_2",21);
- if ((long long)t[__e_acsl_k_2][__e_acsl_l_2] == (long long)__e_acsl_k_2 * (long long)__e_acsl_l_2)
+ /*@ assert
+ Value: initialisation:
+ \initialized(&t[__e_acsl_k_2][__e_acsl_l_2]);
+ */
+ if ((long)t[__e_acsl_k_2][__e_acsl_l_2] == (long)__e_acsl_k_2 * (long)__e_acsl_l_2)
;
else {
__e_acsl_forall_2 = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
index 0e669f9d45241b210c1f25cf89653692f1ac1e94..d0ae231495a7a7c0405b8978db216182a4e6a9bb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
@@ -470,6 +470,7 @@ int main(int argc, char **argv)
__e_acsl_valid_read = __valid_read((void *)(argv + argc),sizeof(char *));
e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(argv+argc)",17);
+ /*@ assert Value: mem_access: \valid_read(argv+argc); */
e_acsl_assert(*(argv + argc) == (void *)0,(char *)"Assertion",
(char *)"main",(char *)"*(argv+argc) == \\null",17);
}
@@ -486,6 +487,7 @@ int main(int argc, char **argv)
sizeof(char *));
e_acsl_assert(__e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(argv+argc)",18);
+ /*@ assert Value: mem_access: \valid_read(argv+argc); */
__e_acsl_valid_4 = __valid((void *)*(argv + argc),sizeof(char));
__e_acsl_and = __e_acsl_valid_4;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
index f3bdecf27041c1435e609df8e25c86dda6a0eb81..8fe9bc262e8222efabdf9cba73a2565ee91d7711 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
index 4fe3c73b67c674ba40d01151765379894d692504..dd2c4e03f7fff905f1d010500804dd7821b6015f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
index a09b2333e5245328a47e607b26fad3b34f7ae9e2..d9590cff0ee096ef90154b6400dbbd5b92b1dccf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
index 3cfb1dca11d84e641a0036ec3fcb0a9b4798bbe0..e07ba68c2e885a2fdee888266042eacd112e3329 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
enum bool {
false = 0,
true = 1
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
index 856c8b3ced8ed0a91cd30192fc0a1d12fda13e7e..0c7c5a55ff7ffbf39593498106c86ec5f95cc8e2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -83,9 +83,9 @@ int main(void)
int x;
int t[3];
int *p;
- __store_block((void *)(& p),4U);
- __store_block((void *)(t),12U);
- __store_block((void *)(& x),4U);
+ __store_block((void *)(& p),8UL);
+ __store_block((void *)(t),12UL);
+ __store_block((void *)(& x),4UL);
__full_init((void *)(& x));
x = 1;
__initialize((void *)(t),sizeof(int));
@@ -130,19 +130,14 @@ int main(void)
(char *)"index_bound: i < 3",19);
e_acsl_assert(0 <= i,(char *)"RTE",(char *)"main",
(char *)"index_bound: 0 <= i",19);
- e_acsl_assert((long long)t[i] == (long long)i + (long long)2,
- (char *)"Assertion",(char *)"main",(char *)"t[i] == i+2",
- 19);
+ e_acsl_assert((long)t[i] == (long)i + (long)2,(char *)"Assertion",
+ (char *)"main",(char *)"t[i] == i+2",19);
/*@ assert t[2-i] ≡ 4-i; */
- e_acsl_assert((long long)2 - (long long)i < (long long)3,(char *)"RTE",
- (char *)"main",
- (char *)"index_bound: (long long)(2-(long long)i) < 3",
- 20);
- e_acsl_assert(0LL <= (long long)2 - (long long)i,(char *)"RTE",
- (char *)"main",
- (char *)"index_bound: 0 <= (long long)(2-(long long)i)",
- 20);
- e_acsl_assert((long long)t[(long long)2 - (long long)i] == (long long)4 - (long long)i,
+ e_acsl_assert((long)2 - (long)i < (long)3,(char *)"RTE",(char *)"main",
+ (char *)"index_bound: (long)(2-(long)i) < 3",20);
+ e_acsl_assert(0L <= (long)2 - (long)i,(char *)"RTE",(char *)"main",
+ (char *)"index_bound: 0 <= (long)(2-(long)i)",20);
+ e_acsl_assert((long)t[(long)2 - (long)i] == (long)4 - (long)i,
(char *)"Assertion",(char *)"main",
(char *)"t[2-i] == 4-i",20);
/*@ assert *(&t[2]-i) ≡ 4-i; */
@@ -152,7 +147,7 @@ int main(void)
sizeof(int));
e_acsl_assert(__e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(&t[2]-i)",21);
- e_acsl_assert((long long)*(& t[2] - i) == (long long)4 - (long long)i,
+ e_acsl_assert((long)*(& t[2] - i) == (long)4 - (long)i,
(char *)"Assertion",(char *)"main",
(char *)"*(&t[2]-i) == 4-i",21);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
index 7eba374f37b83e18e221e1675afa3a6442d0732a..7cc465121a5cca75e127f57a2fccdfe4d5758d57 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -87,7 +87,7 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
- __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& __retres),8UL);
__retres = __malloc(size);
__delete_block((void *)(& __retres));
return __retres;
@@ -109,7 +109,7 @@ void f(void)
void g(int *C, int *D)
{
/*@ assert \initialized(&C); */
- __store_block((void *)(& C),4U);
+ __store_block((void *)(& C),8UL);
e_acsl_assert(1,(char *)"Assertion",(char *)"g",
(char *)"\\initialized(&C)",19);
__delete_block((void *)(& C));
@@ -118,9 +118,9 @@ void g(int *C, int *D)
void __e_acsl_memory_init(void)
{
- __store_block((void *)(& B),4U);
+ __store_block((void *)(& B),8UL);
__full_init((void *)(& B));
- __store_block((void *)(& A),4U);
+ __store_block((void *)(& A),8UL);
__full_init((void *)(& A));
return;
}
@@ -131,8 +131,8 @@ int main(void)
int *x;
int *y;
__e_acsl_memory_init();
- __store_block((void *)(& y),4U);
- __store_block((void *)(& x),4U);
+ __store_block((void *)(& y),8UL);
+ __store_block((void *)(& x),8UL);
B = (int *)__e_acsl_malloc(sizeof(int));
__full_init((void *)(& y));
y = (int *)__e_acsl_malloc(sizeof(int));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
index b3e10d11118ae131a3f74767740287d909bb70db..ea196a0a7df50b9157d300cb02160bf256cf2d75 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
index e2992629f11b5c954e9c0b134993096a447fdd7e..3e20e4219a2a35ad2fea74eec095cec9d9a828d1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -55,7 +55,7 @@ int __e_acsl_f(int x)
__e_acsl_at_2 = x;
__e_acsl_at = x;
__retres = f(x);
- e_acsl_assert(__retres == (int)((long long)__e_acsl_at - (long long)__e_acsl_at_2),
+ e_acsl_assert(__retres == (int)((long)__e_acsl_at - (long)__e_acsl_at_2),
(char *)"Postcondition",(char *)"f",
(char *)"\\result == (int)(\\old(x)-\\old(x))",7);
return __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
index 7c3daa2acdceb95c1bbdddc0d17711abdfdd685e..32712cefda2e937c39aca7fd25491ac24bdaadc9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
index dbada0dda058055449e510f927e7765e00b196fa..591cdfd9e2d0c25db32e10a734b4d856c68afb21 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -84,17 +84,15 @@ int main(void)
{
e_acsl_assert(x == 5,(char *)"Precondition",(char *)"main",
(char *)"x == 5",24);
- e_acsl_assert((long long)x == (long long)3 + (long long)y,
- (char *)"Precondition",(char *)"main",(char *)"x == 3+y",
- 27);
+ e_acsl_assert((long)x == (long)3 + (long)y,(char *)"Precondition",
+ (char *)"main",(char *)"x == 3+y",27);
e_acsl_assert(y == 2,(char *)"Precondition",(char *)"main",
(char *)"y == 2",28);
x = 3;
e_acsl_assert(x == 3,(char *)"Postcondition",(char *)"main",
(char *)"x == 3",25);
- e_acsl_assert((long long)x == (long long)y + (long long)1,
- (char *)"Postcondition",(char *)"main",(char *)"x == y+1",
- 29);
+ e_acsl_assert((long)x == (long)y + (long)1,(char *)"Postcondition",
+ (char *)"main",(char *)"x == y+1",29);
}
/*@ behavior b1:
assumes x ≡ 1;
@@ -122,7 +120,7 @@ int main(void)
(char *)"x == 3 && y == 2 ==> x == 3",38);
if (x == 3) __e_acsl_and_2 = y == 2; else __e_acsl_and_2 = 0;
if (! __e_acsl_and_2) __e_acsl_implies_3 = 1;
- else __e_acsl_implies_3 = (long long)x + (long long)y == (long long)5;
+ else __e_acsl_implies_3 = (long)x + (long)y == (long)5;
e_acsl_assert(__e_acsl_implies_3,(char *)"Precondition",(char *)"main",
(char *)"x == 3 && y == 2 ==> x+y == 5",39);
x += y;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
index c7f61875787758513755bd9b4326dfd98efc3e98..3d5b43fc9495b9f146161f312ddbe61af1193ff5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
index 146b775b2f6bf29a8c7b7ccd6441a77c5e4f41d3..53194b31e9013ff174d9118037ad11f5b2e9e0de 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
typedef unsigned char uint8;
/*@ requires predicate ≢ 0;
assigns \nothing; */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
index aeef2091f8929b09f759b0997fed1aa7b0980417..c5dbe52c76fbfc25cf6a960cf5bc8dfe31264f75 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
@@ -565,6 +565,7 @@ int main(void)
__e_acsl_initialized_17 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_17) {
int __e_acsl_valid_18;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&a); */
__e_acsl_valid_18 = __valid((void *)a,sizeof(int));
__e_acsl_and_27 = __e_acsl_valid_18;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
index 9298497a1ff5db75741a00f45d3d769bf9f69bd1..ed699ad21ca0decf201ae3cc13428301fe1ed4aa 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -113,7 +113,7 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
- __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& __retres),8UL);
__retres = __malloc(size);
__delete_block((void *)(& __retres));
return __retres;
@@ -143,7 +143,7 @@ void __e_acsl_free(void *p)
int __e_acsl_at;
{
int __e_acsl_implies;
- __store_block((void *)(& p),4U);
+ __store_block((void *)(& p),8UL);
if (! (p != (void *)0)) __e_acsl_implies = 1;
else {
int __e_acsl_freeable;
@@ -152,7 +152,7 @@ void __e_acsl_free(void *p)
}
e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
(char *)"p != \\null ==> \\freeable(p)",178);
- __store_block((void *)(& __e_acsl_at),4U);
+ __store_block((void *)(& __e_acsl_at),4UL);
__e_acsl_at = p != (void *)0;
__free(p);
}
@@ -171,8 +171,8 @@ int main(void)
int *a;
int *b;
int n;
- __store_block((void *)(& b),4U);
- __store_block((void *)(& a),4U);
+ __store_block((void *)(& b),8UL);
+ __store_block((void *)(& a),8UL);
n = 0;
/*@ assert ¬\valid(a) ∧ ¬\valid(b); */
{
@@ -261,6 +261,7 @@ int main(void)
__e_acsl_initialized_6 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_6) {
int __e_acsl_valid_5;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&a); */
__e_acsl_valid_5 = __valid((void *)a,sizeof(int));
__e_acsl_and_8 = __e_acsl_valid_5;
}
@@ -271,6 +272,7 @@ int main(void)
__e_acsl_initialized_7 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_7) {
int __e_acsl_valid_6;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&b); */
__e_acsl_valid_6 = __valid((void *)b,sizeof(int));
__e_acsl_and_9 = __e_acsl_valid_6;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
index 6b59fc96e3cc0306e04073eddbe39a644a1e4818..7b34b898ab994142fff07a0b0a96bab3fffee6b3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
struct list {
int element ;
struct list *next ;
@@ -96,8 +96,8 @@ predicate diffSize{L1, L2}(ℤ i) =
struct list *f(struct list *l)
{
struct list *__retres;
- __store_block((void *)(& __retres),4U);
- __store_block((void *)(& l),4U);
+ __store_block((void *)(& __retres),8UL);
+ __store_block((void *)(& l),8UL);
if (l == (struct list *)0) {
__full_init((void *)(& __retres));
__retres = l;
@@ -132,9 +132,9 @@ struct list *__e_acsl_f(struct list *l)
struct list *__e_acsl_at_2;
int __e_acsl_at;
struct list *__retres;
- __store_block((void *)(& __retres),4U);
- __store_block((void *)(& l),4U);
- __store_block((void *)(& __e_acsl_at_4),4U);
+ __store_block((void *)(& __retres),8UL);
+ __store_block((void *)(& l),8UL);
+ __store_block((void *)(& __e_acsl_at_4),8UL);
__e_acsl_at_4 = l;
{
int __e_acsl_valid;
@@ -152,6 +152,7 @@ struct list *__e_acsl_f(struct list *l)
sizeof(struct list *));
e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"f",
(char *)"mem_access: \\valid_read(&l->next)",21);
+ /*@ assert Value: mem_access: \valid_read(&l->next); */
__e_acsl_valid_2 = __valid((void *)l->next,sizeof(struct list));
__e_acsl_and = __e_acsl_valid_2;
}
@@ -161,9 +162,9 @@ struct list *__e_acsl_f(struct list *l)
else __e_acsl_and_2 = 0;
__e_acsl_at_3 = __e_acsl_and_2;
}
- __store_block((void *)(& __e_acsl_at_2),4U);
+ __store_block((void *)(& __e_acsl_at_2),8UL);
__e_acsl_at_2 = l;
- __store_block((void *)(& __e_acsl_at),4U);
+ __store_block((void *)(& __e_acsl_at),4UL);
__e_acsl_at = l == (void *)0;
__retres = f(l);
{
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
index a26c08d266e91ab8a0978b18714f50348a7a2480..b68d6a103349a30bdae438f80a6ffcd37a14f573 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
@@ -6,7 +6,7 @@ struct __anonstruct___mpz_struct_1 {
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
+typedef unsigned long size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -97,7 +97,7 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
- __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& __retres),8UL);
__retres = __malloc(size);
__delete_block((void *)(& __retres));
return __retres;
@@ -127,7 +127,7 @@ void __e_acsl_free(void *p)
int __e_acsl_at;
{
int __e_acsl_implies;
- __store_block((void *)(& p),4U);
+ __store_block((void *)(& p),8UL);
if (! (p != (void *)0)) __e_acsl_implies = 1;
else {
int __e_acsl_freeable;
@@ -136,7 +136,7 @@ void __e_acsl_free(void *p)
}
e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
(char *)"p != \\null ==> \\freeable(p)",178);
- __store_block((void *)(& __e_acsl_at),4U);
+ __store_block((void *)(& __e_acsl_at),4UL);
__e_acsl_at = p != (void *)0;
__free(p);
}
@@ -154,9 +154,9 @@ int *new_inversed(int len, int *v)
{
int i;
int *p;
- __store_block((void *)(& p),4U);
+ __store_block((void *)(& p),8UL);
__full_init((void *)(& p));
- p = (int *)__e_acsl_malloc(sizeof(int) * (unsigned int)len);
+ p = (int *)__e_acsl_malloc(sizeof(int) * (unsigned long)len);
i = 0;
while (i < len) {
__initialize((void *)(p + i),sizeof(int));
@@ -173,8 +173,8 @@ int main(void)
int x;
int v1[3];
int *v2;
- __store_block((void *)(& v2),4U);
- __store_block((void *)(v1),12U);
+ __store_block((void *)(& v2),8UL);
+ __store_block((void *)(v1),12UL);
x = 3;
__initialize((void *)(v1),sizeof(int));
v1[0] = 1;
@@ -201,6 +201,7 @@ int main(void)
(char *)"\\initialized(v2+2)",29);
}
/*@ assert LAST ≡ 1; */
+ /*@ assert Value: initialisation: \initialized(&LAST); */
e_acsl_assert(LAST == 1,(char *)"Assertion",(char *)"main",
(char *)"LAST == 1",30);
__e_acsl_free((void *)v2);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.0.res.oracle
index c23dbf0116b90a43d690e5ac4edad3a1d95dc58f..f0d9dbf6c715c6fb6e5314a8a737295cb93f35a9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.0.res.oracle
@@ -10,8 +10,5 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/invariant.i:8:[value] entering loop for the first time
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/invariant.i:10:[kernel] warning: signed overflow. assert x+i ≤ 2147483647;
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
index 097c17aa47de4a463334f05f7d6bc509f5867f7d..4b0e3fa2ff8b4d7d988b352ed7f2926690aee934 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
@@ -10,11 +10,12 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/invariant.i:8:[value] entering loop for the first time
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_cmp
[value] using specification for function __gmpz_clear
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status invalid.
+tests/e-acsl-runtime/invariant.i:8:[value] entering loop for the first time
tests/e-acsl-runtime/invariant.i:10:[kernel] warning: signed overflow. assert x+i ≤ 2147483647;
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle
index 570e5a2cd7ddf866a6a3442f37e6d744e161c11d..7179ab8da9dfbb3ce4c88d0c3158e6d67ba9770c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle
@@ -28,6 +28,10 @@ tests/e-acsl-runtime/mainargs.c:14:[value] warning: assertion got status unknown
tests/e-acsl-runtime/mainargs.c:14:[value] entering loop for the first time
tests/e-acsl-runtime/mainargs.c:15:[value] warning: assertion got status unknown.
[value] using specification for function __block_length
+[value] using specification for function __gmpz_init_set_ui
+[value] using specification for function __gmpz_init_set_si
+[value] using specification for function __gmpz_cmp
+[value] using specification for function __gmpz_clear
tests/e-acsl-runtime/mainargs.c:17:[value] warning: assertion got status unknown.
[value] using specification for function __valid_read
tests/e-acsl-runtime/mainargs.c:17:[kernel] warning: out of bounds read. assert \valid_read(argv+argc);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle
index a0141f070c9fed6e0f9642d4663b8e597e06497d..f2f824e0e9b115cee8e1dfecdf4adda30c513b53 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle
@@ -22,26 +22,45 @@ FRAMAC_SHARE/libc/stdio.h:107:[e-acsl] warning: E-ACSL construct `logic function
__p_fc_fopen ∈ {{ &__fc_fopen[0] }}
__e_acsl_literal_string ∈ {0}
__e_acsl_literal_string_2 ∈ {0}
- S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
- [--..--]
- [0].[bits 80 to 95] ∈ UNINITIALIZED
+ S___fc_stdout[0].__fc_stdio_id ∈ [--..--]
+ [0].[bits 32 to 63] ∈ UNINITIALIZED
+ [0]{.__fc_position; .__fc_error; .__fc_eof} ∈ [--..--]
+ [0].[bits 144 to 159] ∈ UNINITIALIZED
[0].__fc_flags ∈ [--..--]
[0].__fc_inode ∈
{{ NULL ; &S___fc_inode_0_S___fc_stdout[0] }}
[0].__fc_real_data ∈
{{ NULL ; &S___fc_real_data_0_S___fc_stdout[0] }}
- {[0].__fc_real_data_max_size; [1]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof}} ∈
- [--..--]
- [1].[bits 80 to 95] ∈ UNINITIALIZED
+ [0].__fc_real_data_max_size ∈ [--..--]
+ [0].[bits 352 to 383] ∈ UNINITIALIZED
+ [1].__fc_stdio_id ∈ [--..--]
+ [1].[bits 32 to 63] ∈ UNINITIALIZED
+ [1]{.__fc_position; .__fc_error; .__fc_eof} ∈ [--..--]
+ [1].[bits 144 to 159] ∈ UNINITIALIZED
[1].__fc_flags ∈ [--..--]
[1].__fc_inode ∈
{{ NULL ; &S___fc_inode_1_S___fc_stdout[0] }}
[1].__fc_real_data ∈
{{ NULL ; &S___fc_real_data_1_S___fc_stdout[0] }}
[1].__fc_real_data_max_size ∈ [--..--]
- S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
+ [1].[bits 352 to 383] ∈ UNINITIALIZED
+ S___fc_inode_0_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev} ∈
+ [--..--]
+ [0].[bits 224 to 255] ∈ UNINITIALIZED
+ {[0]{.st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev}} ∈
+ [--..--]
+ [1].[bits 224 to 255] ∈ UNINITIALIZED
+ [1]{.st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks} ∈
+ [--..--]
S___fc_real_data_0_S___fc_stdout[0..1] ∈ [--..--]
- S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_inode_1_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev} ∈
+ [--..--]
+ [0].[bits 224 to 255] ∈ UNINITIALIZED
+ {[0]{.st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev}} ∈
+ [--..--]
+ [1].[bits 224 to 255] ∈ UNINITIALIZED
+ [1]{.st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks} ∈
+ [--..--]
S___fc_real_data_1_S___fc_stdout[0..1] ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
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 86759b11e3156fdbf7d8908034e1e744c7779fbb..66a141526d31c00c6e39aa90d20c3943a508c2df 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,6 +1,6 @@
/* 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_runtime.sh other_constants
+ COMMENT: no diff
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
*/
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 1a25c90c0aea1b8263d6cf1fd5c9761337318a15..a3f8f5176cc186f71d3fcd28a419357c735207f4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/ptr.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/ptr.i
@@ -1,6 +1,6 @@
/* 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_runtime.sh ptr
+ COMMENT: no diff
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
*/
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 60163f51c1e9181454e9ca99cdb23a6c715246e0..50f2049cb0a8a1615df1a52153a19e5ed87c2e35 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,7 +1,7 @@
/* 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_runtime.sh ptr_init
+ COMMENT: no diff
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
*/
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 069060d8d2e20395114f559792aa3678dcc0b2b8..afcac4ef3cda6a9d9f5033edfff9c32736023790 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/quantif.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/quantif.i
@@ -1,6 +1,6 @@
/* 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_runtime.sh quantif
+ COMMENT: no diff
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
*/
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 12f04ceec132415a4a447d86f0d8ba0e5f7aac14..4f966951aeae5319f1bcf4ac4db998f953306c9f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/result.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/result.i
@@ -1,6 +1,6 @@
/* 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_runtime.sh result
+ COMMENT: no diff
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
*/
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 59dc3db917257e50bf82f60eba06d199e5e8d2ab..b114e3ed8b7770b46d5ff633dab9da1c77a1c026 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/sizeof.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/sizeof.i
@@ -1,6 +1,6 @@
/* 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_runtime.sh sizeof
+ COMMENT: no diff
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
*/
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 d548394d253a3a74420e3c0d4434a4b47390d147..643f09508c1612d3f2ef0019e43cc1f6bde9ff4d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/stdout.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/stdout.c
@@ -1,7 +1,7 @@
/* run.config
COMMENT: __fc_stdout et __fc_fopen
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_runtime.sh stdout
+ COMMENT: no diff
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
*/
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 9c0cd4bd9bd63294e80fc8763a44932f8dc1f16e..52c30df93b250bfec0b27f0dcba2c18f436b7e5e 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,6 +1,6 @@
/* 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_runtime.sh stmt_contract
+ COMMENT: no diff
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) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
index 31618f99b7d448ba68098010412e63a4a40aaa34..ad3c03dc9ebcf9cc09926459b91744e54a41ef93 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
@@ -1,2 +1,4 @@
-OPT: -check -e-acsl -then-last -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
+LOG: gen_@PTEST_NAME@.c
+OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -print -ocode tests/e-acsl-runtime/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
+EXECNOW: ./scripts/testrun.sh @PTEST_NAME@ e-acsl-runtime
OPT: -check -e-acsl -e-acsl-gmp-only -then-last -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
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 1e7b96ed15cb3c4f88e426696e3aaf5285d7b474..c63ff066adf4fc60b1f8867f46c8518852ab9081 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/true.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/true.i
@@ -1,6 +1,6 @@
/* 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_runtime.sh true
+ COMMENT: no diff
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) {
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 67dec6370db44c230a587712078e2bbd35693588..dcd423e790b24fe2d4c2e827fac0f57c4d65dafb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/typedef.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/typedef.i
@@ -1,6 +1,6 @@
/* 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_runtime.sh typedef
+ COMMENT: no diff
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
*/
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 db9e09a076b76b7fd9566d8c8f5a886b6d6250f7..37d2b9ec5c2d3ae9287f1a3aba155036829064cb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
@@ -1,7 +1,7 @@
/* 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_runtime.sh valid
+ STDOPT: +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
+ COMMENT: no diff
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
*/
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 b1f71d717ffe3839c4b9e8ff04ec446888bf1629..d7aa926c1129dbce891c9d637bfeaf3eb6784d8a 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,7 +1,7 @@
/* 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_runtime.sh valid_alias
+ COMMENT: no diff
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
*/
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 0d9017f796fac19ea2488261c1b22c0717e2eb73..304a03f10ea69960a15de705a80de30bb170ea7b 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,7 +1,7 @@
/* 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_runtime.sh valid_in_contract
+ COMMENT: no diff
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
*/
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 dcbcd63f998039beccdeaea000e573fcaa92b200..370349e319b1923c3a5822ef0e33202ce1ad9f64 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c
@@ -1,7 +1,7 @@
/* 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_runtime.sh vector
+ COMMENT: no diff
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
*/