From ea074b22f1dfe172a52256e3fe42c0e3d2f5d40b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 3 Sep 2020 17:33:34 +0200
Subject: [PATCH] tests for tests/rte pass
---
tests/libc/coverage.c | 2 +-
tests/libc/runtime.c | 2 +-
tests/libc/string_c_generic.c | 2 +-
tests/libc/string_c_strchr.c | 2 +-
tests/libc/string_c_strstr.c | 2 +-
tests/rte/oracle/divmod.res.oracle | 89 +++++++++++++++++++--
tests/rte/oracle/divmod_typedef.res.oracle | 92 ++++++++++++++++++++--
tests/rte/oracle/value_rte.res.oracle | 28 +++----
tests/rte/twofunc3.c | 4 +-
tests/rte/value_rte.c | 1 +
tests/slicing/adpcm.c | 2 +-
tests/slicing/variadic.c | 2 +-
12 files changed, 191 insertions(+), 37 deletions(-)
diff --git a/tests/libc/coverage.c b/tests/libc/coverage.c
index 8c2b1421bfd..42f6476d300 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 37647e76af9..a245abd3365 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 d960a9b44fc..57c5461faa5 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 4179b4f27cb..79ee7bebace 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 2bfbbdbe125..e7f30e82d08 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 d4b45c78263..f7f9626762a 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 38a4968f0d0..9d2cba27982 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 42555aba886..bc6feb41074 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 dd0b7781dcc..df7ec688f80 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 0587fca439d..f5fe77aaf87 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 83dedf9a0f0..7b3717a1f7d 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 4629542db44..440eff0a6ce 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"
--
GitLab