Skip to content
Snippets Groups Projects
Commit ea074b22 authored by François Bobot's avatar François Bobot
Browse files

tests for tests/rte pass

parent 9841fb95
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 191 additions and 37 deletions
tests/libc/coverage.c
+ 1
− 1
View file @ ea074b22
/* 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
*/
......
tests/libc/runtime.c
+ 1
− 1
View file @ ea074b22
/* 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:
*/
......
tests/libc/string_c_generic.c
+ 1
− 1
View file @ ea074b22
/* 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
......
tests/libc/string_c_strchr.c
+ 1
− 1
View file @ ea074b22
/* 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
......
tests/libc/string_c_strstr.c
+ 1
− 1
View file @ ea074b22
/* 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
......
tests/rte/oracle/divmod.res.oracle
+ 82
− 7
View file @ ea074b22
[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;
}
tests/rte/oracle/divmod_typedef.res.oracle
+ 85
− 7
View file @ ea074b22
[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;
}
tests/rte/oracle/value_rte.res.oracle
+ 14
− 14
View file @ ea074b22
......@@ -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.
--------------------------------------------------------------------------------
......
tests/rte/twofunc3.c
+ 2
− 2
View file @ ea074b22
/* 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
*/
......
tests/rte/value_rte.c
+ 1
− 0
View file @ ea074b22
/* run.config
PLUGIN: report
OPT: -rte -then -eva @EVA_OPTIONS@ -then -report
*/
......
tests/slicing/adpcm.c
+ 1
− 1
View file @ ea074b22
/* 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"
*/
......
tests/slicing/variadic.c
+ 1
− 1
View file @ ea074b22
/* 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"
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment