diff --git a/src/plugins/e-acsl/tests/bts/bts1395.i b/src/plugins/e-acsl/tests/bts/bts1395.i index a6086e8542ab21e6c435d6997a048fbfd0d81947..6b82653a96baf7ce2a68119d105cc35fce8a6232 100644 --- a/src/plugins/e-acsl/tests/bts/bts1395.i +++ b/src/plugins/e-acsl/tests/bts/bts1395.i @@ -1,5 +1,6 @@ /* run.config COMMENT: recursive function + STDOPT: +"-eva-ignore-recursive-calls" */ /*@ requires n > 0; */ diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle index 99ac6de8e2a918c54a2628fc247e7c42a7934020..ea1cf8d1c6a78f3d1b0e3848de85ba662f87849f 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle @@ -1,11 +1,15 @@ [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". -[eva] tests/bts/bts1395.i:8: Warning: - detected recursive call - (__gen_e_acsl_fact <- fact :: tests/bts/bts1395.i:6 <- - __gen_e_acsl_fact :: tests/bts/bts1395.i:12 <- - main) - Use -eva-ignore-recursive-calls to ignore (beware this will make the analysis - unsound) -[eva] User Error: Degeneration occurred: - results are not correct for lines of code that can be reached from the degeneration point. +[eva] tests/bts/bts1395.i:9: Warning: + recursive call during value analysis + of __gen_e_acsl_fact (__gen_e_acsl_fact <- fact :: tests/bts/bts1395.i:7 <- + __gen_e_acsl_fact :: tests/bts/bts1395.i:13 <- + main). + Assuming the call has no effect. The analysis will be unsound. +[eva:alarm] tests/bts/bts1395.i:9: Warning: + signed overflow. assert -2147483648 ≤ n * tmp; + (tmp from fact(n - 1)) +[eva:alarm] tests/bts/bts1395.i:9: Warning: + signed overflow. assert n * tmp ≤ 2147483647; + (tmp from fact(n - 1)) +[eva:alarm] tests/bts/bts1395.i:14: Warning: assertion got status unknown. diff --git a/src/plugins/e-acsl/tests/bts/test_config b/src/plugins/e-acsl/tests/bts/test_config index d7b9c838f9f57438ff7a30b9e82a1d130d7331c9..1fb42e2f9122687547c8d809923862b7e1f27918 100644 --- a/src/plugins/e-acsl/tests/bts/test_config +++ b/src/plugins/e-acsl/tests/bts/test_config @@ -1,3 +1,3 @@ LOG: gen_@PTEST_NAME@.c -OPT: -variadic-no-translation -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 -value-verbose 0 +OPT: -variadic-no-translation -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 -eva -eva-verbose 0 EXEC: ./scripts/testrun.sh @PTEST_NAME@ bts "" "--frama-c=@frama-c@" diff --git a/src/plugins/e-acsl/tests/builtin/test_config b/src/plugins/e-acsl/tests/builtin/test_config index 0a3bc2dc49d91fddd1d4df4fdeb25322a44f35d4..d10e3bc47b50cdf874070f3aae25f19ec3d4f193 100644 --- a/src/plugins/e-acsl/tests/builtin/test_config +++ b/src/plugins/e-acsl/tests/builtin/test_config @@ -1,3 +1,3 @@ LOG: gen_@PTEST_NAME@.c -OPT: -variadic-no-translation -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -e-acsl-replace-libc-functions -then-last -load-script tests/print.cmxs -print -ocode tests/builtin/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results +OPT: -variadic-no-translation -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -e-acsl-replace-libc-functions -then-last -load-script tests/print.cmxs -print -ocode tests/builtin/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-no-print -eva-no-show-progress -no-results EXEC: ./scripts/testrun.sh @PTEST_NAME@ builtin "1" "--frama-c=@frama-c@ --full-mmodel --libc-replacements" diff --git a/src/plugins/e-acsl/tests/format/test_config b/src/plugins/e-acsl/tests/format/test_config index 8f2dae04629c15ccc3f26ad5f4a285bd5f9da370..c42ada82ec5049e1fd36b6512a9927bda04b5e6d 100644 --- a/src/plugins/e-acsl/tests/format/test_config +++ b/src/plugins/e-acsl/tests/format/test_config @@ -1,3 +1,3 @@ LOG: gen_@PTEST_NAME@.c -OPT: -variadic-no-translation -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -e-acsl-validate-format-strings -kernel-warn-key=-annot:missing-spec -then-last -load-script tests/print.cmxs -print -ocode tests/format/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results +OPT: -variadic-no-translation -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -e-acsl-validate-format-strings -kernel-warn-key=annot:missing-spec=inactive -then-last -load-script tests/print.cmxs -print -ocode tests/format/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-no-print -eva-no-show-progress -no-results EXEC: ./scripts/testrun.sh @PTEST_NAME@ format "1" "--frama-c=@frama-c@ --full-mmodel --validate-format-strings" diff --git a/src/plugins/e-acsl/tests/full-mmodel-only/test_config b/src/plugins/e-acsl/tests/full-mmodel-only/test_config index d5f839c452f0928bfe740dc4ce24986477ea8aaa..3920419f522cbbef78959b01ef1aa339ba9acfd9 100644 --- a/src/plugins/e-acsl/tests/full-mmodel-only/test_config +++ b/src/plugins/e-acsl/tests/full-mmodel-only/test_config @@ -1,3 +1,3 @@ EXEC: ./scripts/testrun.sh @PTEST_NAME@ full-mmodel-only "1" "--frama-c=@frama-c@ --full-mmodel" LOG: gen_@PTEST_NAME@.c -OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel-only/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results \ No newline at end of file +OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel-only/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-no-print -eva-no-show-progress -no-results diff --git a/src/plugins/e-acsl/tests/full-mmodel/test_config b/src/plugins/e-acsl/tests/full-mmodel/test_config index 31e1db413b162735af5c2fb71d6bc3315d84694b..dfe9f67a0781cff9d6beaf7aa0f2a625d473b62c 100644 --- a/src/plugins/e-acsl/tests/full-mmodel/test_config +++ b/src/plugins/e-acsl/tests/full-mmodel/test_config @@ -1,5 +1,5 @@ LOG: gen_@PTEST_NAME@.c -OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results +OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-no-print -eva-no-show-progress -no-results EXEC: ./scripts/testrun.sh @PTEST_NAME@ full-mmodel "1" "--frama-c=@frama-c@ --full-mmodel" LOG: gen_@PTEST_NAME@2.c -OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results +OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -eva -eva-no-print -eva-no-show-progress -no-results diff --git a/src/plugins/e-acsl/tests/gmp/longlong.i b/src/plugins/e-acsl/tests/gmp/longlong.i index bdaa2c9cf1716c418b8306ee8834ae832a3ca411..e013c42e76bbfafbd10611ddfa80ab90567ba575 100644 --- a/src/plugins/e-acsl/tests/gmp/longlong.i +++ b/src/plugins/e-acsl/tests/gmp/longlong.i @@ -1,6 +1,6 @@ /* run.config COMMENT: upgrading longlong to GMP - STDOPT: +"-val-ignore-recursive-calls" + STDOPT: +"-eva-ignore-recursive-calls" */ unsigned long long my_pow(unsigned int x, unsigned int n) { diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle index ad18eafd7c5a677b688c1f0e607af85bf88332ba..5b07e0a1fffa404bdfca5158b6fe3344d7a65cf8 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle @@ -10,10 +10,10 @@ __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38] __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308] [eva] using specification for function __e_acsl_memory_init -[eva] tests/gmp/longlong.i:9: User Error: +[eva] tests/gmp/longlong.i:9: Warning: recursive call during value analysis of my_pow (my_pow <- my_pow :: tests/gmp/longlong.i:16 <- main). Assuming - the call has no effect. The analysis will be unsound.] + the call has no effect. The analysis will be unsound. [eva] using specification for function my_pow [eva:alarm] tests/gmp/longlong.i:10: Warning: signed overflow. assert -2147483648 ≤ tmp * tmp; diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle index cf169024abf641ceb0edc8954ca2ccf67075a182..fada6aef03dec76e67853cb0de19edc20b19ea42 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle @@ -10,10 +10,10 @@ __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38] __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308] [eva] using specification for function __e_acsl_memory_init -[eva] tests/gmp/longlong.i:9: User Error: +[eva] tests/gmp/longlong.i:9: Warning: recursive call during value analysis of my_pow (my_pow <- my_pow :: tests/gmp/longlong.i:16 <- main). Assuming - the call has no effect. The analysis will be unsound.] + the call has no effect. The analysis will be unsound. [eva] using specification for function my_pow [eva:alarm] tests/gmp/longlong.i:10: Warning: signed overflow. assert -2147483648 ≤ tmp * tmp; diff --git a/src/plugins/e-acsl/tests/gmp/test_config b/src/plugins/e-acsl/tests/gmp/test_config index 645d2c1fa60b62e4c9c9223a7c2f6adf06608878..5b2172b01dd85c9a5396c0c0a7c9dda207624be7 100644 --- a/src/plugins/e-acsl/tests/gmp/test_config +++ b/src/plugins/e-acsl/tests/gmp/test_config @@ -1,5 +1,5 @@ LOG: gen_@PTEST_NAME@.c -OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results -eva-no-alloc-returns-null +OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-no-print -eva-no-show-progress -no-results -eva-no-alloc-returns-null EXEC: ./scripts/testrun.sh @PTEST_NAME@ gmp "1" "--frama-c=@frama-c@" LOG: gen_@PTEST_NAME@2.c -OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results -eva-no-alloc-returns-null +OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -eva -eva-no-print -eva-no-show-progress -no-results -eva-no-alloc-returns-null diff --git a/src/plugins/e-acsl/tests/runtime/test_config b/src/plugins/e-acsl/tests/runtime/test_config index b1256ec5a21ced560249ef7f189c19eded8a9cd9..3d07f7500426e9ee476265cd446000213411b753 100644 --- a/src/plugins/e-acsl/tests/runtime/test_config +++ b/src/plugins/e-acsl/tests/runtime/test_config @@ -1,3 +1,3 @@ LOG: gen_@PTEST_NAME@.c -OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/runtime/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -value-verbose 0 +OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/runtime/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-verbose 0 EXEC: ./scripts/testrun.sh @PTEST_NAME@ runtime "" "--frama-c=@frama-c@" diff --git a/src/plugins/e-acsl/tests/temporal/t_getenv.c b/src/plugins/e-acsl/tests/temporal/t_getenv.c index 259c1b18ddc9366f0acc79ee70a17fc083ecd1cf..41dfd4549960304c699ced96bd27705370152c42 100644 --- a/src/plugins/e-acsl/tests/temporal/t_getenv.c +++ b/src/plugins/e-acsl/tests/temporal/t_getenv.c @@ -1,6 +1,6 @@ /* run.config COMMENT: Check temporal validity of environment string (via getenv function) - STDOPT: #"-eva-warn-key=-libc:unsupported-spec" + STDOPT: #"-eva-warn-key=libc:unsupported-spec=inactive" */ #include <stdlib.h> #include <errno.h> diff --git a/src/plugins/e-acsl/tests/temporal/test_config b/src/plugins/e-acsl/tests/temporal/test_config index 395b62c1735233dabdaae9fc612ea550b487d138..c9b7be37341c6f4e52281f3278a85b2d23b4e225 100644 --- a/src/plugins/e-acsl/tests/temporal/test_config +++ b/src/plugins/e-acsl/tests/temporal/test_config @@ -1,3 +1,3 @@ LOG: gen_@PTEST_NAME@.c -OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-temporal-validity -then-last -load-script tests/print.cmxs -print -ocode tests/temporal/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -value-verbose 0 -value-warn-key="-alarm" +OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-temporal-validity -then-last -load-script tests/print.cmxs -print -ocode tests/temporal/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -value-verbose 0 -eva-warn-key="alarm=inactive" EXEC: ./scripts/testrun.sh @PTEST_NAME@ temporal "" "--frama-c=@frama-c@ --full-mmodel --temporal"