Skip to content
Snippets Groups Projects
Commit ef2504ad authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[tests] update options against kernel changes

parent 3d97921d
No related branches found
No related tags found
No related merge requests found
LOG: gen_@PTEST_NAME@.c 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@" EXEC: ./scripts/testrun.sh @PTEST_NAME@ bts "" "--frama-c=@frama-c@"
LOG: gen_@PTEST_NAME@.c 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" EXEC: ./scripts/testrun.sh @PTEST_NAME@ builtin "1" "--frama-c=@frama-c@ --full-mmodel --libc-replacements"
LOG: gen_@PTEST_NAME@.c 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" EXEC: ./scripts/testrun.sh @PTEST_NAME@ format "1" "--frama-c=@frama-c@ --full-mmodel --validate-format-strings"
EXEC: ./scripts/testrun.sh @PTEST_NAME@ full-mmodel-only "1" "--frama-c=@frama-c@ --full-mmodel" EXEC: ./scripts/testrun.sh @PTEST_NAME@ full-mmodel-only "1" "--frama-c=@frama-c@ --full-mmodel"
LOG: gen_@PTEST_NAME@.c 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
LOG: gen_@PTEST_NAME@.c 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" EXEC: ./scripts/testrun.sh @PTEST_NAME@ full-mmodel "1" "--frama-c=@frama-c@ --full-mmodel"
LOG: gen_@PTEST_NAME@2.c 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
LOG: gen_@PTEST_NAME@.c 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@" EXEC: ./scripts/testrun.sh @PTEST_NAME@ gmp "1" "--frama-c=@frama-c@"
LOG: gen_@PTEST_NAME@2.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
LOG: gen_@PTEST_NAME@.c 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@" EXEC: ./scripts/testrun.sh @PTEST_NAME@ runtime "" "--frama-c=@frama-c@"
/* run.config /* run.config
COMMENT: Check temporal validity of environment string (via getenv function) 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 <stdlib.h>
#include <errno.h> #include <errno.h>
......
LOG: gen_@PTEST_NAME@.c 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" EXEC: ./scripts/testrun.sh @PTEST_NAME@ temporal "" "--frama-c=@frama-c@ --full-mmodel --temporal"
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment