Merge branch 'feature/virgile/warn-key-unique-opt' into 'master'

synchronisation with frama-c!2038

See merge request frama-c/e-acsl!253

src/plugins/e-acsl/tests/bts/bts1395.i

 /* run.config
    COMMENT: recursive function
+   STDOPT: +"-eva-ignore-recursive-calls"
 */
 
 /*@ requires n > 0; */

src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle

 [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.

src/plugins/e-acsl/tests/bts/test_config

 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@"

src/plugins/e-acsl/tests/builtin/test_config

 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"

src/plugins/e-acsl/tests/format/test_config

 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"

src/plugins/e-acsl/tests/full-mmodel-only/test_config

 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
+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
\ No newline at end of file

src/plugins/e-acsl/tests/full-mmodel/test_config

 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

src/plugins/e-acsl/tests/gmp/longlong.i

 /* 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) {

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;

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;

src/plugins/e-acsl/tests/gmp/test_config

 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

src/plugins/e-acsl/tests/runtime/test_config

 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@"

src/plugins/e-acsl/tests/temporal/t_getenv.c

 /* 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>

src/plugins/e-acsl/tests/temporal/test_config

 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"