diff --git a/src/plugins/e-acsl/tests/bts/bts1304.i b/src/plugins/e-acsl/tests/bts/bts1304.i
index a32a26d4b84c6348d0f3edcfb9eb2926e96ba97e..b8db0455bbb31ee306ec15243a5a80d6003b877c 100644
--- a/src/plugins/e-acsl/tests/bts/bts1304.i
+++ b/src/plugins/e-acsl/tests/bts/bts1304.i
@@ -1,7 +1,7 @@
/* run.config
COMMENT: argument of functions must be kept, so keep its parameter
- EXECNOW: LOG gen_bts1304.c BIN gen_bts1304.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1304.i -constfold -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1304.c > /dev/null && ./gcc_bts.sh bts1304
- EXECNOW: LOG gen_bts13042.c BIN gen_bts13042.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1304.i -constfold -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13042.c > /dev/null && ./gcc_bts.sh bts13042
+ COMMENT: no diff
+ COMMENT: no diff
*/
struct msgA { int type; int a[2]; };
diff --git a/src/plugins/e-acsl/tests/bts/bts1307.i b/src/plugins/e-acsl/tests/bts/bts1307.i
index 2e3cabdd70b0874b3c368204b85ea05edd0694ae..96e3e82febe66f5130c4de8938e654718b605f7b 100644
--- a/src/plugins/e-acsl/tests/bts/bts1307.i
+++ b/src/plugins/e-acsl/tests/bts/bts1307.i
@@ -1,7 +1,7 @@
/* run.config
COMMENT: spec with floats and reals
- EXECNOW: LOG gen_bts1307.c BIN gen_bts1307.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1307.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1307.c > /dev/null && ./gcc_bts.sh bts1307
- EXECNOW: LOG gen_bts13072.c BIN gen_bts13072.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1307.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13072.c > /dev/null && ./gcc_bts.sh bts13072
+ COMMENT: no diff
+ COMMENT: no diff
*/
/*@ requires \valid(Mtmax_in);
diff --git a/src/plugins/e-acsl/tests/bts/bts1324.i b/src/plugins/e-acsl/tests/bts/bts1324.i
index 9b444f126b0cd79eb5b48ff5ab60e82b8b220dcb..c3419dbad8128e7a7c71aea546bc708839dca9dc 100644
--- a/src/plugins/e-acsl/tests/bts/bts1324.i
+++ b/src/plugins/e-acsl/tests/bts/bts1324.i
@@ -1,7 +1,7 @@
/* run.config
COMMENT: fixed bug with typing of universal quantification
- EXECNOW: LOG gen_bts1324.c BIN gen_bts1324.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1324.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1324.c > /dev/null && ./gcc_bts.sh bts1324
- EXECNOW: LOG gen_bts13242.c BIN gen_bts13242.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1324.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13242.c > /dev/null && ./gcc_bts.sh bts13242
+ COMMENT: no diff
+ COMMENT: no diff
*/
/*@ behavior yes:
diff --git a/src/plugins/e-acsl/tests/bts/bts1326.i b/src/plugins/e-acsl/tests/bts/bts1326.i
index b18101c3d1017c34fda38cdc5abb67bdfa4d3b36..83217a8101be1e96baec46f4a687455ce0ff195c 100644
--- a/src/plugins/e-acsl/tests/bts/bts1326.i
+++ b/src/plugins/e-acsl/tests/bts/bts1326.i
@@ -1,7 +1,7 @@
/* run.config
COMMENT: complex term left-values
- EXECNOW: LOG gen_bts1326.c BIN gen_bts1326.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1326.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1326.c > /dev/null && ./gcc_bts.sh bts1326
- EXECNOW: LOG gen_bts13262.c BIN gen_bts13262.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1326.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13262.c > /dev/null && ./gcc_bts.sh bts13262
+ COMMENT: no diff
+ COMMENT: no diff
*/
typedef int ArrayInt[5];
diff --git a/src/plugins/e-acsl/tests/bts/bts1390.c b/src/plugins/e-acsl/tests/bts/bts1390.c
index 5ff6dc147983e8f9ad5de360a38460fb786a3325..10f48b9f930c9a43814949b2a21a70899a41f916 100644
--- a/src/plugins/e-acsl/tests/bts/bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/bts1390.c
@@ -1,8 +1,8 @@
/* run.config
COMMENT: bts #1390, issue with typing of quantified variables
- STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
- EXECNOW: LOG gen_bts1390.c BIN gen_bts1390.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1390.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1390.c > /dev/null && ./gcc_bts.sh bts1390
- EXECNOW: LOG gen_bts13902.c BIN gen_bts13902.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1390.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13902.c > /dev/null && ./gcc_bts.sh bts13902
+ COMMENT: no diff
+ COMMENT: no diff
+ COMMENT: no diff
*/
#include "stdlib.h"
diff --git a/src/plugins/e-acsl/tests/bts/bts1398.c b/src/plugins/e-acsl/tests/bts/bts1398.c
index d02bb8faa91f9272d7cb386afdb6c6b63a8b8de3..c8659d7e87e0ea02c493723b7f701ae91698feb3 100644
--- a/src/plugins/e-acsl/tests/bts/bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/bts1398.c
@@ -1,8 +1,8 @@
/* run.config
COMMENT: variadic function call
- STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
- EXECNOW: LOG gen_bts1398.c BIN gen_bts1398.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1398.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1398.c > /dev/null && ./gcc_bts.sh bts1398 > /dev/null
- EXECNOW: LOG gen_bts13982.c BIN gen_bts13982.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1398.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13982.c > /dev/null && ./gcc_bts.sh bts13982 > /dev/null
+ COMMENT: no diff
+ COMMENT: no diff
+ COMMENT: no diff
*/
#include "stdio.h"
diff --git a/src/plugins/e-acsl/tests/bts/bts1399.c b/src/plugins/e-acsl/tests/bts/bts1399.c
index 43300c93834cf06f063649d63505a1b7356941d8..3c3c7145572def2c774e8dcf228fa5c82d350eda 100644
--- a/src/plugins/e-acsl/tests/bts/bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/bts1399.c
@@ -1,8 +1,8 @@
/* run.config
COMMENT: complex fields and indexes + potential RTE in \initialized
- STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
- EXECNOW: LOG gen_bts1399.c BIN gen_bts1399.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1399.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1399.c > /dev/null && ./gcc_bts.sh bts1399
- EXECNOW: LOG gen_bts13992.c BIN gen_bts13992.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1399.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13992.c > /dev/null && ./gcc_bts.sh bts13992
+ STDOPT: +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
+ COMMENT: no diff
+ COMMENT: no diff
*/
#include "stdlib.h"
diff --git a/src/plugins/e-acsl/tests/bts/bts1478.c b/src/plugins/e-acsl/tests/bts/bts1478.c
index 9b1bcd88bda4e4194f19b1c80af61dc9597eb1df..a453db4197ff92bfbd2cf1606df7a6939c7ea155 100644
--- a/src/plugins/e-acsl/tests/bts/bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/bts1478.c
@@ -1,7 +1,7 @@
/* run.config
COMMENT: bts #1478 about wrong detection of initializers in pre-analysis
- EXECNOW: LOG gen_bts1478.c BIN gen_bts1478.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1478.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1478.c > /dev/null && ./gcc_bts.sh bts1478
- EXECNOW: LOG gen_bts14782.c BIN gen_bts14782.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1478.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts14782.c > /dev/null && ./gcc_bts.sh bts14782
+ COMMENT: no diff
+ COMMENT: no diff
*/
int global_i;
diff --git a/src/plugins/e-acsl/tests/bts/bts1700.i b/src/plugins/e-acsl/tests/bts/bts1700.i
index 2534d1f1be441af6e5db9bcf7421015577fcb7f6..6257adbe85e3ec649f70515c8f3abe0676e987d4 100644
--- a/src/plugins/e-acsl/tests/bts/bts1700.i
+++ b/src/plugins/e-acsl/tests/bts/bts1700.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: pointer to an empty struct
- EXECNOW: LOG gen_bts1700.c BIN gen_bts1700.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1700.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1700.c > /dev/null && ./gcc_bts.sh bts1700
+ COMMENT: no diff
*/
struct toto {};
diff --git a/src/plugins/e-acsl/tests/bts/bts1717.i b/src/plugins/e-acsl/tests/bts/bts1717.i
index 99925f479ec5671173faae23491e201bd96db244..dd38513567d498d4d2e12425d408452b1cc91b8d 100644
--- a/src/plugins/e-acsl/tests/bts/bts1717.i
+++ b/src/plugins/e-acsl/tests/bts/bts1717.i
@@ -1,8 +1,8 @@
/* run.config
COMMENT: bts #1717, issue with labels on memory-related statements
- STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
- EXECNOW: LOG gen_bts1717.c BIN gen_bts1717.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1717.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1717.c > /dev/null && ./gcc_bts.sh bts1717
- EXECNOW: LOG gen_bts17172.c BIN gen_bts17172.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1717.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts17172.c > /dev/null && ./gcc_bts.sh bts17172
+ COMMENT: no diff
+ COMMENT: no diff
+ COMMENT: no diff
*/
int main(void) {
diff --git a/src/plugins/e-acsl/tests/bts/bts1718.i b/src/plugins/e-acsl/tests/bts/bts1718.i
index 0b13703f0a8a510aac910fe717bd0d90f897f230..2434f530b8607ff42c7032f45f1ed70bd1029cd9 100644
--- a/src/plugins/e-acsl/tests/bts/bts1718.i
+++ b/src/plugins/e-acsl/tests/bts/bts1718.i
@@ -1,8 +1,8 @@
/* run.config
COMMENT: bts #1718, issue regarding incorrect initialization of literal strings in global arrays with compound initializers
- STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
- EXECNOW: LOG gen_bts1718.c BIN gen_bts1718.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1718.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1718.c > /dev/null && ./gcc_bts.sh bts1718
- EXECNOW: LOG gen_bts17182.c BIN gen_bts17182.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1718.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts17182.c > /dev/null && ./gcc_bts.sh bts17182
+ COMMENT: no diff
+ COMMENT: no diff
+ COMMENT: no diff
*/
int main(void) {
diff --git a/src/plugins/e-acsl/tests/bts/bts1837.i b/src/plugins/e-acsl/tests/bts/bts1837.i
index cb01fddd8fdbc7d16af21cbe03ac23bcab203473..a3c0d10f9d68a3516911bc30f381313d1dac224f 100644
--- a/src/plugins/e-acsl/tests/bts/bts1837.i
+++ b/src/plugins/e-acsl/tests/bts/bts1837.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: bts #1837, about initialization of literal strings
- EXECNOW: LOG gen_bts1837.c BIN gen_bts1837.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1837.i -e-acsl -then-last -print -ocode ./tests/bts/result/gen_bts1837.c > /dev/null && ./gcc_bts.sh bts1837
+ COMMENT: no diff
*/
char *S = "foo";
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
deleted file mode 100644
index c9fe27e8b98a7c222f15b81a2d62ba8922e56cac..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
+++ /dev/null
@@ -1,22 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
-[value] using specification for function __store_block
-tests/bts/bts1304.i:23:[value] entering loop for the first time
-[value] using specification for function __initialize
-[value] using specification for function __delete_block
-tests/bts/bts1304.i:25:[value] warning: assertion got status unknown.
-[value] using specification for function __initialized
-[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.
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
deleted file mode 100644
index c9fe27e8b98a7c222f15b81a2d62ba8922e56cac..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
+++ /dev/null
@@ -1,22 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
-[value] using specification for function __store_block
-tests/bts/bts1304.i:23:[value] entering loop for the first time
-[value] using specification for function __initialize
-[value] using specification for function __delete_block
-tests/bts/bts1304.i:25:[value] warning: assertion got status unknown.
-[value] using specification for function __initialized
-[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.
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
index 85cef0bc32432b6b63f4c57406e4a5e035b9c5dc..c9fe27e8b98a7c222f15b81a2d62ba8922e56cac 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
@@ -1,31 +1,22 @@
-[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1304.i (no preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __store_block
-tests/e-acsl-runtime/bts1304.i:23:[value] entering loop for the first time
+tests/bts/bts1304.i:23:[value] entering loop for the first time
[value] using specification for function __initialize
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1304.i:25:[value] Assertion got status unknown.
+tests/bts/bts1304.i:25:[value] warning: assertion got status unknown.
[value] using specification for function __initialized
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] 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 unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
-[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
deleted file mode 100644
index c7d6f581b9c68ae6cb484e6d6026f243808731a3..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
+++ /dev/null
@@ -1,27 +0,0 @@
-tests/bts/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
-[e-acsl] beginning translation.
-tests/bts/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
-tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
-tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
-[value] using specification for function __store_block
-[value] using specification for function __full_init
-[value] using specification for function __valid
-[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.
-[value] using specification for function __initialize
-[value] using specification for function __delete_block
-[value] using specification for function __valid_read
-[value] user error: type long double not implemented. Using double instead
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status invalid.
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
deleted file mode 100644
index 3f9e8609612695c9f97ee3f4649c80771c98ff81..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
+++ /dev/null
@@ -1,35 +0,0 @@
-tests/bts/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
-[e-acsl] beginning translation.
-tests/bts/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
-tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
-tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
-[value] using specification for function __store_block
-[value] using specification for function __full_init
-[value] using specification for function __valid
-[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.
-[value] using specification for function __initialize
-[value] using specification for function __delete_block
-[value] using specification for function __gmpz_init_set_si
-[value] using specification for function __gmpz_cmp
-[value] using specification for function __gmpz_init
-[value] using specification for function __gmpz_tdiv_q
-[value] using specification for function __gmpz_get_ui
-[value] using specification for function __valid_read
-[value] user error: type long double not implemented. Using double instead
-[value] using specification for function __gmpz_clear
-tests/bts/bts1307.i:25:[value] warning: function bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
-tests/bts/bts1307.i:25:[value] warning: function __e_acsl_bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
index e383dfcf607563d8df0128d208184cf33abfcc3d..c7d6f581b9c68ae6cb484e6d6026f243808731a3 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
@@ -1,44 +1,27 @@
-[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1307.i (no preprocessing)
-tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
+tests/bts/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
[e-acsl] beginning translation.
-tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
-tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
-tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/bts1307.i:7:[value] Function __e_acsl_foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:8:[value] Function __e_acsl_foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:9:[value] Function __e_acsl_foo: precondition got status valid.
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/bts1307.i:7:[value] Function foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:8:[value] Function foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:9:[value] Function foo: precondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __initialize
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
[value] using specification for function __valid_read
[value] user error: type long double not implemented. Using double instead
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid.
-tests/e-acsl-runtime/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: no state left in which to evaluate postcondition, status not computed.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status invalid.
[value] done for function main
-[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
deleted file mode 100644
index 1b06bc092ff68a5c3c237049c724b31c6f648fbe..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
+++ /dev/null
@@ -1,31 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
-[value] using specification for function __store_block
-[value] using specification for function __initialize
-[value] using specification for function __gmpz_init
-[value] using specification for function __gmpz_init_set_si
-[value] using specification for function __gmpz_add
-[value] using specification for function __gmpz_set
-[value] using specification for function __gmpz_clear
-tests/bts/bts1324.i:8:[value] entering loop for the first time
-[value] using specification for function __gmpz_cmp
-[value] using specification for function __gmpz_sub
-[value] using specification for function __gmpz_get_ui
-tests/bts/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_2);
-tests/bts/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_i_2);
-tests/bts/bts1324.i:15:[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.
-[value] using specification for function __delete_block
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1304.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1324.err.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
deleted file mode 100644
index 3920964dc2c217df243cf3f0df2727c81c72409c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
+++ /dev/null
@@ -1,25 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
-[value] using specification for function __store_block
-[value] using specification for function __initialize
-[value] using specification for function __delete_block
-[value] using specification for function __gmpz_init_set_si
-[value] using specification for function __gmpz_init
-[value] using specification for function __gmpz_add
-[value] using specification for function __gmpz_cmp
-[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.
-[value] using specification for function __gmpz_tdiv_q
-[value] using specification for function __gmpz_clear
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1304.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1326.err.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
deleted file mode 100644
index 07aa4ab20e4edd8fba195c589237e0ce9c53a6b4..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
+++ /dev/null
@@ -1,31 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
- __e_acsl_literal_string ∈ {0}
- __e_acsl_literal_string_2 ∈ {0}
-[value] using specification for function __store_block
-[value] using specification for function __full_init
-[value] using specification for function __literal_string
-tests/bts/bts1390.c:15:[value] entering loop for the first time
-[value] using specification for function __valid_read
-[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/bts/bts1390.c:11:[value] entering loop for the first time
-tests/bts/bts1390.c:20:[value] entering loop for the first time
-[value] using specification for function __delete_block
-tests/bts/bts1390.c:16:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:13:[value] entering loop for the first time
-[value] using specification for function __offset
-tests/bts/bts1390.c:16:[value] warning: function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s);
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
deleted file mode 100644
index 4167be2b1419df4c68742b3372e83f7be7c67621..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
+++ /dev/null
@@ -1,41 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
- __e_acsl_literal_string ∈ {0}
- __e_acsl_literal_string_2 ∈ {0}
-[value] using specification for function __store_block
-[value] using specification for function __full_init
-[value] using specification for function __literal_string
-[value] using specification for function __gmpz_init
-[value] using specification for function __gmpz_init_set_si
-[value] using specification for function __gmpz_set
-[value] using specification for function __gmpz_clear
-tests/bts/bts1390.c:15:[value] entering loop for the first time
-[value] using specification for function __gmpz_init_set_ui
-[value] using specification for function __gmpz_cmp
-[value] using specification for function __gmpz_get_ui
-tests/bts/bts1390.c:15:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_k_2);
-[value] using specification for function __gmpz_add
-tests/bts/bts1390.c:11:[value] entering loop for the first time
-tests/bts/bts1390.c:11:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_i_2);
-tests/bts/bts1390.c:20:[value] entering loop for the first time
-[value] using specification for function __delete_block
-tests/bts/bts1390.c:16:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:13:[value] entering loop for the first time
-[value] using specification for function __offset
-tests/bts/bts1390.c:13:[kernel] warning: out of bounds read. assert \valid_read((char *)__e_acsl_at_2+__e_acsl_j_2);
-[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/bts/bts1390.c:16:[value] warning: function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s);
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
index 1e2f316c2132a5e764075c5c3cf1ec2b4c203626..07aa4ab20e4edd8fba195c589237e0ce9c53a6b4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
@@ -1,19 +1,11 @@
-[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1390.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
@@ -23,45 +15,17 @@
[value] using specification for function __store_block
[value] using specification for function __full_init
[value] using specification for function __literal_string
-[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
-[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
-[value] using specification for function __gmpz_set
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid.
-[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/bts1390.c:15:[value] entering loop for the first time
-[value] using specification for function __gmpz_init_set_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid.
-[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
-[value] using specification for function __gmpz_get_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
-tests/e-acsl-runtime/bts1390.c:15:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_k_2);
-[value] using specification for function __gmpz_add
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
-tests/e-acsl-runtime/bts1390.c:11:[value] entering loop for the first time
-tests/e-acsl-runtime/bts1390.c:11:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_i_2);
-tests/e-acsl-runtime/bts1390.c:20:[value] entering loop for the first time
+tests/bts/bts1390.c:15:[value] entering loop for the first time
+[value] using specification for function __valid_read
+[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/bts/bts1390.c:11:[value] entering loop for the first time
+tests/bts/bts1390.c:20:[value] entering loop for the first time
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:13:[value] entering loop for the first time
+tests/bts/bts1390.c:16:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:13:[value] entering loop for the first time
[value] using specification for function __offset
-tests/e-acsl-runtime/bts1390.c:13:[kernel] warning: out of bounds read. assert \valid_read((char *)__e_acsl_at_2+__e_acsl_j_2);
-[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s);
-tests/e-acsl-runtime/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:16:[value] warning: function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s);
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
-[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
deleted file mode 100644
index 99d1861463a6dcc225e00eb28b7435708ae8e927..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
+++ /dev/null
@@ -1,38 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
- stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
- __fc_fopen[0..511] ∈ {0}
- __p_fc_fopen ∈ {{ &__fc_fopen[0] }}
- S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
- [--..--]
- [0].[bits 80 to 95] ∈ 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
- [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] ∈ [--..--]
- S___fc_real_data_0_S___fc_stdout[0..1] ∈ [--..--]
- S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
- S___fc_real_data_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function printf
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
deleted file mode 100644
index 99d1861463a6dcc225e00eb28b7435708ae8e927..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
+++ /dev/null
@@ -1,38 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
- stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
- __fc_fopen[0..511] ∈ {0}
- __p_fc_fopen ∈ {{ &__fc_fopen[0] }}
- S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
- [--..--]
- [0].[bits 80 to 95] ∈ 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
- [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] ∈ [--..--]
- S___fc_real_data_0_S___fc_stdout[0..1] ∈ [--..--]
- S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
- S___fc_real_data_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function printf
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1307.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1398.err.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ced893ef9e2cb2b8e0ce1086f210dddfccd820fc
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
@@ -0,0 +1,57 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+ stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
+ __fc_fopen[0..511] ∈ {0}
+ __p_fc_fopen ∈ {{ &__fc_fopen[0] }}
+ 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 ∈ [--..--]
+ [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 ∈ [--..--]
+ [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]{.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 printf
+[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
deleted file mode 100644
index 0e90a522d2cdd7d222c3cbc010fa94ba0406f388..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
+++ /dev/null
@@ -1,52 +0,0 @@
-[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
- Ignoring annotation.
-tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
- Ignoring annotation.
-tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
-[value] using specification for function __store_block
-[value] using specification for function __full_init
-FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
-[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
-[value] using specification for function __initialize
-[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_init
-[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.
-[value] using specification for function __gmpz_tdiv_q
-[value] using specification for function __gmpz_get_ui
-[value] using specification for function __initialized
-[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
-[value] using specification for function __freeable
-:0:[value] Assigning imprecise value to __e_acsl_implies.
- The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
-FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
- It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
- Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
-FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown.
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1307.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1399.err.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
deleted file mode 100644
index 3be1a2aeb0d5f81cf38e0978f683f15f28c3b0eb..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
+++ /dev/null
@@ -1,25 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
- global_i ∈ {0}
- global_i_ptr ∈ {{ &global_i }}
-[value] using specification for function __store_block
-[value] using specification for function __full_init
-[value] using specification for function __gmpz_init_set_si
-[value] using specification for function __gmpz_cmp
-[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.
-[value] using specification for function __valid
-[value] using specification for function __gmpz_clear
-[value] using specification for function __delete_block
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1324.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1478.err.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
deleted file mode 100644
index b323b8576182f6f3b8d636b5e8dcf035d262943d..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
+++ /dev/null
@@ -1,21 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
-[value] using specification for function __store_block
-[value] using specification for function __valid
-[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.
-[value] using specification for function __full_init
-[value] using specification for function __initialized
-[value] using specification for function __delete_block
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
deleted file mode 100644
index b323b8576182f6f3b8d636b5e8dcf035d262943d..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
+++ /dev/null
@@ -1,21 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
-[value] using specification for function __store_block
-[value] using specification for function __valid
-[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.
-[value] using specification for function __full_init
-[value] using specification for function __initialized
-[value] using specification for function __delete_block
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.err.log b/src/plugins/e-acsl/tests/bts/oracle/bts1700.err.log
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.log b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.log
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
index ec85865ef4537e0356b51932740b1ea052ff0d72..b323b8576182f6f3b8d636b5e8dcf035d262943d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
@@ -1,32 +1,21 @@
-[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1700.i (no preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __store_block
-tests/e-acsl-runtime/bts1700.i:10:[value] Assertion got status unknown.
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] 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 unknown.
[value] using specification for function __full_init
-tests/e-acsl-runtime/bts1700.i:13:[value] Assertion got status unknown.
[value] using specification for function __initialized
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
-[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1324.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1717.err.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle
deleted file mode 100644
index 2c04f4eb44ed2c35b7ae1ae22a95ca2ee8fc2e9b..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle
+++ /dev/null
@@ -1,21 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
-[value] using specification for function __store_block
-[value] using specification for function __full_init
-[value] using specification for function __initialized
-[value] using specification for function __valid
-[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.
-[value] using specification for function __delete_block
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle
deleted file mode 100644
index 2c04f4eb44ed2c35b7ae1ae22a95ca2ee8fc2e9b..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle
+++ /dev/null
@@ -1,21 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
-[value] using specification for function __store_block
-[value] using specification for function __full_init
-[value] using specification for function __initialized
-[value] using specification for function __valid
-[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.
-[value] using specification for function __delete_block
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1326.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1718.err.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle
deleted file mode 100644
index 82924e5df2db14afa891c2a10fecf511d9a179c1..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle
+++ /dev/null
@@ -1,29 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
- S ∈ {{ "foo" }}
- __e_acsl_literal_string ∈ {0}
- __e_acsl_literal_string_2 ∈ {0}
- __e_acsl_literal_string_3 ∈ {0}
-[value] using specification for function __store_block
-[value] using specification for function __full_init
-[value] using specification for function __literal_string
-tests/bts/bts1837.i:19:[value] entering loop for the first time
-[value] using specification for function __initialized
-[value] using specification for function __valid_read
-[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.
-[value] using specification for function __valid
-[value] using specification for function __delete_block
-tests/bts/bts1837.i:19:[kernel] warning: signed overflow. assert -2147483648 ≤ i-1;
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
deleted file mode 100644
index 82924e5df2db14afa891c2a10fecf511d9a179c1..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
+++ /dev/null
@@ -1,29 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- __memory_size ∈ [--..--]
- S ∈ {{ "foo" }}
- __e_acsl_literal_string ∈ {0}
- __e_acsl_literal_string_2 ∈ {0}
- __e_acsl_literal_string_3 ∈ {0}
-[value] using specification for function __store_block
-[value] using specification for function __full_init
-[value] using specification for function __literal_string
-tests/bts/bts1837.i:19:[value] entering loop for the first time
-[value] using specification for function __initialized
-[value] using specification for function __valid_read
-[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.
-[value] using specification for function __valid
-[value] using specification for function __delete_block
-tests/bts/bts1837.i:19:[kernel] warning: signed overflow. assert -2147483648 ≤ i-1;
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
index efd924c556296cc37747d56a5a72f0bae13e0177..82924e5df2db14afa891c2a10fecf511d9a179c1 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
@@ -10,7 +10,7 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
- S ∈ {0}
+ S ∈ {{ "foo" }}
__e_acsl_literal_string ∈ {0}
__e_acsl_literal_string_2 ∈ {0}
__e_acsl_literal_string_3 ∈ {0}
@@ -18,17 +18,12 @@
[value] using specification for function __full_init
[value] using specification for function __literal_string
tests/bts/bts1837.i:19:[value] entering loop for the first time
-tests/bts/bts1837.i:21:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/bts/bts1837.i:22:[value] Assertion got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __valid
[value] using specification for function __delete_block
tests/bts/bts1837.i:19:[kernel] warning: signed overflow. assert -2147483648 ≤ i-1;
-tests/bts/bts1837.i:11:[value] Assertion got status valid.
-tests/bts/bts1837.i:12:[value] Assertion got status valid.
-tests/bts/bts1837.i:13:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
index b2f7f38d1805dfa9a01003c60bec70fd9a9259f5..1837e016b51d3a2a431e050ce39aa1cbda24c066 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
@@ -1,12 +1,4 @@
/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
struct msgA {
int type ;
int a[2] ;
@@ -23,69 +15,11 @@ union msg {
struct msgA A ;
struct msgB B ;
};
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = 32767UL;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
- size_t size);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
- size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
void read_sensor_4(unsigned int *m)
{
- __store_block((void *)(& m),4U);
+ __store_block((void *)(& m),8UL);
__initialize((void *)m,sizeof(unsigned int));
- *m = 0U;
+ *m = (unsigned int)0;
__delete_block((void *)(& m));
return;
}
@@ -93,11 +27,11 @@ void read_sensor_4(unsigned int *m)
int main(void)
{
int __retres;
- unsigned char buf[12U];
+ unsigned char buf[sizeof(union msg)];
int i;
- __store_block((void *)(buf),12U);
+ __store_block((void *)(buf),16UL);
i = 0;
- while ((unsigned int)i < 3U) {
+ while ((unsigned long)i < sizeof(buf) / (unsigned long)4) {
read_sensor_4((unsigned int *)(buf) + i);
i ++;
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13042.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13042.c
deleted file mode 100644
index b2f7f38d1805dfa9a01003c60bec70fd9a9259f5..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13042.c
+++ /dev/null
@@ -1,118 +0,0 @@
-/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-struct msgA {
- int type ;
- int a[2] ;
-};
-struct msgB {
- int type ;
- double x ;
-};
-struct __anonstruct_T_1 {
- int type ;
-};
-union msg {
- struct __anonstruct_T_1 T ;
- struct msgA A ;
- struct msgB B ;
-};
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = 32767UL;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
- size_t size);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
- size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
-void read_sensor_4(unsigned int *m)
-{
- __store_block((void *)(& m),4U);
- __initialize((void *)m,sizeof(unsigned int));
- *m = 0U;
- __delete_block((void *)(& m));
- return;
-}
-
-int main(void)
-{
- int __retres;
- unsigned char buf[12U];
- int i;
- __store_block((void *)(buf),12U);
- i = 0;
- while ((unsigned int)i < 3U) {
- read_sensor_4((unsigned int *)(buf) + i);
- i ++;
- }
- /*@ assert \initialized((union msg *)((unsigned char *)buf)); */
- {
- int __e_acsl_initialized;
- __e_acsl_initialized = __initialized((void *)(buf),sizeof(union msg));
- e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
- (char *)"\\initialized((union msg *)((unsigned char *)buf))",
- 25);
- }
- __retres = 0;
- __delete_block((void *)(buf));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index bf2eb65234bd4cf6a74e74b410097516d5ddcc27..4c1fe9328fd11b8f4052f20d07637511faafbad2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -1,80 +1,4 @@
/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \valid_read((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
- size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
/*@ requires \valid(Mtmax_in);
requires \valid(Mwmax);
requires \valid(Mtmax_out);
@@ -86,9 +10,9 @@ predicate diffSize{L1, L2}(ℤ i) =
*/
void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
{
- __store_block((void *)(& Mtmax_in),4U);
- __store_block((void *)(& Mwmax),4U);
- __store_block((void *)(& Mtmax_out),4U);
+ __store_block((void *)(& Mtmax_in),8UL);
+ __store_block((void *)(& Mwmax),8UL);
+ __store_block((void *)(& Mtmax_out),8UL);
__initialize((void *)Mtmax_out,sizeof(float));
*Mtmax_out = (float)((double)*Mtmax_in + ((double)5 - (double)((float)(
5 / 80) * *Mwmax) * 0.4));
@@ -116,9 +40,9 @@ void __e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
int __e_acsl_valid;
int __e_acsl_valid_2;
int __e_acsl_valid_3;
- __store_block((void *)(& Mtmax_in),4U);
- __store_block((void *)(& Mwmax),4U);
- __store_block((void *)(& Mtmax_out),4U);
+ __store_block((void *)(& Mtmax_in),8UL);
+ __store_block((void *)(& Mwmax),8UL);
+ __store_block((void *)(& Mtmax_out),8UL);
__e_acsl_valid = __valid((void *)Mtmax_in,sizeof(float));
e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"foo",
(char *)"\\valid(Mtmax_in)",7);
@@ -128,11 +52,11 @@ void __e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_valid_3 = __valid((void *)Mtmax_out,sizeof(float));
e_acsl_assert(__e_acsl_valid_3,(char *)"Precondition",(char *)"foo",
(char *)"\\valid(Mtmax_out)",9);
- __store_block((void *)(& __e_acsl_at_3),4U);
+ __store_block((void *)(& __e_acsl_at_3),8UL);
__e_acsl_at_3 = Mwmax;
- __store_block((void *)(& __e_acsl_at_2),4U);
+ __store_block((void *)(& __e_acsl_at_2),8UL);
__e_acsl_at_2 = Mtmax_in;
- __store_block((void *)(& __e_acsl_at),4U);
+ __store_block((void *)(& __e_acsl_at),8UL);
__e_acsl_at = Mtmax_out;
foo(Mtmax_in,Mwmax,Mtmax_out);
}
@@ -175,9 +99,9 @@ void __e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
*/
void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
{
- __store_block((void *)(& Mtmin_in),4U);
- __store_block((void *)(& Mwmin),4U);
- __store_block((void *)(& Mtmin_out),4U);
+ __store_block((void *)(& Mtmin_in),8UL);
+ __store_block((void *)(& Mwmin),8UL);
+ __store_block((void *)(& Mtmin_out),8UL);
__initialize((void *)Mtmin_out,sizeof(float));
*Mtmin_out = (float)(0.85 * (double)*Mwmin);
__delete_block((void *)(& Mtmin_in));
@@ -209,9 +133,9 @@ void __e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
int __e_acsl_valid;
int __e_acsl_valid_2;
int __e_acsl_valid_3;
- __store_block((void *)(& Mtmin_in),4U);
- __store_block((void *)(& Mwmin),4U);
- __store_block((void *)(& Mtmin_out),4U);
+ __store_block((void *)(& Mtmin_in),8UL);
+ __store_block((void *)(& Mwmin),8UL);
+ __store_block((void *)(& Mtmin_out),8UL);
__e_acsl_valid = __valid((void *)Mtmin_in,sizeof(float));
e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"bar",
(char *)"\\valid(Mtmin_in)",19);
@@ -221,17 +145,17 @@ void __e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_valid_3 = __valid((void *)Mtmin_out,sizeof(float));
e_acsl_assert(__e_acsl_valid_3,(char *)"Precondition",(char *)"bar",
(char *)"\\valid(Mtmin_out)",21);
- __store_block((void *)(& __e_acsl_at_6),4U);
+ __store_block((void *)(& __e_acsl_at_6),8UL);
__e_acsl_at_6 = Mwmin;
- __store_block((void *)(& __e_acsl_at_5),4U);
+ __store_block((void *)(& __e_acsl_at_5),8UL);
__e_acsl_at_5 = Mtmin_in;
- __store_block((void *)(& __e_acsl_at_4),4U);
+ __store_block((void *)(& __e_acsl_at_4),8UL);
__e_acsl_at_4 = Mwmin;
- __store_block((void *)(& __e_acsl_at_3),4U);
+ __store_block((void *)(& __e_acsl_at_3),8UL);
__e_acsl_at_3 = Mtmin_in;
- __store_block((void *)(& __e_acsl_at_2),4U);
+ __store_block((void *)(& __e_acsl_at_2),8UL);
__e_acsl_at_2 = Mtmin_in;
- __store_block((void *)(& __e_acsl_at),4U);
+ __store_block((void *)(& __e_acsl_at),8UL);
__e_acsl_at = Mtmin_out;
bar(Mtmin_in,Mwmin,Mtmin_out);
}
@@ -292,9 +216,9 @@ int main(void)
float f;
float g;
float h;
- __store_block((void *)(& h),4U);
- __store_block((void *)(& g),4U);
- __store_block((void *)(& f),4U);
+ __store_block((void *)(& h),4UL);
+ __store_block((void *)(& g),4UL);
+ __store_block((void *)(& f),4UL);
__full_init((void *)(& f));
f = (float)1.0;
__full_init((void *)(& g));
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13072.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13072.c
deleted file mode 100644
index b0fc85c485edb633748505648101eecec9c3b163..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13072.c
+++ /dev/null
@@ -1,396 +0,0 @@
-/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ requires ¬\initialized(z);
- ensures \valid(\old(z));
- assigns *z;
- assigns *z \from __e_acsl_init;
- allocates \old(z);
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
-
-/*@ requires \valid_read(z_orig);
- requires ¬\initialized(z);
- ensures \valid(\old(z));
- assigns *z;
- assigns *z \from *z_orig;
- allocates \old(z);
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set(__mpz_struct * /*[1]*/ z,
- __mpz_struct const * /*[1]*/ z_orig);
-
-/*@ requires ¬\initialized(z);
- ensures \valid(\old(z));
- ensures \initialized(\old(z));
- assigns *z;
- assigns *z \from n;
- allocates \old(z);
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
- long n);
-
-/*@ requires \valid(x);
- assigns *x;
- assigns *x \from *x; */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-
-/*@ requires \valid_read(z1);
- requires \valid_read(z2);
- assigns \result;
- assigns \result \from *z1, *z2;
- */
-extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
- __mpz_struct const * /*[1]*/ z2);
-
-/*@ requires \valid(z1);
- requires \valid_read(z2);
- requires \valid_read(z3);
- assigns *z1;
- assigns *z1 \from *z2, *z3;
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
- __mpz_struct const * /*[1]*/ z2,
- __mpz_struct const * /*[1]*/ z3);
-
-/*@ requires \valid_read(z);
- assigns \result;
- assigns \result \from *z; */
-extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \valid_read((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
- size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
-/*@ requires \valid(Mtmax_in);
- requires \valid(Mwmax);
- requires \valid(Mtmax_out);
-
- behavior OverEstimate_Motoring:
- assumes \true;
- ensures
- *\old(Mtmax_out) ≡ *\old(Mtmax_in)+(5-((5/80)**\old(Mwmax))*0.4);
- */
-void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
-{
- __store_block((void *)(& Mtmax_in),4U);
- __store_block((void *)(& Mwmax),4U);
- __store_block((void *)(& Mtmax_out),4U);
- __initialize((void *)Mtmax_out,sizeof(float));
- *Mtmax_out = (float)((double)*Mtmax_in + ((double)5 - (double)((float)(
- 5 / 80) * *Mwmax) * 0.4));
- __delete_block((void *)(& Mtmax_in));
- __delete_block((void *)(& Mwmax));
- __delete_block((void *)(& Mtmax_out));
- return;
-}
-
-/*@ requires \valid(Mtmax_in);
- requires \valid(Mwmax);
- requires \valid(Mtmax_out);
-
- behavior OverEstimate_Motoring:
- assumes \true;
- ensures
- *\old(Mtmax_out) ≡ *\old(Mtmax_in)+(5-((5/80)**\old(Mwmax))*0.4);
- */
-void __e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
-{
- float *__e_acsl_at_3;
- float *__e_acsl_at_2;
- float *__e_acsl_at;
- {
- int __e_acsl_valid;
- int __e_acsl_valid_2;
- int __e_acsl_valid_3;
- __store_block((void *)(& Mtmax_in),4U);
- __store_block((void *)(& Mwmax),4U);
- __store_block((void *)(& Mtmax_out),4U);
- __e_acsl_valid = __valid((void *)Mtmax_in,sizeof(float));
- e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"foo",
- (char *)"\\valid(Mtmax_in)",7);
- __e_acsl_valid_2 = __valid((void *)Mwmax,sizeof(float));
- e_acsl_assert(__e_acsl_valid_2,(char *)"Precondition",(char *)"foo",
- (char *)"\\valid(Mwmax)",8);
- __e_acsl_valid_3 = __valid((void *)Mtmax_out,sizeof(float));
- e_acsl_assert(__e_acsl_valid_3,(char *)"Precondition",(char *)"foo",
- (char *)"\\valid(Mtmax_out)",9);
- __store_block((void *)(& __e_acsl_at_3),4U);
- __e_acsl_at_3 = Mwmax;
- __store_block((void *)(& __e_acsl_at_2),4U);
- __e_acsl_at_2 = Mtmax_in;
- __store_block((void *)(& __e_acsl_at),4U);
- __e_acsl_at = Mtmax_out;
- foo(Mtmax_in,Mwmax,Mtmax_out);
- }
- {
- mpz_t __e_acsl;
- mpz_t __e_acsl_2;
- mpz_t __e_acsl_3;
- int __e_acsl_div_guard;
- mpz_t __e_acsl_div;
- unsigned long __e_acsl_4;
- int __e_acsl_valid_read;
- int __e_acsl_valid_read_2;
- int __e_acsl_valid_read_3;
- __gmpz_init_set_si(__e_acsl,(long)5);
- __gmpz_init_set_si(__e_acsl_2,(long)80);
- __gmpz_init_set_si(__e_acsl_3,0L);
- __e_acsl_div_guard = __gmpz_cmp((__mpz_struct const *)(__e_acsl_2),
- (__mpz_struct const *)(__e_acsl_3));
- __gmpz_init(__e_acsl_div);
- /*@ assert E_ACSL: 80 ≢ 0; */
- e_acsl_assert(! (__e_acsl_div_guard == 0),(char *)"Postcondition",
- (char *)"foo",(char *)"80 == 0",13);
- __gmpz_tdiv_q(__e_acsl_div,(__mpz_struct const *)(__e_acsl),
- (__mpz_struct const *)(__e_acsl_2));
- __e_acsl_4 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_div));
- __e_acsl_valid_read = __valid_read((void *)__e_acsl_at_3,sizeof(float));
- e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"foo",
- (char *)"mem_access: \\valid_read(__e_acsl_at_3)",13);
- __e_acsl_valid_read_2 = __valid_read((void *)__e_acsl_at_2,sizeof(float));
- e_acsl_assert(__e_acsl_valid_read_2,(char *)"RTE",(char *)"foo",
- (char *)"mem_access: \\valid_read(__e_acsl_at_2)",13);
- __e_acsl_valid_read_3 = __valid_read((void *)__e_acsl_at,sizeof(float));
- e_acsl_assert(__e_acsl_valid_read_3,(char *)"RTE",(char *)"foo",
- (char *)"mem_access: \\valid_read(__e_acsl_at)",13);
- e_acsl_assert(*__e_acsl_at == *__e_acsl_at_2 + ((long double)5 -
- ((long double)__e_acsl_4 * *__e_acsl_at_3) * 0.4),
- (char *)"Postcondition",(char *)"foo",
- (char *)"*\\old(Mtmax_out) == *\\old(Mtmax_in)+(5-((5/80)**\\old(Mwmax))*0.4)",
- 13);
- __delete_block((void *)(& Mtmax_in));
- __delete_block((void *)(& Mwmax));
- __delete_block((void *)(& Mtmax_out));
- __gmpz_clear(__e_acsl);
- __gmpz_clear(__e_acsl_2);
- __gmpz_clear(__e_acsl_3);
- __gmpz_clear(__e_acsl_div);
- return;
- }
-}
-
-/*@ requires \valid(Mtmin_in);
- requires \valid(Mwmin);
- requires \valid(Mtmin_out);
-
- behavior UnderEstimate_Motoring:
- assumes \true;
- ensures
- *\old(Mtmin_out) ≡ *\old(Mtmin_in) < 0.85**\old(Mwmin)?
- *\old(Mtmin_in) ≢ 0.:
- 0.85**\old(Mwmin) ≢ 0.;
- */
-void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
-{
- __store_block((void *)(& Mtmin_in),4U);
- __store_block((void *)(& Mwmin),4U);
- __store_block((void *)(& Mtmin_out),4U);
- __initialize((void *)Mtmin_out,sizeof(float));
- *Mtmin_out = (float)(0.85 * (double)*Mwmin);
- __delete_block((void *)(& Mtmin_in));
- __delete_block((void *)(& Mwmin));
- __delete_block((void *)(& Mtmin_out));
- return;
-}
-
-/*@ requires \valid(Mtmin_in);
- requires \valid(Mwmin);
- requires \valid(Mtmin_out);
-
- behavior UnderEstimate_Motoring:
- assumes \true;
- ensures
- *\old(Mtmin_out) ≡ *\old(Mtmin_in) < 0.85**\old(Mwmin)?
- *\old(Mtmin_in) ≢ 0.:
- 0.85**\old(Mwmin) ≢ 0.;
- */
-void __e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
-{
- float *__e_acsl_at_6;
- float *__e_acsl_at_5;
- float *__e_acsl_at_4;
- float *__e_acsl_at_3;
- float *__e_acsl_at_2;
- float *__e_acsl_at;
- {
- int __e_acsl_valid;
- int __e_acsl_valid_2;
- int __e_acsl_valid_3;
- __store_block((void *)(& Mtmin_in),4U);
- __store_block((void *)(& Mwmin),4U);
- __store_block((void *)(& Mtmin_out),4U);
- __e_acsl_valid = __valid((void *)Mtmin_in,sizeof(float));
- e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"bar",
- (char *)"\\valid(Mtmin_in)",19);
- __e_acsl_valid_2 = __valid((void *)Mwmin,sizeof(float));
- e_acsl_assert(__e_acsl_valid_2,(char *)"Precondition",(char *)"bar",
- (char *)"\\valid(Mwmin)",20);
- __e_acsl_valid_3 = __valid((void *)Mtmin_out,sizeof(float));
- e_acsl_assert(__e_acsl_valid_3,(char *)"Precondition",(char *)"bar",
- (char *)"\\valid(Mtmin_out)",21);
- __store_block((void *)(& __e_acsl_at_6),4U);
- __e_acsl_at_6 = Mwmin;
- __store_block((void *)(& __e_acsl_at_5),4U);
- __e_acsl_at_5 = Mtmin_in;
- __store_block((void *)(& __e_acsl_at_4),4U);
- __e_acsl_at_4 = Mwmin;
- __store_block((void *)(& __e_acsl_at_3),4U);
- __e_acsl_at_3 = Mtmin_in;
- __store_block((void *)(& __e_acsl_at_2),4U);
- __e_acsl_at_2 = Mtmin_in;
- __store_block((void *)(& __e_acsl_at),4U);
- __e_acsl_at = Mtmin_out;
- bar(Mtmin_in,Mwmin,Mtmin_out);
- }
- {
- int __e_acsl_valid_read;
- int __e_acsl_valid_read_2;
- mpz_t __e_acsl_and;
- unsigned long __e_acsl_2;
- int __e_acsl_if;
- __e_acsl_valid_read = __valid_read((void *)__e_acsl_at_2,sizeof(float));
- e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"bar",
- (char *)"mem_access: \\valid_read(__e_acsl_at_2)",25);
- __e_acsl_valid_read_2 = __valid_read((void *)__e_acsl_at,sizeof(float));
- e_acsl_assert(__e_acsl_valid_read_2,(char *)"RTE",(char *)"bar",
- (char *)"mem_access: \\valid_read(__e_acsl_at)",25);
- if (*__e_acsl_at == *__e_acsl_at_2) {
- int __e_acsl_valid_read_3;
- int __e_acsl_valid_read_4;
- mpz_t __e_acsl;
- __e_acsl_valid_read_3 = __valid_read((void *)__e_acsl_at_4,
- sizeof(float));
- e_acsl_assert(__e_acsl_valid_read_3,(char *)"RTE",(char *)"bar",
- (char *)"mem_access: \\valid_read(__e_acsl_at_4)",25);
- __e_acsl_valid_read_4 = __valid_read((void *)__e_acsl_at_3,
- sizeof(float));
- e_acsl_assert(__e_acsl_valid_read_4,(char *)"RTE",(char *)"bar",
- (char *)"mem_access: \\valid_read(__e_acsl_at_3)",25);
- __gmpz_init_set_si(__e_acsl,
- (long)(*__e_acsl_at_3 < 0.85 * *__e_acsl_at_4));
- __gmpz_init_set(__e_acsl_and,(__mpz_struct const *)(__e_acsl));
- __gmpz_clear(__e_acsl);
- }
- else __gmpz_init_set_si(__e_acsl_and,0L);
- __e_acsl_2 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_and));
- if (__e_acsl_2) {
- int __e_acsl_valid_read_5;
- __e_acsl_valid_read_5 = __valid_read((void *)__e_acsl_at_5,
- sizeof(float));
- e_acsl_assert(__e_acsl_valid_read_5,(char *)"RTE",(char *)"bar",
- (char *)"mem_access: \\valid_read(__e_acsl_at_5)",25);
- __e_acsl_if = *__e_acsl_at_5 != 0.;
- }
- else {
- int __e_acsl_valid_read_6;
- __e_acsl_valid_read_6 = __valid_read((void *)__e_acsl_at_6,
- sizeof(float));
- e_acsl_assert(__e_acsl_valid_read_6,(char *)"RTE",(char *)"bar",
- (char *)"mem_access: \\valid_read(__e_acsl_at_6)",25);
- __e_acsl_if = 0.85 * *__e_acsl_at_6 != 0.;
- }
- e_acsl_assert(__e_acsl_if,(char *)"Postcondition",(char *)"bar",
- (char *)"*\\old(Mtmin_out) == *\\old(Mtmin_in) < 0.85**\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.:\n 0.85**\\old(Mwmin) != 0.",
- 25);
- __delete_block((void *)(& Mtmin_in));
- __delete_block((void *)(& Mwmin));
- __delete_block((void *)(& Mtmin_out));
- __gmpz_clear(__e_acsl_and);
- return;
- }
-}
-
-int main(void)
-{
- int __retres;
- float f;
- float g;
- float h;
- __store_block((void *)(& h),4U);
- __store_block((void *)(& g),4U);
- __store_block((void *)(& f),4U);
- __full_init((void *)(& f));
- f = (float)1.0;
- __full_init((void *)(& g));
- g = (float)1.0;
- __e_acsl_foo(& f,& g,& h);
- __e_acsl_bar(& f,& g,& h);
- __retres = 0;
- __delete_block((void *)(& h));
- __delete_block((void *)(& g));
- __delete_block((void *)(& f));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index bad798ea364dc5f9a53442723b3734b4528e02c0..bc6ba5e2659462ef4d757307dc36010189013763 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -1,70 +1,4 @@
/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
- size_t size);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \valid_read((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
- size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
/*@ behavior yes:
assumes ∀ int i; 0 < i < n ⇒ *(t+(i-1)) ≤ *(t+i);
ensures \result ≡ 1;
@@ -98,7 +32,7 @@ int __e_acsl_sorted(int *t, int n)
{
int __e_acsl_at;
int __retres;
- __store_block((void *)(& t),4U);
+ __store_block((void *)(& t),8UL);
{
int __e_acsl_forall;
int __e_acsl_i;
@@ -113,12 +47,12 @@ int __e_acsl_sorted(int *t, int n)
sizeof(int));
e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"sorted",
(char *)"mem_access: \\valid_read(t+__e_acsl_i)",8);
- __e_acsl_valid_read_2 = __valid_read((void *)(t + ((long long)__e_acsl_i - (long long)1)),
+ __e_acsl_valid_read_2 = __valid_read((void *)(t + ((long)__e_acsl_i - (long)1)),
sizeof(int));
e_acsl_assert(__e_acsl_valid_read_2,(char *)"RTE",(char *)"sorted",
- (char *)"mem_access: \\valid_read(t+(long long)((long long)__e_acsl_i-1))",
+ (char *)"mem_access: \\valid_read(t+(long)((long)__e_acsl_i-1))",
8);
- if (*(t + ((long long)__e_acsl_i - (long long)1)) <= *(t + __e_acsl_i))
+ if (*(t + ((long)__e_acsl_i - (long)1)) <= *(t + __e_acsl_i))
;
else {
__e_acsl_forall = 0;
@@ -148,7 +82,7 @@ int main(void)
int __retres;
int t[7];
int n;
- __store_block((void *)(t),28U);
+ __store_block((void *)(t),28UL);
__initialize((void *)(t),sizeof(int));
t[0] = 1;
__initialize((void *)(& t[1]),sizeof(int));
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13242.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13242.c
deleted file mode 100644
index aab5a6b122816b329918cab015120a46b869dc0f..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13242.c
+++ /dev/null
@@ -1,295 +0,0 @@
-/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ requires ¬\initialized(z);
- ensures \valid(\old(z));
- assigns *z;
- assigns *z \from __e_acsl_init;
- allocates \old(z);
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
-
-/*@ requires ¬\initialized(z);
- ensures \valid(\old(z));
- ensures \initialized(\old(z));
- assigns *z;
- assigns *z \from n;
- allocates \old(z);
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
- long n);
-
-/*@ requires \valid_read(z_orig);
- requires \valid(z);
- assigns *z;
- assigns *z \from *z_orig;
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_set(__mpz_struct * /*[1]*/ z,
- __mpz_struct const * /*[1]*/ z_orig);
-
-/*@ requires \valid(x);
- assigns *x;
- assigns *x \from *x; */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-
-/*@ requires \valid_read(z1);
- requires \valid_read(z2);
- assigns \result;
- assigns \result \from *z1, *z2;
- */
-extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
- __mpz_struct const * /*[1]*/ z2);
-
-/*@ requires \valid(z1);
- requires \valid_read(z2);
- requires \valid_read(z3);
- assigns *z1;
- assigns *z1 \from *z2, *z3;
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
- __mpz_struct const * /*[1]*/ z2,
- __mpz_struct const * /*[1]*/ z3);
-
-/*@ requires \valid(z1);
- requires \valid_read(z2);
- requires \valid_read(z3);
- assigns *z1;
- assigns *z1 \from *z2, *z3;
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
- __mpz_struct const * /*[1]*/ z2,
- __mpz_struct const * /*[1]*/ z3);
-
-/*@ requires \valid_read(z);
- assigns \result;
- assigns \result \from *z; */
-extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
- size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
-/*@ behavior yes:
- assumes ∀ int i; 0 < i < n ⇒ *(t+(i-1)) ≤ *(t+i);
- ensures \result ≡ 1;
- */
-int sorted(int *t, int n)
-{
- int __retres;
- int b;
- b = 1;
- if (n <= 1) {
- __retres = 1;
- goto return_label;
- }
- b = 1;
- while (b < n) {
- if (*(t + (b - 1)) > *(t + b)) {
- __retres = 0;
- goto return_label;
- }
- b ++;
- }
- __retres = 1;
- return_label: return __retres;
-}
-
-/*@ behavior yes:
- assumes ∀ int i; 0 < i < n ⇒ *(t+(i-1)) ≤ *(t+i);
- ensures \result ≡ 1;
- */
-int __e_acsl_sorted(int *t, int n)
-{
- int __e_acsl_at;
- int __retres;
- __store_block((void *)(& t),4U);
- {
- int __e_acsl_forall;
- mpz_t __e_acsl_i;
- __e_acsl_forall = 1;
- __gmpz_init(__e_acsl_i);
- {
- mpz_t __e_acsl_5;
- mpz_t __e_acsl_6;
- mpz_t __e_acsl_add;
- __gmpz_init_set_si(__e_acsl_5,(long)0);
- __gmpz_init_set_si(__e_acsl_6,1L);
- __gmpz_init(__e_acsl_add);
- __gmpz_add(__e_acsl_add,(__mpz_struct const *)(__e_acsl_5),
- (__mpz_struct const *)(__e_acsl_6));
- __gmpz_set(__e_acsl_i,(__mpz_struct const *)(__e_acsl_add));
- __gmpz_clear(__e_acsl_5);
- __gmpz_clear(__e_acsl_6);
- __gmpz_clear(__e_acsl_add);
- }
- while (1) {
- {
- mpz_t __e_acsl_n;
- int __e_acsl_lt;
- __gmpz_init_set_si(__e_acsl_n,(long)n);
- __e_acsl_lt = __gmpz_cmp((__mpz_struct const *)(__e_acsl_i),
- (__mpz_struct const *)(__e_acsl_n));
- if (__e_acsl_lt < 0) ; else break;
- __gmpz_clear(__e_acsl_n);
- }
- {
- mpz_t __e_acsl;
- mpz_t __e_acsl_sub;
- unsigned long __e_acsl_2;
- mpz_t __e_acsl_3;
- unsigned long __e_acsl_i_2;
- mpz_t __e_acsl_4;
- int __e_acsl_le;
- __gmpz_init_set_si(__e_acsl,(long)1);
- __gmpz_init(__e_acsl_sub);
- __gmpz_sub(__e_acsl_sub,(__mpz_struct const *)(__e_acsl_i),
- (__mpz_struct const *)(__e_acsl));
- __e_acsl_2 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_sub));
- __gmpz_init_set_si(__e_acsl_3,(long)*(t + __e_acsl_2));
- __e_acsl_i_2 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_i));
- __gmpz_init_set_si(__e_acsl_4,(long)*(t + __e_acsl_i_2));
- __e_acsl_le = __gmpz_cmp((__mpz_struct const *)(__e_acsl_3),
- (__mpz_struct const *)(__e_acsl_4));
- __gmpz_clear(__e_acsl);
- __gmpz_clear(__e_acsl_sub);
- __gmpz_clear(__e_acsl_3);
- __gmpz_clear(__e_acsl_4);
- if (__e_acsl_le <= 0) ;
- else {
- __e_acsl_forall = 0;
- goto e_acsl_end_loop1;
- }
- }
- {
- mpz_t __e_acsl_7;
- mpz_t __e_acsl_add_2;
- __gmpz_init_set_si(__e_acsl_7,1L);
- __gmpz_init(__e_acsl_add_2);
- __gmpz_add(__e_acsl_add_2,(__mpz_struct const *)(__e_acsl_i),
- (__mpz_struct const *)(__e_acsl_7));
- __gmpz_set(__e_acsl_i,(__mpz_struct const *)(__e_acsl_add_2));
- __gmpz_clear(__e_acsl_7);
- __gmpz_clear(__e_acsl_add_2);
- }
- }
- e_acsl_end_loop1: ;
- __e_acsl_at = __e_acsl_forall;
- __gmpz_clear(__e_acsl_i);
- }
- __retres = sorted(t,n);
- {
- int __e_acsl_implies;
- if (! __e_acsl_at) __e_acsl_implies = 1;
- else {
- mpz_t __e_acsl_result;
- mpz_t __e_acsl_8;
- int __e_acsl_eq;
- __gmpz_init_set_si(__e_acsl_result,(long)__retres);
- __gmpz_init_set_si(__e_acsl_8,(long)1);
- __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_result),
- (__mpz_struct const *)(__e_acsl_8));
- __e_acsl_implies = __e_acsl_eq == 0;
- __gmpz_clear(__e_acsl_result);
- __gmpz_clear(__e_acsl_8);
- }
- e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",(char *)"sorted",
- (char *)"\\old(\\forall int i; 0 < i < n ==> *(t+(i-1)) <= *(t+i)) ==> \\result == 1",
- 9);
- __delete_block((void *)(& t));
- return __retres;
- }
-}
-
-int main(void)
-{
- int __retres;
- int t[7];
- int n;
- __store_block((void *)(t),28U);
- __initialize((void *)(t),sizeof(int));
- t[0] = 1;
- __initialize((void *)(& t[1]),sizeof(int));
- t[1] = 4;
- __initialize((void *)(& t[2]),sizeof(int));
- t[2] = 4;
- __initialize((void *)(& t[3]),sizeof(int));
- t[3] = 5;
- __initialize((void *)(& t[4]),sizeof(int));
- t[4] = 5;
- __initialize((void *)(& t[5]),sizeof(int));
- t[5] = 5;
- __initialize((void *)(& t[6]),sizeof(int));
- t[6] = 7;
- n = __e_acsl_sorted(t,7);
- /*@ assert n ≡ 1; */
- {
- mpz_t __e_acsl_n;
- mpz_t __e_acsl;
- int __e_acsl_eq;
- __gmpz_init_set_si(__e_acsl_n,(long)n);
- __gmpz_init_set_si(__e_acsl,(long)1);
- __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_n),
- (__mpz_struct const *)(__e_acsl));
- e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
- (char *)"n == 1",25);
- __gmpz_clear(__e_acsl_n);
- __gmpz_clear(__e_acsl);
- }
- __retres = 0;
- __delete_block((void *)(t));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index a5bf59395c9f283c9de2e158dd06991205359b47..6ccfa703b0201ec345ec24eb91200fdca17e68b1 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -1,71 +1,5 @@
/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
typedef int ArrayInt[5];
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
- size_t size);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \valid_read((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
- size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
/*@ ensures
*\old(AverageAccel) ≡
(((((*\old(Accel))[4]+(*\old(Accel))[3])+(*\old(Accel))[2])+(*\old(
@@ -74,8 +8,8 @@ predicate diffSize{L1, L2}(ℤ i) =
*/
void atp_NORMAL_computeAverageAccel(ArrayInt *Accel, int *AverageAccel)
{
- __store_block((void *)(& Accel),4U);
- __store_block((void *)(& AverageAccel),4U);
+ __store_block((void *)(& Accel),8UL);
+ __store_block((void *)(& AverageAccel),8UL);
__initialize((void *)AverageAccel,sizeof(int));
*AverageAccel = (((((*Accel)[4] + (*Accel)[3]) + (*Accel)[2]) + (*Accel)[1]) + (*Accel)[0]) / 5;
__delete_block((void *)(& Accel));
@@ -98,19 +32,19 @@ void __e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
ArrayInt *__e_acsl_at_3;
ArrayInt *__e_acsl_at_2;
int *__e_acsl_at;
- __store_block((void *)(& Accel),4U);
- __store_block((void *)(& AverageAccel),4U);
- __store_block((void *)(& __e_acsl_at_6),4U);
+ __store_block((void *)(& Accel),8UL);
+ __store_block((void *)(& AverageAccel),8UL);
+ __store_block((void *)(& __e_acsl_at_6),8UL);
__e_acsl_at_6 = Accel;
- __store_block((void *)(& __e_acsl_at_5),4U);
+ __store_block((void *)(& __e_acsl_at_5),8UL);
__e_acsl_at_5 = Accel;
- __store_block((void *)(& __e_acsl_at_4),4U);
+ __store_block((void *)(& __e_acsl_at_4),8UL);
__e_acsl_at_4 = Accel;
- __store_block((void *)(& __e_acsl_at_3),4U);
+ __store_block((void *)(& __e_acsl_at_3),8UL);
__e_acsl_at_3 = Accel;
- __store_block((void *)(& __e_acsl_at_2),4U);
+ __store_block((void *)(& __e_acsl_at_2),8UL);
__e_acsl_at_2 = Accel;
- __store_block((void *)(& __e_acsl_at),4U);
+ __store_block((void *)(& __e_acsl_at),8UL);
__e_acsl_at = AverageAccel;
atp_NORMAL_computeAverageAccel(Accel,AverageAccel);
{
@@ -153,7 +87,7 @@ void __e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
e_acsl_assert(__e_acsl_valid_read_6,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"mem_access: \\valid_read(__e_acsl_at)",10);
- e_acsl_assert(*__e_acsl_at == (((((long long)(*__e_acsl_at_2)[4] + (long long)(*__e_acsl_at_3)[3]) + (long long)(*__e_acsl_at_4)[2]) + (long long)(*__e_acsl_at_5)[1]) + (long long)(*__e_acsl_at_6)[0]) / (long long)5,
+ e_acsl_assert(*__e_acsl_at == (((((long)(*__e_acsl_at_2)[4] + (long)(*__e_acsl_at_3)[3]) + (long)(*__e_acsl_at_4)[2]) + (long)(*__e_acsl_at_5)[1]) + (long)(*__e_acsl_at_6)[0]) / (long)5,
(char *)"Postcondition",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"*\\old(AverageAccel) ==\n(((((*\\old(Accel))[4]+(*\\old(Accel))[3])+(*\\old(Accel))[2])+(*\\old(Accel))[1])+(*\n \\old(Accel))[0])/5",
@@ -169,8 +103,8 @@ int main(void)
int __retres;
ArrayInt Accel;
int av;
- __store_block((void *)(& av),4U);
- __store_block((void *)(Accel),20U);
+ __store_block((void *)(& av),4UL);
+ __store_block((void *)(Accel),20UL);
__initialize((void *)(Accel),sizeof(int));
Accel[0] = 1;
__initialize((void *)(& Accel[1]),sizeof(int));
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13262.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13262.c
deleted file mode 100644
index c5e1dc20355e66da9357905a35084b5bab8597be..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13262.c
+++ /dev/null
@@ -1,253 +0,0 @@
-/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-typedef int ArrayInt[5];
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ requires ¬\initialized(z);
- ensures \valid(\old(z));
- assigns *z;
- assigns *z \from __e_acsl_init;
- allocates \old(z);
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
-
-/*@ requires ¬\initialized(z);
- ensures \valid(\old(z));
- ensures \initialized(\old(z));
- assigns *z;
- assigns *z \from n;
- allocates \old(z);
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
- long n);
-
-/*@ requires \valid(x);
- assigns *x;
- assigns *x \from *x; */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-
-/*@ requires \valid_read(z1);
- requires \valid_read(z2);
- assigns \result;
- assigns \result \from *z1, *z2;
- */
-extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
- __mpz_struct const * /*[1]*/ z2);
-
-/*@ requires \valid(z1);
- requires \valid_read(z2);
- requires \valid_read(z3);
- assigns *z1;
- assigns *z1 \from *z2, *z3;
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
- __mpz_struct const * /*[1]*/ z2,
- __mpz_struct const * /*[1]*/ z3);
-
-/*@ requires \valid(z1);
- requires \valid_read(z2);
- requires \valid_read(z3);
- assigns *z1;
- assigns *z1 \from *z2, *z3;
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
- __mpz_struct const * /*[1]*/ z2,
- __mpz_struct const * /*[1]*/ z3);
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
- size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
-/*@ ensures
- *\old(AverageAccel) ≡
- (((((*\old(Accel))[4]+(*\old(Accel))[3])+(*\old(Accel))[2])+(*\old(
- Accel))[1])+(*
- \old(Accel))[0])/5;
- */
-void atp_NORMAL_computeAverageAccel(ArrayInt *Accel, int *AverageAccel)
-{
- __store_block((void *)(& Accel),4U);
- __store_block((void *)(& AverageAccel),4U);
- __initialize((void *)AverageAccel,sizeof(int));
- *AverageAccel = (((((*Accel)[4] + (*Accel)[3]) + (*Accel)[2]) + (*Accel)[1]) + (*Accel)[0]) / 5;
- __delete_block((void *)(& Accel));
- __delete_block((void *)(& AverageAccel));
- return;
-}
-
-/*@ ensures
- *\old(AverageAccel) ≡
- (((((*\old(Accel))[4]+(*\old(Accel))[3])+(*\old(Accel))[2])+(*\old(
- Accel))[1])+(*
- \old(Accel))[0])/5;
- */
-void __e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
- int *AverageAccel)
-{
- ArrayInt *__e_acsl_at_6;
- ArrayInt *__e_acsl_at_5;
- ArrayInt *__e_acsl_at_4;
- ArrayInt *__e_acsl_at_3;
- ArrayInt *__e_acsl_at_2;
- int *__e_acsl_at;
- __store_block((void *)(& Accel),4U);
- __store_block((void *)(& AverageAccel),4U);
- __store_block((void *)(& __e_acsl_at_6),4U);
- __e_acsl_at_6 = Accel;
- __store_block((void *)(& __e_acsl_at_5),4U);
- __e_acsl_at_5 = Accel;
- __store_block((void *)(& __e_acsl_at_4),4U);
- __e_acsl_at_4 = Accel;
- __store_block((void *)(& __e_acsl_at_3),4U);
- __e_acsl_at_3 = Accel;
- __store_block((void *)(& __e_acsl_at_2),4U);
- __e_acsl_at_2 = Accel;
- __store_block((void *)(& __e_acsl_at),4U);
- __e_acsl_at = AverageAccel;
- atp_NORMAL_computeAverageAccel(Accel,AverageAccel);
- {
- mpz_t __e_acsl;
- mpz_t __e_acsl_2;
- mpz_t __e_acsl_3;
- mpz_t __e_acsl_add;
- mpz_t __e_acsl_4;
- mpz_t __e_acsl_add_2;
- mpz_t __e_acsl_5;
- mpz_t __e_acsl_add_3;
- mpz_t __e_acsl_6;
- mpz_t __e_acsl_add_4;
- mpz_t __e_acsl_7;
- mpz_t __e_acsl_8;
- int __e_acsl_div_guard;
- mpz_t __e_acsl_div;
- int __e_acsl_eq;
- __gmpz_init_set_si(__e_acsl,(long)*__e_acsl_at);
- __gmpz_init_set_si(__e_acsl_2,(long)(*__e_acsl_at_2)[4]);
- __gmpz_init_set_si(__e_acsl_3,(long)(*__e_acsl_at_3)[3]);
- __gmpz_init(__e_acsl_add);
- __gmpz_add(__e_acsl_add,(__mpz_struct const *)(__e_acsl_2),
- (__mpz_struct const *)(__e_acsl_3));
- __gmpz_init_set_si(__e_acsl_4,(long)(*__e_acsl_at_4)[2]);
- __gmpz_init(__e_acsl_add_2);
- __gmpz_add(__e_acsl_add_2,(__mpz_struct const *)(__e_acsl_add),
- (__mpz_struct const *)(__e_acsl_4));
- __gmpz_init_set_si(__e_acsl_5,(long)(*__e_acsl_at_5)[1]);
- __gmpz_init(__e_acsl_add_3);
- __gmpz_add(__e_acsl_add_3,(__mpz_struct const *)(__e_acsl_add_2),
- (__mpz_struct const *)(__e_acsl_5));
- __gmpz_init_set_si(__e_acsl_6,(long)(*__e_acsl_at_6)[0]);
- __gmpz_init(__e_acsl_add_4);
- __gmpz_add(__e_acsl_add_4,(__mpz_struct const *)(__e_acsl_add_3),
- (__mpz_struct const *)(__e_acsl_6));
- __gmpz_init_set_si(__e_acsl_7,(long)5);
- __gmpz_init_set_si(__e_acsl_8,0L);
- __e_acsl_div_guard = __gmpz_cmp((__mpz_struct const *)(__e_acsl_7),
- (__mpz_struct const *)(__e_acsl_8));
- __gmpz_init(__e_acsl_div);
- /*@ assert E_ACSL: 5 ≢ 0; */
- e_acsl_assert(! (__e_acsl_div_guard == 0),(char *)"Postcondition",
- (char *)"atp_NORMAL_computeAverageAccel",(char *)"5 == 0",
- 11);
- __gmpz_tdiv_q(__e_acsl_div,(__mpz_struct const *)(__e_acsl_add_4),
- (__mpz_struct const *)(__e_acsl_7));
- __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl),
- (__mpz_struct const *)(__e_acsl_div));
- e_acsl_assert(__e_acsl_eq == 0,(char *)"Postcondition",
- (char *)"atp_NORMAL_computeAverageAccel",
- (char *)"*\\old(AverageAccel) ==\n(((((*\\old(Accel))[4]+(*\\old(Accel))[3])+(*\\old(Accel))[2])+(*\\old(Accel))[1])+(*\n \\old(Accel))[0])/5",
- 10);
- __delete_block((void *)(& Accel));
- __delete_block((void *)(& AverageAccel));
- __gmpz_clear(__e_acsl);
- __gmpz_clear(__e_acsl_2);
- __gmpz_clear(__e_acsl_3);
- __gmpz_clear(__e_acsl_add);
- __gmpz_clear(__e_acsl_4);
- __gmpz_clear(__e_acsl_add_2);
- __gmpz_clear(__e_acsl_5);
- __gmpz_clear(__e_acsl_add_3);
- __gmpz_clear(__e_acsl_6);
- __gmpz_clear(__e_acsl_add_4);
- __gmpz_clear(__e_acsl_7);
- __gmpz_clear(__e_acsl_8);
- __gmpz_clear(__e_acsl_div);
- return;
- }
-}
-
-int main(void)
-{
- int __retres;
- ArrayInt Accel;
- int av;
- __store_block((void *)(& av),4U);
- __store_block((void *)(Accel),20U);
- __initialize((void *)(Accel),sizeof(int));
- Accel[0] = 1;
- __initialize((void *)(& Accel[1]),sizeof(int));
- Accel[1] = 2;
- __initialize((void *)(& Accel[2]),sizeof(int));
- Accel[2] = 3;
- __initialize((void *)(& Accel[3]),sizeof(int));
- Accel[3] = 4;
- __initialize((void *)(& Accel[4]),sizeof(int));
- Accel[4] = 5;
- __e_acsl_atp_NORMAL_computeAverageAccel(& Accel,& av);
- __retres = 0;
- __delete_block((void *)(& av));
- __delete_block((void *)(Accel));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
index 95439a4657d03a382f8b8dfff5999a0c41f6e6e2..e24a306e17224549bbc2135da6b191dde0336a60 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -1,80 +1,6 @@
/* Generated by Frama-C */
char *__e_acsl_literal_string;
char *__e_acsl_literal_string_2;
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \valid_read((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
- size_t size);
-
-/*@ ensures \result ≡ \offset(\old(ptr));
- assigns \result;
- assigns \result \from ptr;
- */
-extern __attribute__((__FC_BUILTIN__)) int __offset(void *ptr);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
/*@ behavior exists:
assumes ∃ ℤ i; 0 ≤ i < n ∧ (int)*((char *)buf+i) ≡ c;
ensures
@@ -91,13 +17,14 @@ void *memchr(void const *buf, int c, size_t n)
void *__retres;
int i;
char *s;
- __store_block((void *)(& s),4U);
- __store_block((void *)(& __retres),4U);
- __store_block((void *)(& buf),4U);
+ __store_block((void *)(& s),8UL);
+ __store_block((void *)(& __retres),8UL);
+ __store_block((void *)(& buf),8UL);
__full_init((void *)(& s));
s = (char *)buf;
i = 0;
while ((size_t)i < n) {
+ /*@ assert Value: mem_access: \valid_read(s); */
if ((int)*s == c) {
__full_init((void *)(& __retres));
__retres = (void *)s;
@@ -134,13 +61,13 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
void const *__e_acsl_at_2;
int __e_acsl_at;
void *__retres;
- __store_block((void *)(& __retres),4U);
- __store_block((void *)(& buf),4U);
+ __store_block((void *)(& __retres),8UL);
+ __store_block((void *)(& buf),8UL);
{
int __e_acsl_forall_2;
- unsigned int __e_acsl_k;
+ unsigned long __e_acsl_k;
__e_acsl_forall_2 = 1;
- __e_acsl_k = (unsigned int)0;
+ __e_acsl_k = (unsigned long)0;
while (1) {
if (__e_acsl_k < n) ; else break;
{
@@ -162,13 +89,13 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_at_4 = __e_acsl_forall_2;
}
__e_acsl_at_3 = c;
- __store_block((void *)(& __e_acsl_at_2),4U);
+ __store_block((void *)(& __e_acsl_at_2),8UL);
__e_acsl_at_2 = buf;
{
int __e_acsl_exists;
- unsigned int __e_acsl_i;
+ unsigned long __e_acsl_i;
__e_acsl_exists = 0;
- __e_acsl_i = (unsigned int)0;
+ __e_acsl_i = (unsigned long)0;
while (1) {
if (__e_acsl_i < n) ; else break;
{
@@ -196,14 +123,14 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
if (! __e_acsl_at) __e_acsl_implies = 1;
else {
int __e_acsl_forall;
- unsigned int __e_acsl_j;
+ unsigned long __e_acsl_j;
__e_acsl_forall = 1;
- __e_acsl_j = (unsigned int)0;
+ __e_acsl_j = (unsigned long)0;
while (1) {
{
int __e_acsl_offset;
__e_acsl_offset = __offset(__retres);
- if (__e_acsl_j < (unsigned int)__e_acsl_offset) ; else break;
+ if (__e_acsl_j < (unsigned long)__e_acsl_offset) ; else break;
}
{
int __e_acsl_valid_read_2;
@@ -256,9 +183,9 @@ int main(void)
{
int __retres;
__e_acsl_memory_init();
- __e_acsl_memchr((void const *)__e_acsl_literal_string,'o',(unsigned int)4);
+ __e_acsl_memchr((void const *)__e_acsl_literal_string,'o',(unsigned long)4);
__e_acsl_memchr((void const *)__e_acsl_literal_string_2,'o',
- (unsigned int)4);
+ (unsigned long)4);
__retres = 0;
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c
deleted file mode 100644
index 4405fd55d8d2b5712208daeb6c6de7bf1dcd5f1c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c
+++ /dev/null
@@ -1,412 +0,0 @@
-/* Generated by Frama-C */
-char *__e_acsl_literal_string;
-char *__e_acsl_literal_string_2;
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ requires ¬\initialized(z);
- ensures \valid(\old(z));
- assigns *z;
- assigns *z \from __e_acsl_init;
- allocates \old(z);
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
-
-/*@ requires ¬\initialized(z);
- ensures \valid(\old(z));
- ensures \initialized(\old(z));
- assigns *z;
- assigns *z \from n;
- allocates \old(z);
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_ui(__mpz_struct * /*[1]*/ z,
- unsigned long n);
-
-/*@ requires ¬\initialized(z);
- ensures \valid(\old(z));
- ensures \initialized(\old(z));
- assigns *z;
- assigns *z \from n;
- allocates \old(z);
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
- long n);
-
-/*@ requires \valid_read(z_orig);
- requires \valid(z);
- assigns *z;
- assigns *z \from *z_orig;
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_set(__mpz_struct * /*[1]*/ z,
- __mpz_struct const * /*[1]*/ z_orig);
-
-/*@ requires \valid(x);
- assigns *x;
- assigns *x \from *x; */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-
-/*@ requires \valid_read(z1);
- requires \valid_read(z2);
- assigns \result;
- assigns \result \from *z1, *z2;
- */
-extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
- __mpz_struct const * /*[1]*/ z2);
-
-/*@ requires \valid(z1);
- requires \valid_read(z2);
- requires \valid_read(z3);
- assigns *z1;
- assigns *z1 \from *z2, *z3;
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
- __mpz_struct const * /*[1]*/ z2,
- __mpz_struct const * /*[1]*/ z3);
-
-/*@ requires \valid_read(z);
- assigns \result;
- assigns \result \from *z; */
-extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
-
-/*@ ensures \result ≡ \offset(\old(ptr));
- assigns \result;
- assigns \result \from ptr;
- */
-extern __attribute__((__FC_BUILTIN__)) int __offset(void *ptr);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
-/*@ behavior exists:
- assumes ∃ ℤ i; 0 ≤ i < n ∧ (int)*((char *)buf+i) ≡ c;
- ensures
- ∀ int j;
- 0 ≤ j < \offset((char *)\result) ⇒
- (int)*((char *)\old(buf)+j) ≢ \old(c);
-
- behavior not_exists:
- assumes ∀ ℤ k; 0 ≤ k < n ⇒ (int)*((char *)buf+k) ≢ c;
- ensures \result ≡ (void *)0;
- */
-void *memchr(void const *buf, int c, size_t n)
-{
- void *__retres;
- int i;
- char *s;
- __store_block((void *)(& s),4U);
- __store_block((void *)(& __retres),4U);
- __store_block((void *)(& buf),4U);
- __full_init((void *)(& s));
- s = (char *)buf;
- i = 0;
- while ((size_t)i < n) {
- if ((int)*s == c) {
- __full_init((void *)(& __retres));
- __retres = (void *)s;
- goto return_label;
- }
- __full_init((void *)(& s));
- s ++;
- i ++;
- }
- __full_init((void *)(& __retres));
- __retres = (void *)0;
- return_label:
- __delete_block((void *)(& buf));
- __delete_block((void *)(& s));
- __delete_block((void *)(& __retres));
- return __retres;
-}
-
-/*@ behavior exists:
- assumes ∃ ℤ i; 0 ≤ i < n ∧ (int)*((char *)buf+i) ≡ c;
- ensures
- ∀ int j;
- 0 ≤ j < \offset((char *)\result) ⇒
- (int)*((char *)\old(buf)+j) ≢ \old(c);
-
- behavior not_exists:
- assumes ∀ ℤ k; 0 ≤ k < n ⇒ (int)*((char *)buf+k) ≢ c;
- ensures \result ≡ (void *)0;
- */
-void *__e_acsl_memchr(void const *buf, int c, size_t n)
-{
- int __e_acsl_at_4;
- int __e_acsl_at_3;
- void const *__e_acsl_at_2;
- int __e_acsl_at;
- void *__retres;
- __store_block((void *)(& __retres),4U);
- __store_block((void *)(& buf),4U);
- {
- int __e_acsl_forall_2;
- mpz_t __e_acsl_k;
- __e_acsl_forall_2 = 1;
- __gmpz_init(__e_acsl_k);
- {
- mpz_t __e_acsl_6;
- __gmpz_init_set_si(__e_acsl_6,(long)0);
- __gmpz_set(__e_acsl_k,(__mpz_struct const *)(__e_acsl_6));
- __gmpz_clear(__e_acsl_6);
- }
- while (1) {
- {
- mpz_t __e_acsl_n_2;
- int __e_acsl_lt_3;
- __gmpz_init_set_ui(__e_acsl_n_2,(unsigned long)n);
- __e_acsl_lt_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_k),
- (__mpz_struct const *)(__e_acsl_n_2));
- if (__e_acsl_lt_3 < 0) ; else break;
- __gmpz_clear(__e_acsl_n_2);
- }
- {
- unsigned long __e_acsl_k_2;
- mpz_t __e_acsl_cast_3;
- mpz_t __e_acsl_c_2;
- int __e_acsl_ne_2;
- __e_acsl_k_2 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_k));
- __gmpz_init_set_si(__e_acsl_cast_3,
- (long)((int)*((char *)buf + __e_acsl_k_2)));
- __gmpz_init_set_si(__e_acsl_c_2,(long)c);
- __e_acsl_ne_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_cast_3),
- (__mpz_struct const *)(__e_acsl_c_2));
- __gmpz_clear(__e_acsl_cast_3);
- __gmpz_clear(__e_acsl_c_2);
- if (__e_acsl_ne_2 != 0) ;
- else {
- __e_acsl_forall_2 = 0;
- goto e_acsl_end_loop3;
- }
- }
- {
- mpz_t __e_acsl_7;
- mpz_t __e_acsl_add_3;
- __gmpz_init_set_si(__e_acsl_7,1L);
- __gmpz_init(__e_acsl_add_3);
- __gmpz_add(__e_acsl_add_3,(__mpz_struct const *)(__e_acsl_k),
- (__mpz_struct const *)(__e_acsl_7));
- __gmpz_set(__e_acsl_k,(__mpz_struct const *)(__e_acsl_add_3));
- __gmpz_clear(__e_acsl_7);
- __gmpz_clear(__e_acsl_add_3);
- }
- }
- e_acsl_end_loop3: ;
- __e_acsl_at_4 = __e_acsl_forall_2;
- __gmpz_clear(__e_acsl_k);
- }
- __e_acsl_at_3 = c;
- __store_block((void *)(& __e_acsl_at_2),4U);
- __e_acsl_at_2 = buf;
- {
- int __e_acsl_exists;
- mpz_t __e_acsl_i;
- __e_acsl_exists = 0;
- __gmpz_init(__e_acsl_i);
- {
- mpz_t __e_acsl;
- __gmpz_init_set_si(__e_acsl,(long)0);
- __gmpz_set(__e_acsl_i,(__mpz_struct const *)(__e_acsl));
- __gmpz_clear(__e_acsl);
- }
- while (1) {
- {
- mpz_t __e_acsl_n;
- int __e_acsl_lt;
- __gmpz_init_set_ui(__e_acsl_n,(unsigned long)n);
- __e_acsl_lt = __gmpz_cmp((__mpz_struct const *)(__e_acsl_i),
- (__mpz_struct const *)(__e_acsl_n));
- if (__e_acsl_lt < 0) ; else break;
- __gmpz_clear(__e_acsl_n);
- }
- {
- unsigned long __e_acsl_i_2;
- mpz_t __e_acsl_cast;
- mpz_t __e_acsl_c;
- int __e_acsl_eq;
- __e_acsl_i_2 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_i));
- __gmpz_init_set_si(__e_acsl_cast,
- (long)((int)*((char *)buf + __e_acsl_i_2)));
- __gmpz_init_set_si(__e_acsl_c,(long)c);
- __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_cast),
- (__mpz_struct const *)(__e_acsl_c));
- __gmpz_clear(__e_acsl_cast);
- __gmpz_clear(__e_acsl_c);
- if (! (__e_acsl_eq == 0)) ;
- else {
- __e_acsl_exists = 1;
- goto e_acsl_end_loop1;
- }
- }
- {
- mpz_t __e_acsl_2;
- mpz_t __e_acsl_add;
- __gmpz_init_set_si(__e_acsl_2,1L);
- __gmpz_init(__e_acsl_add);
- __gmpz_add(__e_acsl_add,(__mpz_struct const *)(__e_acsl_i),
- (__mpz_struct const *)(__e_acsl_2));
- __gmpz_set(__e_acsl_i,(__mpz_struct const *)(__e_acsl_add));
- __gmpz_clear(__e_acsl_2);
- __gmpz_clear(__e_acsl_add);
- }
- }
- e_acsl_end_loop1: ;
- __e_acsl_at = __e_acsl_exists;
- __gmpz_clear(__e_acsl_i);
- }
- __retres = memchr(buf,c,n);
- {
- int __e_acsl_implies;
- int __e_acsl_implies_2;
- if (! __e_acsl_at) __e_acsl_implies = 1;
- else {
- int __e_acsl_forall;
- mpz_t __e_acsl_j;
- __e_acsl_forall = 1;
- __gmpz_init(__e_acsl_j);
- {
- mpz_t __e_acsl_4;
- __gmpz_init_set_si(__e_acsl_4,(long)0);
- __gmpz_set(__e_acsl_j,(__mpz_struct const *)(__e_acsl_4));
- __gmpz_clear(__e_acsl_4);
- }
- while (1) {
- {
- int __e_acsl_offset;
- mpz_t __e_acsl_offset_2;
- int __e_acsl_lt_2;
- __e_acsl_offset = __offset(__retres);
- __gmpz_init_set_si(__e_acsl_offset_2,(long)__e_acsl_offset);
- __e_acsl_lt_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_j),
- (__mpz_struct const *)(__e_acsl_offset_2));
- if (__e_acsl_lt_2 < 0) ; else break;
- __gmpz_clear(__e_acsl_offset_2);
- }
- {
- unsigned long __e_acsl_j_2;
- mpz_t __e_acsl_cast_2;
- mpz_t __e_acsl_3;
- int __e_acsl_ne;
- __e_acsl_j_2 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_j));
- __gmpz_init_set_si(__e_acsl_cast_2,
- (long)((int)*((char *)__e_acsl_at_2 + __e_acsl_j_2)));
- __gmpz_init_set_si(__e_acsl_3,(long)__e_acsl_at_3);
- __e_acsl_ne = __gmpz_cmp((__mpz_struct const *)(__e_acsl_cast_2),
- (__mpz_struct const *)(__e_acsl_3));
- __gmpz_clear(__e_acsl_cast_2);
- __gmpz_clear(__e_acsl_3);
- if (__e_acsl_ne != 0) ;
- else {
- __e_acsl_forall = 0;
- goto e_acsl_end_loop2;
- }
- }
- {
- mpz_t __e_acsl_5;
- mpz_t __e_acsl_add_2;
- __gmpz_init_set_si(__e_acsl_5,1L);
- __gmpz_init(__e_acsl_add_2);
- __gmpz_add(__e_acsl_add_2,(__mpz_struct const *)(__e_acsl_j),
- (__mpz_struct const *)(__e_acsl_5));
- __gmpz_set(__e_acsl_j,(__mpz_struct const *)(__e_acsl_add_2));
- __gmpz_clear(__e_acsl_5);
- __gmpz_clear(__e_acsl_add_2);
- }
- }
- e_acsl_end_loop2: ;
- __e_acsl_implies = __e_acsl_forall;
- __gmpz_clear(__e_acsl_j);
- }
- e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",(char *)"memchr",
- (char *)"\\old(\\exists integer i; 0 <= i < n && (int)*((char *)buf+i) == c) ==>\n(\\forall int j;\n 0 <= j < \\offset((char *)\\result) ==>\n (int)*((char *)\\old(buf)+j) != \\old(c))",
- 13);
- if (! __e_acsl_at_4) __e_acsl_implies_2 = 1;
- else __e_acsl_implies_2 = __retres == (void *)0;
- e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
- (char *)"memchr",
- (char *)"\\old(\\forall integer k; 0 <= k < n ==> (int)*((char *)buf+k) != c) ==>\n\\result == (void *)0",
- 16);
- __delete_block((void *)(& buf));
- __delete_block((void *)(& __retres));
- return __retres;
- }
-}
-
-void __e_acsl_memory_init(void)
-{
- __e_acsl_literal_string = "toto";
- __store_block((void *)__e_acsl_literal_string,sizeof("toto"));
- __full_init((void *)__e_acsl_literal_string);
- __literal_string((void *)__e_acsl_literal_string);
- __e_acsl_literal_string_2 = "tata";
- __store_block((void *)__e_acsl_literal_string_2,sizeof("tata"));
- __full_init((void *)__e_acsl_literal_string_2);
- __literal_string((void *)__e_acsl_literal_string_2);
- return;
-}
-
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init();
- __e_acsl_memchr((void const *)__e_acsl_literal_string,'o',(unsigned int)4);
- __e_acsl_memchr((void const *)__e_acsl_literal_string_2,'o',
- (unsigned int)4);
- __retres = 0;
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
index 97bd608c9bf3e8d9404530bb6027dcb372b6a2e0..e61c3232854b6664eca6470db61ee80eaccc021e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
@@ -1,84 +1,4 @@
/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-typedef unsigned int ino_t;
-typedef unsigned int gid_t;
-typedef unsigned int uid_t;
-typedef long time_t;
-typedef unsigned int blkcnt_t;
-typedef unsigned int blksize_t;
-typedef unsigned int dev_t;
-typedef unsigned int mode_t;
-typedef unsigned int nlink_t;
-typedef long off_t;
-struct stat {
- dev_t st_dev ;
- ino_t st_ino ;
- mode_t st_mode ;
- nlink_t st_nlink ;
- uid_t st_uid ;
- gid_t st_gid ;
- dev_t st_rdev ;
- off_t st_size ;
- time_t st_atime ;
- time_t st_mtime ;
- time_t st_ctime ;
- blksize_t st_blksize ;
- blkcnt_t st_blocks ;
-};
-struct __fc_pos_t {
- unsigned long __fc_stdio_position ;
-};
-typedef struct __fc_pos_t fpos_t;
-struct __fc_FILE {
- unsigned int __fc_stdio_id ;
- fpos_t __fc_position ;
- char __fc_error ;
- char __fc_eof ;
- int __fc_flags ;
- struct stat *__fc_inode ;
- unsigned char *__fc_real_data ;
- int __fc_real_data_max_size ;
-};
-typedef struct __fc_FILE FILE;
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
-extern FILE *stdout;
-
-FILE __fc_fopen[512];
-FILE * const __p_fc_fopen = __fc_fopen;
-/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
-extern int printf(char const *format , ...);
-
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c
deleted file mode 100644
index 97bd608c9bf3e8d9404530bb6027dcb372b6a2e0..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c
+++ /dev/null
@@ -1,97 +0,0 @@
-/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-typedef unsigned int ino_t;
-typedef unsigned int gid_t;
-typedef unsigned int uid_t;
-typedef long time_t;
-typedef unsigned int blkcnt_t;
-typedef unsigned int blksize_t;
-typedef unsigned int dev_t;
-typedef unsigned int mode_t;
-typedef unsigned int nlink_t;
-typedef long off_t;
-struct stat {
- dev_t st_dev ;
- ino_t st_ino ;
- mode_t st_mode ;
- nlink_t st_nlink ;
- uid_t st_uid ;
- gid_t st_gid ;
- dev_t st_rdev ;
- off_t st_size ;
- time_t st_atime ;
- time_t st_mtime ;
- time_t st_ctime ;
- blksize_t st_blksize ;
- blkcnt_t st_blocks ;
-};
-struct __fc_pos_t {
- unsigned long __fc_stdio_position ;
-};
-typedef struct __fc_pos_t fpos_t;
-struct __fc_FILE {
- unsigned int __fc_stdio_id ;
- fpos_t __fc_position ;
- char __fc_error ;
- char __fc_eof ;
- int __fc_flags ;
- struct stat *__fc_inode ;
- unsigned char *__fc_real_data ;
- int __fc_real_data_max_size ;
-};
-typedef struct __fc_FILE FILE;
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
-extern FILE *stdout;
-
-FILE __fc_fopen[512];
-FILE * const __p_fc_fopen = __fc_fopen;
-/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
-extern int printf(char const *format , ...);
-
-int main(void)
-{
- int __retres;
- int x;
- int t[2];
- int i;
- x = 0;
- i = 1;
- t[0] = 1;
- t[1] = 2;
- printf("X=%d, t[0]=%d, t[1]=%d\n",x,t[0],t[i]);
- __retres = 0;
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
index 11363caf14febf93e83232c0264b7384fae1155b..3a3ad0b23b1c2ac64a6b399e03151c0c2b8f25a4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
@@ -1,174 +1,15 @@
/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
struct spongeStateStruct {
unsigned char __attribute__((__aligned__(32))) state[1600 / 8] ;
unsigned char __attribute__((__aligned__(32))) dataQueue[1536 / 8] ;
unsigned int bitsInQueue ;
} __attribute__((__aligned__(32)));
typedef struct spongeStateStruct spongeState;
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-void *__malloc(size_t size);
-
-void __free(void *p);
-
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ assigns \result;
- assigns \result \from ptr; */
-extern __attribute__((__FC_BUILTIN__)) int __freeable(void *ptr);
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \valid_read((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
- size_t size);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
- size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@ assigns __fc_heap_status, \result;
- assigns __fc_heap_status \from size, __fc_heap_status;
- assigns \result \from size, __fc_heap_status;
- allocates \result;
-
- behavior allocation:
- assumes is_allocable(size);
- ensures \fresh{Old, Here}(\result,\old(size));
- assigns __fc_heap_status, \result;
- assigns __fc_heap_status \from size, __fc_heap_status;
- assigns \result \from size, __fc_heap_status;
-
- behavior no_allocation:
- assumes ¬is_allocable(size);
- ensures \result ≡ \null;
- assigns \result;
- assigns \result \from \nothing;
- allocates \nothing;
-
- complete behaviors no_allocation, allocation;
- disjoint behaviors no_allocation, allocation;
- */
-void *__e_acsl_malloc(size_t size)
-{
- void *__retres;
- __store_block((void *)(& __retres),4U);
- __retres = __malloc(size);
- __delete_block((void *)(& __retres));
- return __retres;
-}
-
-/*@ assigns __fc_heap_status;
- assigns __fc_heap_status \from __fc_heap_status;
- frees p;
-
- behavior deallocation:
- assumes p ≢ \null;
- requires freeable: \freeable(p);
- ensures \allocable(\old(p));
- assigns __fc_heap_status;
- assigns __fc_heap_status \from __fc_heap_status;
-
- behavior no_deallocation:
- assumes p ≡ \null;
- assigns \nothing;
- allocates \nothing;
-
- complete behaviors no_deallocation, deallocation;
- disjoint behaviors no_deallocation, deallocation;
- */
-void __e_acsl_free(void *p)
-{
- int __e_acsl_at;
- {
- int __e_acsl_implies;
- __store_block((void *)(& p),4U);
- if (! (p != (void *)0)) __e_acsl_implies = 1;
- else {
- int __e_acsl_freeable;
- __e_acsl_freeable = __freeable(p);
- __e_acsl_implies = __e_acsl_freeable;
- }
- e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
- (char *)"p != \\null ==> \\freeable(p)",178);
- __store_block((void *)(& __e_acsl_at),4U);
- __e_acsl_at = p != (void *)0;
- __free(p);
- }
- __delete_block((void *)(& p));
- return;
-}
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
-
-*/
int main(void)
{
int __retres;
spongeState *state;
- __store_block((void *)(& state),4U);
+ __store_block((void *)(& state),8UL);
__full_init((void *)(& state));
state = (spongeState *)__e_acsl_malloc(sizeof(spongeState));
__initialize((void *)(& state->bitsInQueue),sizeof(unsigned int));
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
deleted file mode 100644
index 85b487196c33c8be906d1bd6ce30cd132320fa6c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
+++ /dev/null
@@ -1,262 +0,0 @@
-/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-struct spongeStateStruct {
- unsigned char __attribute__((__aligned__(32))) state[1600 / 8] ;
- unsigned char __attribute__((__aligned__(32))) dataQueue[1536 / 8] ;
- unsigned int bitsInQueue ;
-} __attribute__((__aligned__(32)));
-typedef struct spongeStateStruct spongeState;
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-void *__malloc(size_t size);
-
-void __free(void *p);
-
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ requires ¬\initialized(z);
- ensures \valid(\old(z));
- assigns *z;
- assigns *z \from __e_acsl_init;
- allocates \old(z);
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
-
-/*@ requires ¬\initialized(z);
- ensures \valid(\old(z));
- ensures \initialized(\old(z));
- assigns *z;
- assigns *z \from n;
- allocates \old(z);
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_ui(__mpz_struct * /*[1]*/ z,
- unsigned long n);
-
-/*@ requires ¬\initialized(z);
- ensures \valid(\old(z));
- ensures \initialized(\old(z));
- assigns *z;
- assigns *z \from n;
- allocates \old(z);
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
- long n);
-
-/*@ requires \valid(x);
- assigns *x;
- assigns *x \from *x; */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-
-/*@ requires \valid_read(z1);
- requires \valid_read(z2);
- assigns \result;
- assigns \result \from *z1, *z2;
- */
-extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
- __mpz_struct const * /*[1]*/ z2);
-
-/*@ requires \valid(z1);
- requires \valid_read(z2);
- requires \valid_read(z3);
- assigns *z1;
- assigns *z1 \from *z2, *z3;
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
- __mpz_struct const * /*[1]*/ z2,
- __mpz_struct const * /*[1]*/ z3);
-
-/*@ requires \valid_read(z);
- assigns \result;
- assigns \result \from *z; */
-extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
-
-/*@ assigns \result;
- assigns \result \from ptr; */
-extern __attribute__((__FC_BUILTIN__)) int __freeable(void *ptr);
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
- size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@ assigns __fc_heap_status, \result;
- assigns __fc_heap_status \from size, __fc_heap_status;
- assigns \result \from size, __fc_heap_status;
- allocates \result;
-
- behavior allocation:
- assumes is_allocable(size);
- ensures \fresh{Old, Here}(\result,\old(size));
- assigns __fc_heap_status, \result;
- assigns __fc_heap_status \from size, __fc_heap_status;
- assigns \result \from size, __fc_heap_status;
-
- behavior no_allocation:
- assumes ¬is_allocable(size);
- ensures \result ≡ \null;
- assigns \result;
- assigns \result \from \nothing;
- allocates \nothing;
-
- complete behaviors no_allocation, allocation;
- disjoint behaviors no_allocation, allocation;
- */
-void *__e_acsl_malloc(size_t size)
-{
- void *__retres;
- __store_block((void *)(& __retres),4U);
- __retres = __malloc(size);
- __delete_block((void *)(& __retres));
- return __retres;
-}
-
-/*@ assigns __fc_heap_status;
- assigns __fc_heap_status \from __fc_heap_status;
- frees p;
-
- behavior deallocation:
- assumes p ≢ \null;
- requires freeable: \freeable(p);
- ensures \allocable(\old(p));
- assigns __fc_heap_status;
- assigns __fc_heap_status \from __fc_heap_status;
-
- behavior no_deallocation:
- assumes p ≡ \null;
- assigns \nothing;
- allocates \nothing;
-
- complete behaviors no_deallocation, deallocation;
- disjoint behaviors no_deallocation, deallocation;
- */
-void __e_acsl_free(void *p)
-{
- int __e_acsl_at;
- {
- int __e_acsl_implies;
- __store_block((void *)(& p),4U);
- if (! (p != (void *)0)) __e_acsl_implies = 1;
- else {
- int __e_acsl_freeable;
- __e_acsl_freeable = __freeable(p);
- __e_acsl_implies = __e_acsl_freeable;
- }
- e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
- (char *)"p != \\null ==> \\freeable(p)",178);
- __store_block((void *)(& __e_acsl_at),4U);
- __e_acsl_at = p != (void *)0;
- __free(p);
- }
- __delete_block((void *)(& p));
- return;
-}
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
-
-*/
-int main(void)
-{
- int __retres;
- spongeState *state;
- __store_block((void *)(& state),4U);
- __full_init((void *)(& state));
- state = (spongeState *)__e_acsl_malloc(sizeof(spongeState));
- __initialize((void *)(& state->bitsInQueue),sizeof(unsigned int));
- state->bitsInQueue = (unsigned int)16;
- /*@ assert ¬\initialized(&state->dataQueue[state->bitsInQueue/8]); */
- {
- mpz_t __e_acsl;
- mpz_t __e_acsl_2;
- mpz_t __e_acsl_3;
- int __e_acsl_div_guard;
- mpz_t __e_acsl_div;
- unsigned long __e_acsl_4;
- int __e_acsl_initialized;
- __gmpz_init_set_ui(__e_acsl,(unsigned long)state->bitsInQueue);
- __gmpz_init_set_si(__e_acsl_2,(long)8);
- __gmpz_init_set_si(__e_acsl_3,0L);
- __e_acsl_div_guard = __gmpz_cmp((__mpz_struct const *)(__e_acsl_2),
- (__mpz_struct const *)(__e_acsl_3));
- __gmpz_init(__e_acsl_div);
- /*@ assert E_ACSL: 8 ≢ 0; */
- e_acsl_assert(! (__e_acsl_div_guard == 0),(char *)"Assertion",
- (char *)"main",(char *)"8 == 0",24);
- __gmpz_tdiv_q(__e_acsl_div,(__mpz_struct const *)(__e_acsl),
- (__mpz_struct const *)(__e_acsl_2));
- __e_acsl_4 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_div));
- __e_acsl_initialized = __initialized((void *)(& state->dataQueue[__e_acsl_4]),
- sizeof(unsigned char __attribute__((
- __aligned__(32)))));
- e_acsl_assert(! __e_acsl_initialized,(char *)"Assertion",(char *)"main",
- (char *)"!\\initialized(&state->dataQueue[state->bitsInQueue/8])",
- 24);
- __gmpz_clear(__e_acsl);
- __gmpz_clear(__e_acsl_2);
- __gmpz_clear(__e_acsl_3);
- __gmpz_clear(__e_acsl_div);
- }
- __e_acsl_free((void *)state);
- __retres = 0;
- __delete_block((void *)(& state));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
index de9f0a6c8650efc82f34727701c81f9418787def..973237653c9cfbff2b49d87d6dbd01b916815bbd 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
@@ -1,67 +1,4 @@
/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
int global_i;
int *global_i_ptr = & global_i;
@@ -97,9 +34,9 @@ void __e_acsl_loop(void)
void __e_acsl_memory_init(void)
{
- __store_block((void *)(& global_i_ptr),4U);
+ __store_block((void *)(& global_i_ptr),8UL);
__full_init((void *)(& global_i_ptr));
- __store_block((void *)(& global_i),4U);
+ __store_block((void *)(& global_i),4UL);
__full_init((void *)(& global_i));
return;
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts14782.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts14782.c
deleted file mode 100644
index 3be5246cfb3f3f6e7d3d20a7debc1a17dc60abb3..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts14782.c
+++ /dev/null
@@ -1,151 +0,0 @@
-/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ requires ¬\initialized(z);
- ensures \valid(\old(z));
- ensures \initialized(\old(z));
- assigns *z;
- assigns *z \from n;
- allocates \old(z);
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
- long n);
-
-/*@ requires \valid(x);
- assigns *x;
- assigns *x \from *x; */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-
-/*@ requires \valid_read(z1);
- requires \valid_read(z2);
- assigns \result;
- assigns \result \from *z1, *z2;
- */
-extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
- __mpz_struct const * /*[1]*/ z2);
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
-int global_i;
-
-int *global_i_ptr = & global_i;
-int global_i = 0;
-/*@ requires global_i ≡ 0;
- requires \valid(global_i_ptr);
- requires global_i_ptr ≡ &global_i;
- */
-void loop(void)
-{
- return;
-}
-
-/*@ requires global_i ≡ 0;
- requires \valid(global_i_ptr);
- requires global_i_ptr ≡ &global_i;
- */
-void __e_acsl_loop(void)
-{
- {
- mpz_t __e_acsl_global_i;
- mpz_t __e_acsl;
- int __e_acsl_eq;
- int __e_acsl_valid;
- __gmpz_init_set_si(__e_acsl_global_i,(long)global_i);
- __gmpz_init_set_si(__e_acsl,(long)0);
- __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_global_i),
- (__mpz_struct const *)(__e_acsl));
- e_acsl_assert(__e_acsl_eq == 0,(char *)"Precondition",(char *)"loop",
- (char *)"global_i == 0",11);
- __e_acsl_valid = __valid((void *)global_i_ptr,sizeof(int));
- e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"loop",
- (char *)"\\valid(global_i_ptr)",12);
- e_acsl_assert(global_i_ptr == & global_i,(char *)"Precondition",
- (char *)"loop",(char *)"global_i_ptr == &global_i",13);
- __gmpz_clear(__e_acsl_global_i);
- __gmpz_clear(__e_acsl);
- loop();
- }
- return;
-}
-
-void __e_acsl_memory_init(void)
-{
- __store_block((void *)(& global_i_ptr),4U);
- __full_init((void *)(& global_i_ptr));
- __store_block((void *)(& global_i),4U);
- __full_init((void *)(& global_i));
- return;
-}
-
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init();
- __e_acsl_loop();
- __retres = 0;
- __delete_block((void *)(& global_i_ptr));
- __delete_block((void *)(& global_i));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
index 487a65e7f23cd3ef46b18d985612ff10757f8ba3..e12d751b4d3a3e30cab654e203fc906ceaed91b7 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
@@ -1,86 +1,14 @@
/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
struct toto {
};
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
- size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
int main(void)
{
int __retres;
struct toto s;
struct toto *p;
- __store_block((void *)(& p),4U);
- __store_block((void *)(& s),0U);
+ __store_block((void *)(& p),8UL);
+ __store_block((void *)(& s),0UL);
/*@ assert \valid(&s); */
{
int __e_acsl_valid;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
index bfd83983a86a46b25cb49bae40eb908e42a9d0cb..fc8d950d02102730b9d03e2becd77f205580c7d4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
@@ -1,83 +1,11 @@
/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
- size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
int main(void)
{
int __retres;
int a;
int *p;
- __store_block((void *)(& p),4U);
- __store_block((void *)(& a),4U);
+ __store_block((void *)(& p),8UL);
+ __store_block((void *)(& a),4UL);
__full_init((void *)(& a));
a = 10;
goto lbl_1;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts17172.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts17172.c
deleted file mode 100644
index bfd83983a86a46b25cb49bae40eb908e42a9d0cb..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts17172.c
+++ /dev/null
@@ -1,111 +0,0 @@
-/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
- size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
-int main(void)
-{
- int __retres;
- int a;
- int *p;
- __store_block((void *)(& p),4U);
- __store_block((void *)(& a),4U);
- __full_init((void *)(& a));
- a = 10;
- goto lbl_1;
- lbl_2:
- /*@ assert \valid(p); */
- {
- int __e_acsl_initialized;
- int __e_acsl_and;
- __e_acsl_initialized = __initialized((void *)(& p),sizeof(int *));
- if (__e_acsl_initialized) {
- int __e_acsl_valid;
- __e_acsl_valid = __valid((void *)p,sizeof(int));
- __e_acsl_and = __e_acsl_valid;
- }
- else __e_acsl_and = 0;
- e_acsl_assert(__e_acsl_and,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(p)",13);
- }
- __retres = 0;
- goto return_label;
- lbl_1: __full_init((void *)(& p));
- p = & a;
- goto lbl_2;
- return_label:
- __delete_block((void *)(& p));
- __delete_block((void *)(& a));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
index bfd83983a86a46b25cb49bae40eb908e42a9d0cb..fc8d950d02102730b9d03e2becd77f205580c7d4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
@@ -1,83 +1,11 @@
/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
- size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
int main(void)
{
int __retres;
int a;
int *p;
- __store_block((void *)(& p),4U);
- __store_block((void *)(& a),4U);
+ __store_block((void *)(& p),8UL);
+ __store_block((void *)(& a),4UL);
__full_init((void *)(& a));
a = 10;
goto lbl_1;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts17182.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts17182.c
deleted file mode 100644
index bfd83983a86a46b25cb49bae40eb908e42a9d0cb..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts17182.c
+++ /dev/null
@@ -1,111 +0,0 @@
-/* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
- size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
-int main(void)
-{
- int __retres;
- int a;
- int *p;
- __store_block((void *)(& p),4U);
- __store_block((void *)(& a),4U);
- __full_init((void *)(& a));
- a = 10;
- goto lbl_1;
- lbl_2:
- /*@ assert \valid(p); */
- {
- int __e_acsl_initialized;
- int __e_acsl_and;
- __e_acsl_initialized = __initialized((void *)(& p),sizeof(int *));
- if (__e_acsl_initialized) {
- int __e_acsl_valid;
- __e_acsl_valid = __valid((void *)p,sizeof(int));
- __e_acsl_and = __e_acsl_valid;
- }
- else __e_acsl_and = 0;
- e_acsl_assert(__e_acsl_and,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(p)",13);
- }
- __retres = 0;
- goto return_label;
- lbl_1: __full_init((void *)(& p));
- p = & a;
- goto lbl_2;
- return_label:
- __delete_block((void *)(& p));
- __delete_block((void *)(& a));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
index 32445cb1f02704a681cefc0a633a3b5df006e254..e14e15af6d5011d27b5468b767538f6b8f9f7760 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -2,98 +2,14 @@
char *__e_acsl_literal_string_3;
char *__e_acsl_literal_string;
char *__e_acsl_literal_string_2;
-struct __anonstruct___mpz_struct_1 {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
-typedef unsigned int size_t;
-/*@ requires predicate ≢ 0;
- assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
- char *kind,
- char *fct,
- char *pred_txt,
- int line);
-
-/*@
-model __mpz_struct { ℤ n };
-*/
-int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(size_t n)
- reads __fc_heap_status;
-
- }
- */
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1)); */
-extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-
-/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \valid_read((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
- size_t size);
-
-/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures
- \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
- assigns \result;
- assigns \result \from *((char *)ptr+(0 .. size-1));
- */
-extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
- size_t size);
-
-/*@ ghost extern int __e_acsl_internal_heap; */
-
-/*@ assigns __e_acsl_internal_heap;
- assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
- */
-extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-extern size_t __memory_size;
-
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
- */
char *S = (char *)"foo";
int f(void)
{
int __retres;
char *s1;
char *s2;
- __store_block((void *)(& s2),4U);
- __store_block((void *)(& s1),4U);
+ __store_block((void *)(& s2),8UL);
+ __store_block((void *)(& s1),8UL);
__full_init((void *)(& s1));
s1 = (char *)__e_acsl_literal_string;
__full_init((void *)(& s2));
@@ -153,7 +69,7 @@ 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 *)(& S),4U);
+ __store_block((void *)(& S),8UL);
__full_init((void *)(& S));
return;
}
@@ -168,13 +84,14 @@ int main(void)
int tmp;
{ /* sequence */
tmp = i;
+ /*@ assert Value: signed_overflow: -2147483648 ≤ i-1; */
i --;
;
}
if (! tmp) break;
{
char *s;
- __store_block((void *)(& s),4U);
+ __store_block((void *)(& s),8UL);
__full_init((void *)(& s));
s = (char *)__e_acsl_literal_string_3;
/*@ assert \valid_read(s); */
diff --git a/src/plugins/e-acsl/tests/bts/test_config b/src/plugins/e-acsl/tests/bts/test_config
index 31618f99b7d448ba68098010412e63a4a40aaa34..a8847da733c55d5fb572c39fd7e6fb790d466841 100644
--- a/src/plugins/e-acsl/tests/bts/test_config
+++ b/src/plugins/e-acsl/tests/bts/test_config
@@ -1,2 +1,3 @@
-OPT: -check -e-acsl -then-last -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
-OPT: -check -e-acsl -e-acsl-gmp-only -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 -load-script tests/print.cmxs -print -ocode tests/bts/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
+EXECNOW: ./scripts/testrun.sh @PTEST_NAME@ bts "" "--frama-c=@frama-c@"