From f223a74ea36b9c0ab7de53f300051371ee9ba823 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 5 Feb 2016 19:41:18 +0100
Subject: [PATCH] [tests] Compare the generated code just after running Value.
Use gcc_x86_64 as machdep for all these tests. [tests] call testrun.sh in
test_config in order to compile and run the generated code. This code is no
more the one being compared with the oracle (see above item).
---
.../e-acsl/tests/e-acsl-runtime/addrOf.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/alias.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/arith.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/array.i | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/at.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/call.c | 6 +--
.../e-acsl/tests/e-acsl-runtime/cast.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/comparison.i | 2 +-
.../e-acsl-runtime/compound_initializers.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/false.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/freeable.c | 2 +-
.../tests/e-acsl-runtime/function_contract.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/ghost.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/init.c | 2 +-
.../tests/e-acsl-runtime/integer_constant.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/invariant.i | 2 +-
.../tests/e-acsl-runtime/labeled_stmt.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/lazy.i | 2 +-
.../tests/e-acsl-runtime/linear_search.i | 2 +-
.../tests/e-acsl-runtime/literal_string.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/localvar.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/longlong.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/loop.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/mainargs.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/memsize.c | 2 +-
.../tests/e-acsl-runtime/nested_code_annot.i | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/not.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/null.i | 2 +-
.../oracle/compound_initializers.0.res.oracle | 2 +
.../tests/e-acsl-runtime/oracle/gen_addrOf.c | 8 ++--
.../tests/e-acsl-runtime/oracle/gen_alias.c | 8 ++--
.../tests/e-acsl-runtime/oracle/gen_arith.c | 21 +++++----
.../tests/e-acsl-runtime/oracle/gen_array.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_at.c | 43 +++++++++----------
.../tests/e-acsl-runtime/oracle/gen_call.c | 20 ++++-----
.../tests/e-acsl-runtime/oracle/gen_cast.c | 2 +-
.../e-acsl-runtime/oracle/gen_comparison.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_false.c | 2 +-
.../e-acsl-runtime/oracle/gen_freeable.c | 1 +
.../oracle/gen_function_contract.c | 14 +++---
.../tests/e-acsl-runtime/oracle/gen_ghost.c | 8 ++--
.../oracle/gen_integer_constant.c | 2 +-
.../e-acsl-runtime/oracle/gen_invariant.c | 2 +-
.../e-acsl-runtime/oracle/gen_labeled_stmt.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_lazy.c | 2 +-
.../e-acsl-runtime/oracle/gen_linear_search.c | 2 +-
.../oracle/gen_literal_string.c | 10 ++---
.../e-acsl-runtime/oracle/gen_localvar.c | 10 ++---
.../e-acsl-runtime/oracle/gen_longlong.c | 10 ++++-
.../tests/e-acsl-runtime/oracle/gen_loop.c | 10 +++--
.../e-acsl-runtime/oracle/gen_mainargs.c | 2 +
.../oracle/gen_nested_code_annot.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_not.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_null.c | 2 +-
.../oracle/gen_other_constants.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_ptr.c | 29 ++++++-------
.../e-acsl-runtime/oracle/gen_ptr_init.c | 14 +++---
.../tests/e-acsl-runtime/oracle/gen_quantif.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_result.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_sizeof.c | 2 +-
.../e-acsl-runtime/oracle/gen_stmt_contract.c | 14 +++---
.../tests/e-acsl-runtime/oracle/gen_true.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_typedef.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_valid.c | 1 +
.../e-acsl-runtime/oracle/gen_valid_alias.c | 14 +++---
.../oracle/gen_valid_in_contract.c | 17 ++++----
.../tests/e-acsl-runtime/oracle/gen_vector.c | 17 ++++----
.../oracle/invariant.0.res.oracle | 3 --
.../oracle/invariant.1.res.oracle | 3 +-
.../oracle/mainargs.0.res.oracle | 4 ++
.../e-acsl-runtime/oracle/stdout.0.res.oracle | 35 +++++++++++----
.../tests/e-acsl-runtime/other_constants.i | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/ptr.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/ptr_init.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/quantif.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/result.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/sizeof.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/stdout.c | 2 +-
.../tests/e-acsl-runtime/stmt_contract.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/test_config | 4 +-
.../e-acsl/tests/e-acsl-runtime/true.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/typedef.i | 2 +-
.../e-acsl/tests/e-acsl-runtime/valid.c | 4 +-
.../e-acsl/tests/e-acsl-runtime/valid_alias.c | 2 +-
.../tests/e-acsl-runtime/valid_in_contract.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/vector.c | 2 +-
86 files changed, 242 insertions(+), 208 deletions(-)
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 42c611babba..d3b99cab2ba 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 9919f2a3443..f0e62abe25d 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 793007db3ac..91954d6142d 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 e6e805f9ad1..2bd785a6135 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 6c4e69866e4..45d8548caec 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 053d17c39d2..0d4fe90d0cd 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 b5f005b2ed4..7e4c94d3a8a 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 3bae6308b58..9ee270ac380 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 c83b3eb4eff..6ef66ddcf55 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 4b551d0f45b..f281753c78c 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 c5b020ec829..473a4f5928f 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 c8e5ee4ee24..f027d045d7c 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 85357b70a20..b4f36ed0ce6 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 2a6e3753ef9..e2564d5c428 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 41a8312b6aa..08c82dcb45f 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 46b75dad8a9..71c48b93f55 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 f5db6c5fe9d..5047e5c57a0 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 2f93252af57..4b1e28a3ceb 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 f0324f6405d..474fcf35d38 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 a089360b58b..281037444fe 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 24d11e3ff91..2cf19baf224 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 061276f4f38..b1e87e04fbf 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 85ed22b976c..613c9161ef4 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 ea74ed80131..7b5a74dbacf 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 1d630e2aaaf..b4a9ee7cf2f 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 ccb46a1f663..4fa8d4b823e 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 96476d72b09..ceb89ce41c9 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 ff0a29e637c..e342967ab54 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 22916af593b..2f92ef23f38 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 af4f3a3fd81..8518275cf6a 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 2fde5581758..d76fcc5daf8 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 5514e19c20c..a9c8583c318 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 35a2e76b508..3cd3958c979 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 1d784f2cdac..51fe71d604b 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 d8e01ffbb5d..c9da637c446 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 7ec7966af93..b85ea90ad71 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 3c38363e213..e286cdd2834 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 f5f1034d249..094195b2848 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 a0f89888636..31d34663ede 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 02887746306..d6b11cb3dc2 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 7f0e671807c..dfded95706b 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 e817129f94b..19b3b6686d0 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 17edc7547d3..edf5feae8bc 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 f9514e7699f..1f6cbd953ce 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 d3ce4ce6b8b..61cb4b498e4 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 50947884763..d623377c687 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 ec689d56078..b4affde831d 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 b012a7b28ff..65eecad07e2 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 acac3c564bb..fa24c65cd18 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 017d65d08d5..bccbc7f1974 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 0e669f9d452..d0ae231495a 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 f3bdecf2704..8fe9bc262e8 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 4fe3c73b67c..dd2c4e03f7f 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 a09b2333e52..d9590cff0ee 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 3cfb1dca11d..e07ba68c2e8 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 856c8b3ced8..0c7c5a55ff7 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 7eba374f37b..7cc465121a5 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 b3e10d11118..ea196a0a7df 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 e2992629f11..3e20e4219a2 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 7c3daa2acdc..32712cefda2 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 dbada0dda05..591cdfd9e2d 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 c7f61875787..3d5b43fc949 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 146b775b2f6..53194b31e90 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 aeef2091f89..c5dbe52c76f 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 9298497a1ff..ed699ad21ca 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 6b59fc96e3c..7b34b898ab9 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 a26c08d266e..b68d6a10334 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 c23dbf0116b..f0d9dbf6c71 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 097c17aa47d..4b0e3fa2ff8 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 570e5a2cd7d..7179ab8da9d 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 a0141f070c9..f2f824e0e9b 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 86759b11e31..66a141526d3 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 1a25c90c0ae..a3f8f5176cc 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 60163f51c1e..50f2049cb0a 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 069060d8d2e..afcac4ef3cd 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 12f04ceec13..4f966951aea 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 59dc3db9172..b114e3ed8b7 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 d548394d253..643f09508c1 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 9c0cd4bd9bd..52c30df93b2 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 31618f99b7d..ad3c03dc9eb 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 1e7b96ed15c..c63ff066adf 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 67dec6370db..dcd423e790b 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 db9e09a076b..37d2b9ec5c2 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 b1f71d717ff..d7aa926c112 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 0d9017f796f..304a03f10ea 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 dcbcd63f998..370349e319b 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
*/
--
GitLab