From 6aff6e0710411443a8affee488627fca38e8538b Mon Sep 17 00:00:00 2001 From: Patrick Baudin <patrick.baudin@cea.fr> Date: Fri, 16 Oct 2020 10:48:02 +0200 Subject: [PATCH] [Tests] review of test_config files --- Makefile | 6 +++--- src/plugins/dive/tests/test_config | 5 +++-- src/plugins/loop_analysis/tests/test_config | 2 +- src/plugins/nonterm/tests/test_config | 2 +- src/plugins/variadic/tests/test_config | 2 +- tests/cil/test_config | 7 ++++++- tests/libc/test_config | 2 +- tests/pretty_printing/test_config | 9 +++++++-- tests/slicing/test_config | 2 +- tests/spec/test_config | 8 ++++++-- tests/syntax/test_config | 7 ++++++- tests/test_config | 6 ++++++ 12 files changed, 42 insertions(+), 16 deletions(-) diff --git a/Makefile b/Makefile index f52c261596d..0dd9b6b7e0e 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 4d5ede90091..dee21c98d9e 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 38f5a9cf0d3..cd1e6af6a75 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 ec3e523ed36..3638b0a7f39 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 3a9dd329444..95aa532c634 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 99501d0f39b..318c6810613 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 fca40f27463..237f9df534a 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 f82579be4ec..9aa89de68a1 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 fff12f16b67..4ca5fca8bac 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 f43a4694237..2be9336fce9 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 fbf4ede9f20..3b0f1d682c5 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 5a534c7ec2d..7eb046c8688 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@ -- GitLab