diff --git a/Makefile b/Makefile index f52c261596d3ce5cf8f9afcef6fbc5046fa7058f..0dd9b6b7e0efe2a068038f5e0a9239a9b19e48f2 100644 --- a/Makefile +++ b/Makefile @@ -170,10 +170,10 @@ force-reconfigure: # todo: adds bugs? # todo: adds crowbar? -# todo: adds dynamic_plugin? -# todo: adds fc_script +# todo: adds dynamic_plugin? No, will be removed from master branch. +# todo: adds fc_script (waiting for a fix in scripts of share/analysis-scripts/) # todo: adds make_run_script -# todo: adds more_wp +# todo: adds more_wp? # todo: adds value/numerors? (requires opam package mlgmpidl and system libraries for MPFR) # todo: adds verisec # todo: adds configuration tests related to tests/test_config_apron (and tests/test_config_...) done by the scripts src/plugins/value/vtests and script src/plugins/value/utests. diff --git a/src/plugins/dive/tests/test_config b/src/plugins/dive/tests/test_config index 4d5ede90091775c9f0c2f8f2f869ba3efaf365b5..dee21c98d9efbf3e40eb7ff1138d123babd2db27 100644 --- a/src/plugins/dive/tests/test_config +++ b/src/plugins/dive/tests/test_config @@ -1,5 +1,6 @@ -# Just one test by C file since @PTEST_NUMBER@ is not used into the LOG name. +COMMENT: Just one test by C file since @PTEST_NUMBER@ is not used into the LOG name. + LOG: @PTEST_NAME@.dot PLUGIN: from inout eva variadic scope dive -OPT: -check -eva-msg-key=-initial-state -eva-no-show-progress -dive-output-dot @PTEST_NAME@ +OPT: -journal-disable -eva-msg-key=-initial-state -eva-no-show-progress -dive-output-dot @PTEST_NAME@ FILTER: perl -0777 -pe 's/\[server[^[]*//g' diff --git a/src/plugins/loop_analysis/tests/test_config b/src/plugins/loop_analysis/tests/test_config index 38f5a9cf0d342a8db00e3909b0f2c227e8a808e7..cd1e6af6a75d8886c49b7a0cbb9c36d6d24b54f7 100644 --- a/src/plugins/loop_analysis/tests/test_config +++ b/src/plugins/loop_analysis/tests/test_config @@ -1,2 +1,2 @@ PLUGIN: loop-analysis -OPT: -loop +OPT: -loop -journal-disable diff --git a/src/plugins/nonterm/tests/test_config b/src/plugins/nonterm/tests/test_config index ec3e523ed36de606b7f4cfb55811bced5d02d609..3638b0a7f39432a1392e45cd3f8137aa6574ea9f 100644 --- a/src/plugins/nonterm/tests/test_config +++ b/src/plugins/nonterm/tests/test_config @@ -1,2 +1,2 @@ PLUGIN: from inout nonterm scope -OPT: -eva -eva-show-progress -eva-msg-key=-summary -then -nonterm -nonterm-verbose 2 +OPT: -journal-disable -eva -eva-show-progress -eva-msg-key=-summary -then -nonterm -nonterm-verbose 2 diff --git a/src/plugins/variadic/tests/test_config b/src/plugins/variadic/tests/test_config index 3a9dd329444670bb5233806a1741d750826da077..95aa532c634ca4a5d612cc5e2127a973ddd7788d 100644 --- a/src/plugins/variadic/tests/test_config +++ b/src/plugins/variadic/tests/test_config @@ -1,2 +1,2 @@ PLUGIN: from inout eva variadic scope -OPT: -check -print -kernel-verbose 0 -variadic-verbose 2 -eva -eva-slevel 10 -eva-msg-key=-initial-state,-summary -eva-no-show-progress -eva-print +OPT: -journal-disable -print -kernel-verbose 0 -variadic-verbose 2 -eva -eva-slevel 10 -eva-msg-key=-initial-state,-summary -eva-no-show-progress -eva-print diff --git a/tests/cil/test_config b/tests/cil/test_config index 99501d0f39bd6707cddef97f0c4eecaa5a1a21b6..318c68106133c75b7dbc34882d2548434145e1ef 100644 --- a/tests/cil/test_config +++ b/tests/cil/test_config @@ -1,2 +1,7 @@ +COMMENT: by default, no analysis is performed (since the PLUGIN directive +COMMENT: is empty). +COMMENT: to perform value analyses, the macro @EVA_CONFIG@ (resp. @EVA_OPTIONS@) +COMMENT: can be used into PLUGIN (resp. OPT) directives of specific test files. + PLUGIN: -OPT:-print +OPT: -print -journal-disable diff --git a/tests/libc/test_config b/tests/libc/test_config index fca40f274632be2a48598c781597677a7db02415..237f9df534a80de16aa7bb575c3d9dfcdaf5b2ae 100644 --- a/tests/libc/test_config +++ b/tests/libc/test_config @@ -1 +1 @@ -OPT: -eva @EVA_OPTIONS@ -cpp-extra-args='-nostdinc -Ishare/libc' +OPT: -journal-disable -eva @EVA_OPTIONS@ -cpp-extra-args='-nostdinc -Ishare/libc' diff --git a/tests/pretty_printing/test_config b/tests/pretty_printing/test_config index f82579be4ece4a49ff9c6542ec8d824f4b8f955c..9aa89de68a1640d3e1de517da695c1b6a6afdfbb 100644 --- a/tests/pretty_printing/test_config +++ b/tests/pretty_printing/test_config @@ -1,5 +1,10 @@ -COMMENT: this directory is meant to test the parser and pretty-printer +COMMENT: this directory is meant to test the parser and pretty-printer. COMMENT: the default option checks that pretty-printed code can be merged -COMMENT: with the original one +COMMENT: with the original one. +COMMENT: by default, no analysis is performed (since the PLUGIN directive +COMMENT: is empty). +COMMENT: to perform value analyses, the macro @EVA_CONFIG@ (resp. @EVA_OPTIONS@) +COMMENT: can be used into PLUGIN (resp. OPT) directives of specific test files. + PLUGIN: OPT: -print -journal-disable -check -then -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -print -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print diff --git a/tests/slicing/test_config b/tests/slicing/test_config index fff12f16b671297f812a8f6701b214a3e45ed9b8..4ca5fca8bac218ebd7240d0fd78c85478ff9c118 100644 --- a/tests/slicing/test_config +++ b/tests/slicing/test_config @@ -1,2 +1,2 @@ PLUGIN: slicing @EVA_CONFIG@ -OPT: @EVA_OPTIONS@ +OPT: @EVA_OPTIONS@ -journal-disable diff --git a/tests/spec/test_config b/tests/spec/test_config index f43a4694237743d39446812134ab8f4c79856562..2be9336fce9bcd3207a20142023734b9654c4436 100644 --- a/tests/spec/test_config +++ b/tests/spec/test_config @@ -1,6 +1,10 @@ -COMMENT: for now, this directory mainly tests the annotations syntax, -COMMENT: no analysis is performed. +COMMENT: for now, this directory mainly tests the annotations syntax. COMMENT: we continue on annotation errors, as this allows to put COMMENT: various variations of the same test in one file. +COMMENT: by default, no analysis is performed (since the PLUGIN directive +COMMENT: is empty). +COMMENT: to perform value analyses, the macro @EVA_CONFIG@ (resp. @EVA_OPTIONS@) +COMMENT: can be used into PLUGIN (resp. OPT) directives of specific test files. + PLUGIN: OPT: -pp-annot -print -journal-disable -kernel-warn-key=annot-error=active -check diff --git a/tests/syntax/test_config b/tests/syntax/test_config index fbf4ede9f20c11bee95558bbf61bd84cc14c3ab3..3b0f1d682c5fec48b6a5a24903d0098e308b47a7 100644 --- a/tests/syntax/test_config +++ b/tests/syntax/test_config @@ -1,5 +1,10 @@ COMMENT: this directory is meant to test exclusively the front-end -COMMENT: (parser, type-checker, linker, syntactic transformations) +COMMENT: (parser, type-checker, linker, syntactic transformations). +COMMENT: by default, no analysis is performed since only the varadic plugin is +COMMENT: used. +COMMENT: to perform value analyses, the macro @EVA_CONFIG@ (resp. @EVA_OPTIONS@) +COMMENT: can be used into PLUGIN (resp. OPT) directives of specific test files. + PLUGIN: variadic OPT: -print -journal-disable -check FILEREG:.*\.\(c\|i\|ci\)$ diff --git a/tests/test_config b/tests/test_config index 5a534c7ec2d54b5f4f53205bcf34226bf35bc316..7eb046c8688aa0daddf75117186eb761c08b393b 100644 --- a/tests/test_config +++ b/tests/test_config @@ -1,3 +1,9 @@ +COMMENT: macros @EVA_CONFIG@ (resp. @EVA_OPTIONS@) are usables in test files +COMMENT: redefining the PLUGIN (resp. OPT) directives. +COMMENT: the PLUGIN directive sets automatically the @PLUGIN@ macro that can be +COMMENT: used into others PLUGIN directives in order to extend the parent list +COMMENT: of used plug'ins. + MACRO: EVA_CONFIG from inout eva scope variadic MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 PLUGIN: @EVA_CONFIG@