diff --git a/tests/libc/coverage.c b/tests/libc/coverage.c
index 8c2b1421bfd11b12baee477e43280c7dcec33d67..42f6476d300167f9503ba91858f3132dcf79234d 100644
--- a/tests/libc/coverage.c
+++ b/tests/libc/coverage.c
@@ -1,5 +1,5 @@
/* run.config*
- DEPS: ../../share/libc/string.c
+ DEPS: ../../../share/libc/string.c
OPT: -eva-no-builtins-auto @EVA_OPTIONS@ ../../share/libc/string.c -eva -slevel 6 -metrics-eva-cover -then -metrics-libc
*/
diff --git a/tests/libc/runtime.c b/tests/libc/runtime.c
index 37647e76af9d0db77fbb02015e06d9da1bde813c..a245abd3365263b802f7f30da618e34f19bf6d68 100644
--- a/tests/libc/runtime.c
+++ b/tests/libc/runtime.c
@@ -1,6 +1,6 @@
/* run.config*
COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...)
- DEPS: ../../share/libc/__fc_runtime.c
+ DEPS: ../../../share/libc/__fc_runtime.c
CMD: gcc -D__FC_MACHDEP_X86_64 ../../share/libc/__fc_runtime.c -Wno-attributes -std=c99 -o /dev/null
OPT:
*/
diff --git a/tests/libc/string_c_generic.c b/tests/libc/string_c_generic.c
index d960a9b44fc3f2c0f3253fbec8b2eb321f1bb96b..57c5461faa5bca844da0593d31bd537eb5025100 100644
--- a/tests/libc/string_c_generic.c
+++ b/tests/libc/string_c_generic.c
@@ -1,5 +1,5 @@
/* run.config
- DEPS: ../../share/libc/string.c
+ DEPS: ../../../share/libc/string.c
STDOPT: #"-eva-no-builtins-auto -cpp-extra-args=-include../../share/libc/string.c -slevel-function strcpy:20,strncpy:5,strcmp:6,strchr:20,strrchr:20,strncat:4,memset:32,strlen:20,memcmp:8 -eva-no-skip-stdlib-specs"
*/
/* This file has been adapted from libc-test, which is licensed under the
diff --git a/tests/libc/string_c_strchr.c b/tests/libc/string_c_strchr.c
index 4179b4f27cb504bc1bc4681a9e27d20f0a627dfd..79ee7bebacedd761eb4ed6e8cdd472a2e136154a 100644
--- a/tests/libc/string_c_strchr.c
+++ b/tests/libc/string_c_strchr.c
@@ -1,5 +1,5 @@
/* run.config
- DEPS: ../../share/libc/string.c
+ DEPS: ../../../share/libc/string.c
STDOPT: #"-cpp-extra-args=-include../../share/libc/string.c -slevel-function strchr:256,main:256 -eva-slevel-merge-after-loop main -eva-no-builtins-auto -eva-no-skip-stdlib-specs"
*/
/* This file has been adapted from libc-test, which is licensed under the
diff --git a/tests/libc/string_c_strstr.c b/tests/libc/string_c_strstr.c
index 2bfbbdbe125972c5d18a5b5c70f39cd1adedcd67..e7f30e82d08091877fdbbed27640f17582651892 100644
--- a/tests/libc/string_c_strstr.c
+++ b/tests/libc/string_c_strstr.c
@@ -1,5 +1,5 @@
/* run.config
- DEPS: ../../share/libc/string.c
+ DEPS: ../../../share/libc/string.c
STDOPT: #"-cpp-extra-args=-include../../share/libc/string.c -slevel-function strstr:30 -eva-no-skip-stdlib-specs"
*/
/* This file has been adapted from libc-test, which is licensed under the
diff --git a/tests/rte/oracle/divmod.res.oracle b/tests/rte/oracle/divmod.res.oracle
index d4b45c78263955239f201d589eb84ca6352d56d0..f7f9626762ac19e218518238d3c8636174a0f0b9 100644
--- a/tests/rte/oracle/divmod.res.oracle
+++ b/tests/rte/oracle/divmod.res.oracle
@@ -1,8 +1,83 @@
[kernel] Parsing divmod.c (with preprocessing)
-[kernel] User Error: failed to run: gcc -E -C -I. -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 -o '/tmp/divmod.ce6cb94.i' '/home/bobot/Sources/frama-c/_build/default/result/divmod.c'
- this is possibly due to missing preprocessor flags;
- consider options -cpp-extra-args, -json-compilation-database or -cpp-command.
- See chapter "Preparing the Sources" in the Frama-C user manual for more details.
-[kernel] User Error: stopping on file "divmod.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[rte] annotating function main
+[rte] divmod.c:13: Warning:
+ guaranteed RTE:
+ assert
+ signed_overflow: (int)((int)(-2147483647) - 1) / (int)(-1) ≤ 2147483647;
+[rte] divmod.c:16: Warning: guaranteed RTE: assert division_by_zero: 0 ≢ 0;
+[rte] divmod.c:17: Warning:
+ guaranteed RTE:
+ assert division_by_zero: (unsigned int)(0xffffffff + 1) ≢ 0;
+[rte] divmod.c:24: Warning:
+ guaranteed RTE:
+ assert division_by_zero: (unsigned int)(0xffffffff + 1) ≢ 0;
+[rte] divmod.c:25: Warning:
+ guaranteed RTE:
+ assert
+ signed_overflow: (int)((int)(-0x7fffffff) - 1) / (int)(-1) ≤ 2147483647;
+[rte] divmod.c:36: Warning:
+ guaranteed RTE:
+ assert
+ signed_downcast:
+ (long long)((long long)(-2147483648L) / (long long)((long)(-1L))) ≤
+ 2147483647;
+/* Generated by Frama-C */
+int main(void)
+{
+ int __retres;
+ int x = 0;
+ int y = 0;
+ int z = 0;
+ unsigned int ux = (unsigned int)0;
+ unsigned int uy = (unsigned int)0;
+ unsigned int uz = (unsigned int)0;
+ /*@ assert
+ rte: signed_overflow:
+ (int)((int)(-2147483647) - 1) / (int)(-1) ≤ 2147483647;
+ */
+ z = (-2147483647 - 1) / -1;
+ z = (-2147483647 - 1) % -1;
+ /*@ assert rte: division_by_zero: 0 ≢ 0; */
+ uz = (unsigned int)(1 / 0);
+ /*@ assert rte: division_by_zero: (unsigned int)(0xffffffff + 1) ≢ 0; */
+ uz = (unsigned int)1 / (0xffffffff + (unsigned int)1);
+ ux = 0x80000000;
+ uy = 0xffffffff;
+ /*@ assert rte: signed_downcast: ux ≤ 2147483647; */
+ /*@ assert rte: signed_downcast: uy ≤ 2147483647; */
+ /*@ assert rte: division_by_zero: (int)uy ≢ 0; */
+ /*@ assert rte: signed_overflow: (int)ux / (int)uy ≤ 2147483647; */
+ uz = (unsigned int)((int)ux / (int)uy);
+ /*@ assert rte: division_by_zero: uy ≢ 0; */
+ uz = ux / uy;
+ /*@ assert rte: division_by_zero: (unsigned int)(0xffffffff + 1) ≢ 0; */
+ uz = 0x80000000 / (0xffffffff + (unsigned int)1);
+ /*@ assert
+ rte: signed_overflow:
+ (int)((int)(-0x7fffffff) - 1) / (int)(-1) ≤ 2147483647;
+ */
+ uz = (unsigned int)((-0x7fffffff - 1) / -1);
+ uz = (unsigned int)(-0x7fffffff - 1) / 0xffffffff;
+ uz = 0x80000000 / (unsigned int)(-1);
+ uz = (unsigned int)((int)(0x80000000 / 0xffffffff));
+ /*@ assert rte: signed_overflow: -2147483648 ≤ x + y; */
+ /*@ assert rte: signed_overflow: x + y ≤ 2147483647; */
+ /*@ assert rte: division_by_zero: (int)(x + y) ≢ 0; */
+ z = 1 / (x + y);
+ /*@ assert rte: signed_overflow: x / (int)(-1) ≤ 2147483647; */
+ z = x / -1;
+ /*@ assert rte: division_by_zero: y ≢ 0; */
+ z = (-0x7ffffff - 1) / y;
+ /*@ assert
+ rte: signed_downcast:
+ (long long)((long long)(-2147483648L) / (long long)((long)(-1L))) ≤
+ 2147483647;
+ */
+ z = (int)(-2147483648L / (long long)(-1L));
+ z = (int)(0x80000000 / (unsigned int)(-1));
+ z = (int)(0x80000000 / 0xffffffff);
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/rte/oracle/divmod_typedef.res.oracle b/tests/rte/oracle/divmod_typedef.res.oracle
index 38a4968f0d0fb7a9ac4449772a898e939895b9d3..9d2cba27982e54d9bfb1bba23de7f6ac5179cd1d 100644
--- a/tests/rte/oracle/divmod_typedef.res.oracle
+++ b/tests/rte/oracle/divmod_typedef.res.oracle
@@ -1,8 +1,86 @@
[kernel] Parsing divmod_typedef.c (with preprocessing)
-[kernel] User Error: failed to run: gcc -E -C -I. -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 -o '/tmp/divmod_typedef.c87a25d.i' '/home/bobot/Sources/frama-c/_build/default/result/divmod_typedef.c'
- this is possibly due to missing preprocessor flags;
- consider options -cpp-extra-args, -json-compilation-database or -cpp-command.
- See chapter "Preparing the Sources" in the Frama-C user manual for more details.
-[kernel] User Error: stopping on file "divmod_typedef.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[rte] annotating function main
+[rte] divmod_typedef.c:15: Warning:
+ guaranteed RTE:
+ assert
+ signed_overflow: (int)((int)(-2147483647) - 1) / (int)(-1) ≤ 2147483647;
+[rte] divmod_typedef.c:18: Warning:
+ guaranteed RTE: assert division_by_zero: 0 ≢ 0;
+[rte] divmod_typedef.c:19: Warning:
+ guaranteed RTE:
+ assert division_by_zero: (unsigned int)(0xffffffff + 1) ≢ 0;
+[rte] divmod_typedef.c:26: Warning:
+ guaranteed RTE:
+ assert division_by_zero: (unsigned int)(0xffffffff + 1) ≢ 0;
+[rte] divmod_typedef.c:27: Warning:
+ guaranteed RTE:
+ assert
+ signed_overflow: (int)((int)(-0x7fffffff) - 1) / (int)(-1) ≤ 2147483647;
+[rte] divmod_typedef.c:38: Warning:
+ guaranteed RTE:
+ assert
+ signed_downcast:
+ (long long)((long long)(-2147483648L) / (long long)((long)(-1L))) ≤
+ 2147483647;
+/* Generated by Frama-C */
+typedef int tint;
+typedef unsigned int tuint;
+int main(void)
+{
+ int __retres;
+ tint x = 0;
+ tint y = 0;
+ tint z = 0;
+ tuint ux = (unsigned int)0;
+ tuint uy = (unsigned int)0;
+ tuint uz = (unsigned int)0;
+ /*@ assert
+ rte: signed_overflow:
+ (int)((int)(-2147483647) - 1) / (int)(-1) ≤ 2147483647;
+ */
+ z = (-2147483647 - 1) / -1;
+ z = (-2147483647 - 1) % -1;
+ /*@ assert rte: division_by_zero: 0 ≢ 0; */
+ uz = (unsigned int)(1 / 0);
+ /*@ assert rte: division_by_zero: (unsigned int)(0xffffffff + 1) ≢ 0; */
+ uz = (unsigned int)1 / (0xffffffff + (unsigned int)1);
+ ux = 0x80000000;
+ uy = 0xffffffff;
+ /*@ assert rte: signed_downcast: ux ≤ 2147483647; */
+ /*@ assert rte: signed_downcast: uy ≤ 2147483647; */
+ /*@ assert rte: division_by_zero: (int)uy ≢ 0; */
+ /*@ assert rte: signed_overflow: (int)ux / (int)uy ≤ 2147483647; */
+ uz = (unsigned int)((int)ux / (int)uy);
+ /*@ assert rte: division_by_zero: uy ≢ 0; */
+ uz = ux / uy;
+ /*@ assert rte: division_by_zero: (unsigned int)(0xffffffff + 1) ≢ 0; */
+ uz = 0x80000000 / (0xffffffff + (unsigned int)1);
+ /*@ assert
+ rte: signed_overflow:
+ (int)((int)(-0x7fffffff) - 1) / (int)(-1) ≤ 2147483647;
+ */
+ uz = (unsigned int)((-0x7fffffff - 1) / -1);
+ uz = (unsigned int)(-0x7fffffff - 1) / 0xffffffff;
+ uz = 0x80000000 / (unsigned int)(-1);
+ uz = (unsigned int)((int)(0x80000000 / 0xffffffff));
+ /*@ assert rte: signed_overflow: -2147483648 ≤ x + y; */
+ /*@ assert rte: signed_overflow: x + y ≤ 2147483647; */
+ /*@ assert rte: division_by_zero: (tint)(x + y) ≢ 0; */
+ z = 1 / (x + y);
+ /*@ assert rte: signed_overflow: x / (int)(-1) ≤ 2147483647; */
+ z = x / -1;
+ /*@ assert rte: division_by_zero: y ≢ 0; */
+ z = (-0x7ffffff - 1) / y;
+ /*@ assert
+ rte: signed_downcast:
+ (long long)((long long)(-2147483648L) / (long long)((long)(-1L))) ≤
+ 2147483647;
+ */
+ z = (int)(-2147483648L / (long long)(-1L));
+ z = (int)(0x80000000 / (unsigned int)(-1));
+ z = (int)(0x80000000 / 0xffffffff);
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/rte/oracle/value_rte.res.oracle b/tests/rte/oracle/value_rte.res.oracle
index 42555aba8861cdc3c1a853cf702e86523c52ed77..bc6feb4107471e96aa1e0e13d5433d6782796ca0 100644
--- a/tests/rte/oracle/value_rte.res.oracle
+++ b/tests/rte/oracle/value_rte.res.oracle
@@ -6,30 +6,30 @@
[eva:initial-state] Values of globals at initialization
[eva] computing for function getchar <- main.
- Called from value_rte.c:12.
+ Called from value_rte.c:13.
[eva] using specification for function getchar
[eva] Done for function getchar
-[eva] value_rte.c:13: assertion 'rte,index_bound' got status valid.
-[eva] value_rte.c:15: assertion 'rte,signed_overflow' got status valid.
-[eva] value_rte.c:11: starting to merge loop iterations
+[eva] value_rte.c:14: assertion 'rte,index_bound' got status valid.
+[eva] value_rte.c:16: assertion 'rte,signed_overflow' got status valid.
+[eva] value_rte.c:12: starting to merge loop iterations
[eva] computing for function getchar <- main.
- Called from value_rte.c:12.
+ Called from value_rte.c:13.
[eva] Done for function getchar
[eva] computing for function getchar <- main.
- Called from value_rte.c:12.
+ Called from value_rte.c:13.
[eva] Done for function getchar
[eva] computing for function getchar <- main.
- Called from value_rte.c:12.
+ Called from value_rte.c:13.
[eva] Done for function getchar
[eva] computing for function getchar <- main.
- Called from value_rte.c:12.
+ Called from value_rte.c:13.
[eva] Done for function getchar
-[eva:alarm] value_rte.c:13: Warning:
+[eva:alarm] value_rte.c:14: Warning:
assertion 'rte,index_bound' got status unknown.
[eva] Recording results for main
[eva] done for function main
-[eva] value_rte.c:13: assertion 'rte,index_bound' got final status valid.
-[eva] value_rte.c:15: assertion 'rte,signed_overflow' got final status valid.
+[eva] value_rte.c:14: assertion 'rte,index_bound' got final status valid.
+[eva] value_rte.c:16: assertion 'rte,signed_overflow' got final status valid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
t[0] ∈ {1}
@@ -882,11 +882,11 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ Valid ] Assertion 'rte,index_bound' (file value_rte.c, line 13)
+[ Valid ] Assertion 'rte,index_bound' (file value_rte.c, line 14)
by Eva.
-[ - ] Assertion 'rte,index_bound' (file value_rte.c, line 13)
+[ - ] Assertion 'rte,index_bound' (file value_rte.c, line 14)
tried with Eva.
-[ Valid ] Assertion 'rte,signed_overflow' (file value_rte.c, line 15)
+[ Valid ] Assertion 'rte,signed_overflow' (file value_rte.c, line 16)
by Eva.
--------------------------------------------------------------------------------
diff --git a/tests/rte/twofunc3.c b/tests/rte/twofunc3.c
index dd0b7781dcc65212a9867b12e60b94ac36bdcb54..df7ec688f80a7eea3d71c6176f2b61ad8aa639b5 100644
--- a/tests/rte/twofunc3.c
+++ b/tests/rte/twofunc3.c
@@ -1,6 +1,6 @@
/* run.config
- CMXS: rte_get_annot
- OPT: -rte-select @@all -load-module %{dep:rte_get_annot} -journal-disable
+ MODULE: rte_get_annot.cmxs
+ OPT: -rte-select @@all -journal-disable
*/
diff --git a/tests/rte/value_rte.c b/tests/rte/value_rte.c
index 0587fca439d1864503ee51cac0cbafb41e217127..f5fe77aaf8792c620f7ed6fcaae9eba82d7bda87 100644
--- a/tests/rte/value_rte.c
+++ b/tests/rte/value_rte.c
@@ -1,4 +1,5 @@
/* run.config
+PLUGIN: report
OPT: -rte -then -eva @EVA_OPTIONS@ -then -report
*/
diff --git a/tests/slicing/adpcm.c b/tests/slicing/adpcm.c
index 83dedf9a0f09d66956e102db0d21fa850668f0b6..7b3717a1f7d27364ec3f8b666634358bb52ca57a 100644
--- a/tests/slicing/adpcm.c
+++ b/tests/slicing/adpcm.c
@@ -1,5 +1,5 @@
/* run.config
- DEPS: ../test/adpcm.c
+ DEPS: ../../test/adpcm.c
STDOPT: +"-add-symbolic-path TESTS_DIR:../.. -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs} -ulevel -1 -deps -slicing-level 2 -journal-disable"
*/
diff --git a/tests/slicing/variadic.c b/tests/slicing/variadic.c
index 4629542db44e021920215bdaa6000a1a479e6bd5..440eff0a6cebfe57b5f5a53c5bcc0bb00048bdf3 100644
--- a/tests/slicing/variadic.c
+++ b/tests/slicing/variadic.c
@@ -1,5 +1,5 @@
/* run.config
- DEPS: ../pdg/variadic.c
+ DEPS: ../../pdg/variadic.c
STDOPT: +"-slice-return f3 -no-slice-callers -journal-disable -then-on 'Slicing export' -print"
STDOPT: +"-slice-return f3 -no-slice-callers -journal-disable -variadic-no-translation -then-last -print"
STDOPT: +"-slice-return f3 -journal-disable -then-on 'Slicing export' -print"