From 27dceadc0a77cc85e6f6f0ab6242ae4b5f58e307 Mon Sep 17 00:00:00 2001 From: Patrick Baudin <patrick.baudin@cea.fr> Date: Wed, 14 Oct 2020 18:42:44 +0200 Subject: [PATCH] [Ptests] adds PLUGIN macro and the PLUGIN directive sets the macro --- ptests/ptests.ml | 18 ++++++++++-------- src/plugins/report/tests/report/classify.c | 2 +- src/plugins/report/tests/report/csv.c | 2 +- src/plugins/report/tests/report/test_config | 2 +- tests/builtins/big_local_array.i | 2 +- tests/builtins/test_config | 2 +- tests/constant_propagation/bts117.c | 2 +- tests/constant_propagation/test_config | 2 +- tests/impact/test_config | 2 +- tests/journal/control2.c | 2 +- tests/journal/intra.i | 2 +- tests/libc/coverage.c | 2 +- tests/libc/fc_libc.c | 2 +- tests/metrics/test_config | 2 +- tests/misc/add_assigns.i | 2 +- tests/misc/bts1347.i | 2 +- tests/misc/obfuscate.c | 2 +- tests/occurrence/test_config | 2 +- tests/pdg/bts1194.c | 2 +- tests/pdg/test_config | 2 +- tests/pretty_printing/ghost_parameters.c | 4 ++-- tests/rte/test_config | 1 + tests/rte/value_rte.c | 2 +- tests/saveload/load_one.i | 2 +- tests/saveload/multi_project.i | 2 +- tests/saveload/sparecode.i | 2 +- tests/scope/zones.c | 2 +- tests/slicing/combine.i | 2 +- tests/slicing/test_config | 2 +- tests/sparecode/test_config | 2 +- tests/spec/generalized_check.i | 2 +- tests/test_config | 7 ++++--- tests/value/from_call.i | 6 +++--- tests/value/ilevel.i | 4 ++-- tests/value/redundant_alarms.c | 2 +- 35 files changed, 51 insertions(+), 47 deletions(-) create mode 100644 tests/rte/test_config diff --git a/ptests/ptests.ml b/ptests/ptests.ml index 69e74a117e2..79392ec7067 100644 --- a/ptests/ptests.ml +++ b/ptests/ptests.ml @@ -343,12 +343,12 @@ let test_path = Sys.chdir (Filename.dirname tests); "tests" +let split_blank s = Str.split (Str.regexp "[ ]+") s let parse_config_line = - let regexp_blank = Str.regexp "[ ]+" in fun (key, value) -> match key with | "DEFAULT_SUITES" -> - let l = Str.split regexp_blank value in + let l = split_blank value in default_suites := List.map (Filename.concat test_path) l | _ -> default_env key value (* Environnement variable that Frama-C reads*) @@ -546,7 +546,7 @@ type config = dc_timeout: string } -let default_macros () = Macros.empty +let default_macros () = Macros.add_list [ "PLUGIN", "" ] Macros.empty let default_config () = { dc_test_regexp = test_file_regexp ; @@ -641,14 +641,16 @@ let config_exec ~once dir s current = scan_execnow ~once dir current.dc_timeout s :: current.dc_execnow } let config_cmxs _dir s current = - let l = (String.split_on_char ' ' s) in + let l = split_blank s in { current with dc_cmxs = l @ current.dc_cmxs } let config_deps _dir s current = - { current with dc_deps = (String.split_on_char ' ' s) @ current.dc_deps } + { current with dc_deps = (split_blank s) @ current.dc_deps } let config_plugin _dir s current = - { current with dc_plugins = (String.split_on_char ' ' s) @ current.dc_plugins } + let s = Macros.expand current.dc_macros s in + { current with dc_plugins = split_blank s ; + dc_macros = Macros.add_list ["PLUGIN", s] current.dc_macros } let config_macro _dir s current = let regex = Str.regexp "[ \t]*\\([^ \t@]+\\)\\([ \t]+\\(.*\\)\\|$\\)" in @@ -772,7 +774,7 @@ let scan_options dir scan_buffer default = | [] when !r.dc_framac -> { !r with dc_toplevels = default.dc_toplevels } | l -> { !r with dc_toplevels = List.rev l }) -let split_config = Str.regexp ",[ ]*" +let split_config s = Str.split (Str.regexp ",[ ]*") s let is_config name = let prefix = "run.config" in @@ -797,7 +799,7 @@ let scan_test_file default dir f = name = "run.config" && !special_config = "" || name = "run.config_" ^ !special_config in - let configs = Str.split split_config (String.trim names) in + let configs = split_config (String.trim names) in if List.exists is_current_config configs then (* Found options for current config! *) scan_options dir scan_buffer default diff --git a/src/plugins/report/tests/report/classify.c b/src/plugins/report/tests/report/classify.c index 8a893876607..14b2e87c2fd 100644 --- a/src/plugins/report/tests/report/classify.c +++ b/src/plugins/report/tests/report/classify.c @@ -1,5 +1,5 @@ /* run.config - PLUGIN: wp rtegen + PLUGIN: wp rtegen @PLUGIN@ CMD: @frama-c@ -kernel-warn-key=annot-error=active -report-output classified.@PTEST_NUMBER@.json -wp -wp-msg-key shell LOG: classified.@PTEST_NUMBER@.json OPT: -wp-prover qed -report-unclassified-untried REVIEW -then -report-classify diff --git a/src/plugins/report/tests/report/csv.c b/src/plugins/report/tests/report/csv.c index d2ea04eb37a..c2297cddd44 100644 --- a/src/plugins/report/tests/report/csv.c +++ b/src/plugins/report/tests/report/csv.c @@ -1,5 +1,5 @@ /* run.config - PLUGIN: from inout scope eva + PLUGIN: from inout scope eva @PLUGIN@ LOG: csv.csv OPT: -eva-warn-copy-indeterminate=-main4 -eva -eva-show-progress -eva-remove-redundant-alarms -eva-warn-key=alarm=inactive -then -report-csv csv.csv -report-no-proven -then -report-csv= -eva-warn-key=alarm -eva-slevel 1 COMMENT: first, do an analysis without any message, but check that the .csv is complete. Then, redo the analysis with value warnings. slevel 1 is just there to force Value to restart diff --git a/src/plugins/report/tests/report/test_config b/src/plugins/report/tests/report/test_config index 3c86d703703..62ab168d887 100644 --- a/src/plugins/report/tests/report/test_config +++ b/src/plugins/report/tests/report/test_config @@ -1 +1 @@ -PLUGIN: report +PLUGIN: @PLUGIN@ report diff --git a/tests/builtins/big_local_array.i b/tests/builtins/big_local_array.i index 5dbf03b97e3..0b931e1f1fe 100644 --- a/tests/builtins/big_local_array.i +++ b/tests/builtins/big_local_array.i @@ -1,5 +1,5 @@ /* run.config* - PLUGIN: report + PLUGIN: report @EVA_PLUGINS@ CMXS: big_local_array_script OPT: @EVA_OPTIONS@ -print -journal-disable -eva -report OPT: @EVA_OPTIONS@ -load-module %{dep:big_local_array_script.cmxs} -then-on prj -print -report diff --git a/tests/builtins/test_config b/tests/builtins/test_config index e5aae733192..345f347fd40 100644 --- a/tests/builtins/test_config +++ b/tests/builtins/test_config @@ -1,3 +1,3 @@ MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic +MACRO: EVA_CONFIG @EVA_OPTIONS@ OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps diff --git a/tests/constant_propagation/bts117.c b/tests/constant_propagation/bts117.c index ac5f9db79c6..8577ea903ae 100644 --- a/tests/constant_propagation/bts117.c +++ b/tests/constant_propagation/bts117.c @@ -1,5 +1,5 @@ /* run.config -PLUGIN: sparecode +PLUGIN: sparecode @PLUGIN@ OPT: -journal-disable -print OPT: -journal-disable -semantic-const-folding @EVA_OPTIONS@ OPT: -journal-disable -sparecode-analysis @EVA_OPTIONS@ diff --git a/tests/constant_propagation/test_config b/tests/constant_propagation/test_config index 6aebd71be9a..9b002f56c8c 100644 --- a/tests/constant_propagation/test_config +++ b/tests/constant_propagation/test_config @@ -1,2 +1,2 @@ -PLUGIN: constant_propagation +PLUGIN: constant_propagation @PLUGIN@ OPT: -journal-disable @EVA_OPTIONS@ -scf diff --git a/tests/impact/test_config b/tests/impact/test_config index 7b96f2e94e5..39d00a53e25 100644 --- a/tests/impact/test_config +++ b/tests/impact/test_config @@ -1,2 +1,2 @@ -PLUGIN: impact +PLUGIN: impact @EVA_PLUGINS@ OPT: -journal-disable -impact-print @EVA_OPTIONS@ diff --git a/tests/journal/control2.c b/tests/journal/control2.c index 4271c1d25dd..f5c82393b8e 100644 --- a/tests/journal/control2.c +++ b/tests/journal/control2.c @@ -1,7 +1,7 @@ /* run.config EXECNOW: BIN control_journal2.ml frama-c @FRAMA_C_PLUGINS_OPTIONS@ -journal-enable -eva -deps -out -main f -journal-name control_journal2.ml @PTEST_FILE@ > /dev/null 2> /dev/null EXECNOW: LOG control2_sav.res LOG control2_sav.err BIN control_journal_next2.ml frama-c @FRAMA_C_PLUGINS_OPTIONS@ -journal-enable -load-script %{dep:control_journal2.ml} -lib-entry -journal-name control_journal_next2.ml @PTEST_FILE@ > control2_sav.res 2> control2_sav.err - PLUGIN: callgraph + PLUGIN: callgraph @EVA_PLUGINS@ OPT: -load-script %{dep:control_journal_next2.ml} */ diff --git a/tests/journal/intra.i b/tests/journal/intra.i index 3ece0a57f2b..9d3006bde7e 100644 --- a/tests/journal/intra.i +++ b/tests/journal/intra.i @@ -1,5 +1,5 @@ /* run.config - PLUGIN: sparecode + PLUGIN: sparecode @EVA_PLUGINS@ CMXS: @PTEST_NAME@ EXECNOW: BIN intra_journal.ml frama-c -eva-show-progress -no-autoload-plugins -load-plugin from,inout,eva,scope,variadic,sparecode -load-module %{dep:@PTEST_NAME@.cmxs} -journal-enable -journal-name intra_journal.ml @PTEST_NAME@.i > /dev/null 2> /dev/null CMD: @frama-c@ -load-module %{dep:@PTEST_NAME@.cmxs} diff --git a/tests/libc/coverage.c b/tests/libc/coverage.c index b6249280cb5..e11d52b0330 100644 --- a/tests/libc/coverage.c +++ b/tests/libc/coverage.c @@ -1,5 +1,5 @@ /* run.config* - PLUGIN: metrics + PLUGIN: metrics @EVA_PLUGINS@ OPT: -eva-no-builtins-auto @EVA_OPTIONS@ %{read:../../syntax/framac_share_path}/libc/string.c -eva -eva-slevel 6 -metrics-eva-cover -then -metrics-libc */ diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c index 28076bd24ca..3279d4aa85c 100644 --- a/tests/libc/fc_libc.c +++ b/tests/libc/fc_libc.c @@ -4,7 +4,7 @@ CMXS: check_parsing_individual_headers CMXS: check_libc_anonymous_tags CMXS: check_compliance - PLUGIN: metrics + PLUGIN: metrics @EVA_PLUGINS@ OPT: -load-module %{dep:check_libc_naming_conventions.cmxs} -print -cpp-extra-args='-nostdinc' -metrics -metrics-libc -load-module %{dep:check_const.cmxs} -eva @EVA_CONFIG@ -then -lib-entry -no-print -metrics-no-libc OPT: -print -print-libc OPT: -load-module %{dep:check_parsing_individual_headers.cmxs} diff --git a/tests/metrics/test_config b/tests/metrics/test_config index dc12a108121..11d2b5331ce 100644 --- a/tests/metrics/test_config +++ b/tests/metrics/test_config @@ -1,2 +1,2 @@ -PLUGIN: metrics +PLUGIN: @PLUGIN@ metrics OPT: -metrics diff --git a/tests/misc/add_assigns.i b/tests/misc/add_assigns.i index e61ecc871b3..13b86591a9b 100644 --- a/tests/misc/add_assigns.i +++ b/tests/misc/add_assigns.i @@ -1,5 +1,5 @@ /* run.config -PLUGIN: report +PLUGIN: report @EVA_PLUGINS@ MODULE: @PTEST_NAME@.cmxs OPT: -then -report -then -print */ diff --git a/tests/misc/bts1347.i b/tests/misc/bts1347.i index b22939220f4..2df285ccb7d 100644 --- a/tests/misc/bts1347.i +++ b/tests/misc/bts1347.i @@ -1,5 +1,5 @@ /* run.config - PLUGIN: report + PLUGIN: report @EVA_PLUGINS@ MODULE: @PTEST_NAME@.cmxs OPT: @EVA_OPTIONS@ -then -report */ diff --git a/tests/misc/obfuscate.c b/tests/misc/obfuscate.c index 2683da037cd..d28ccfb42f9 100644 --- a/tests/misc/obfuscate.c +++ b/tests/misc/obfuscate.c @@ -1,5 +1,5 @@ /* run.config - PLUGIN: obfuscator + PLUGIN: obfuscator @EVA_PLUGINS@ OPT: -obfuscate */ int my_var = 0; diff --git a/tests/occurrence/test_config b/tests/occurrence/test_config index 8b5da9340d4..029a71e6518 100644 --- a/tests/occurrence/test_config +++ b/tests/occurrence/test_config @@ -1,2 +1,2 @@ -PLUGIN: occurrence +PLUGIN: occurrence @EVA_PLUGINS@ STDOPT: -"-eva" -"-out" -"-input" -"-deps" +"-occurrence-verbose 1" diff --git a/tests/pdg/bts1194.c b/tests/pdg/bts1194.c index 3836571d3f5..aaa06aacad1 100644 --- a/tests/pdg/bts1194.c +++ b/tests/pdg/bts1194.c @@ -1,5 +1,5 @@ /* run.config - PLUGIN: slicing + PLUGIN: slicing @EVA_PLUGINS@ STDOPT: +"-eva -inout -pdg -calldeps -deps -then -slice-return main -then-last -print @EVA_OPTIONS@" */ diff --git a/tests/pdg/test_config b/tests/pdg/test_config index b5c1a82645a..78c7757cadf 100644 --- a/tests/pdg/test_config +++ b/tests/pdg/test_config @@ -1,2 +1,2 @@ -PLUGIN: pdg +PLUGIN: pdg @EVA_PLUGINS@ OPT: -journal-disable @EVA_OPTIONS@ -pdg-print -pdg-verbose 2 diff --git a/tests/pretty_printing/ghost_parameters.c b/tests/pretty_printing/ghost_parameters.c index 125ea27e9af..74638a96fb5 100644 --- a/tests/pretty_printing/ghost_parameters.c +++ b/tests/pretty_printing/ghost_parameters.c @@ -1,8 +1,8 @@ /* run.config + PLUGIN: STDOPT: +"-kernel-warn-key ghost:bad-use=inactive" */ // Note: we deactivate ghost:bad-use to check that pretty-printing ghost well - void decl_function_void_no_ghost(void); void def_function_void_no_ghost(void) {} void decl_function_void_ghost(void) /*@ ghost (int y) */; @@ -49,4 +49,4 @@ int main(void) { decl_variadic(2, 1, 2, 3, 4, 4); def_variadic(2, 1, 2, 3, 4, 4); */ -} \ No newline at end of file +} diff --git a/tests/rte/test_config b/tests/rte/test_config new file mode 100644 index 00000000000..60080e46918 --- /dev/null +++ b/tests/rte/test_config @@ -0,0 +1 @@ +PLUGIN: rtegen @EVA_PLUGINS@ diff --git a/tests/rte/value_rte.c b/tests/rte/value_rte.c index f5fe77aaf87..186136b4a70 100644 --- a/tests/rte/value_rte.c +++ b/tests/rte/value_rte.c @@ -1,5 +1,5 @@ /* run.config -PLUGIN: report +PLUGIN: report @EVA_PLUGINS@ OPT: -rte -then -eva @EVA_OPTIONS@ -then -report */ diff --git a/tests/saveload/load_one.i b/tests/saveload/load_one.i index 2fda92d767a..de48930209e 100644 --- a/tests/saveload/load_one.i +++ b/tests/saveload/load_one.i @@ -1,5 +1,5 @@ /* run.config - PLUGIN: sparecode + PLUGIN: sparecode @EVA_PLUGINS@ MODULE: @PTEST_NAME@.cmxs STDOPT: */ diff --git a/tests/saveload/multi_project.i b/tests/saveload/multi_project.i index 8fc7d7c5ea4..d7151a31dc4 100644 --- a/tests/saveload/multi_project.i +++ b/tests/saveload/multi_project.i @@ -1,5 +1,5 @@ /* run.config - PLUGIN: constant_propagation + PLUGIN: @PLUGIN@ constant_propagation EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -save @PTEST_NAME@.sav @EVA_OPTIONS@ -semantic-const-folding > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err CMXS: @PTEST_NAME@ STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -journal-disable" diff --git a/tests/saveload/sparecode.i b/tests/saveload/sparecode.i index d918bbf6f05..8e0ef20549a 100644 --- a/tests/saveload/sparecode.i +++ b/tests/saveload/sparecode.i @@ -1,5 +1,5 @@ /* run.config - PLUGIN: slicing + PLUGIN: @PLUGIN@ slicing EXECNOW: BIN sparecode.sav LOG sparecode_sav.res LOG sparecode_sav.err @frama-c@ -slicing-level 2 -slice-return main -eva-show-progress -save sparecode.sav -then-on 'Slicing export' -print > sparecode_sav.res 2> sparecode_sav.err STDOPT: +"-load %{dep:sparecode.sav}" */ diff --git a/tests/scope/zones.c b/tests/scope/zones.c index 7923d96d228..80fc7e30553 100644 --- a/tests/scope/zones.c +++ b/tests/scope/zones.c @@ -1,5 +1,5 @@ /* run.config - PLUGIN: pdg + PLUGIN: @EVA_PLUGINS@ pdg CMXS: @PTEST_NAME@ OPT: -load-module %{dep:@PTEST_NAME@.cmxs} -eva @EVA_OPTIONS@ -journal-disable */ diff --git a/tests/slicing/combine.i b/tests/slicing/combine.i index 678556ebe03..b8d6fd959c1 100644 --- a/tests/slicing/combine.i +++ b/tests/slicing/combine.i @@ -1,5 +1,5 @@ /* run.config - PLUGIN: constant_propagation + PLUGIN: constant_propagation @PLUGIN@ CMD: @frama-c@ -load-plugin slicing -load-plugin constant_propagation -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs} OPT: @EVA_OPTIONS@ -deps -journal-disable */ diff --git a/tests/slicing/test_config b/tests/slicing/test_config index d33c6619cf5..2a8603f22a8 100644 --- a/tests/slicing/test_config +++ b/tests/slicing/test_config @@ -1,2 +1,2 @@ -PLUGIN: slicing +PLUGIN: slicing @EVA_PLUGINS@ OPT: @EVA_OPTIONS@ diff --git a/tests/sparecode/test_config b/tests/sparecode/test_config index a8bbd0d9d8f..f86aafd98cf 100644 --- a/tests/sparecode/test_config +++ b/tests/sparecode/test_config @@ -1,2 +1,2 @@ -PLUGIN: sparecode slicing +PLUGIN: @PLUGIN@ sparecode slicing OPT: -journal-disable @EVA_OPTIONS@ -sparecode-debug 1 diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i index 8f06f2a0a58..5e604fd79a3 100644 --- a/tests/spec/generalized_check.i +++ b/tests/spec/generalized_check.i @@ -1,5 +1,5 @@ /* run.config -PLUGIN: wp +PLUGIN: wp @PLUGIN@ OPT: -wp -wp-prover qed -wp-msg-key shell OPT: -eva -eva-use-spec f OPT: -print diff --git a/tests/test_config b/tests/test_config index 6a01eb0573a..fecc43ece34 100644 --- a/tests/test_config +++ b/tests/test_config @@ -1,4 +1,5 @@ -PLUGIN: from inout eva scope variadic +MACRO: EVA_PLUGINS from inout eva scope variadic MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-plugin from,inout,eva,scope,variadic -OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps +MACRO: EVA_CONFIG @EVA_OPTIONS@ +PLUGIN: @EVA_PLUGINS@ +OPT: -eva @EVA_OPTIONS@ -journal-disable -out -input -deps diff --git a/tests/value/from_call.i b/tests/value/from_call.i index da1f6008c9d..b8d1ded1c9c 100644 --- a/tests/value/from_call.i +++ b/tests/value/from_call.i @@ -1,7 +1,7 @@ /* run.config* - OPT: -no-autoload-plugins -load-module from,eva @EVA_CONFIG@ -deps -show-indirect-deps -journal-disable - PLUGIN: users - OPT: -calldeps -eva @EVA_CONFIG@ -journal-disable -users -then -input + OPT: @EVA_OPTIONS@ -deps -show-indirect-deps -journal-disable + PLUGIN: users @PLUGIN@ + OPT: -calldeps -eva @EVA_OPTIONS@ -journal-disable -users -then -input */ int a,b,c,d; int x,y,z,t; diff --git a/tests/value/ilevel.i b/tests/value/ilevel.i index 1e573528e72..7211a7e64ec 100644 --- a/tests/value/ilevel.i +++ b/tests/value/ilevel.i @@ -1,6 +1,6 @@ /* run.config* - PLUGIN: slicing sparecode - OPT: -eva @EVA_CONFIG@ -slice-return main -then-on "Slicing export" -eva -eva-ilevel 16 -eva-show-progress -then-on "default" -eva-ilevel 17 -then -eva-ilevel 48 + PLUGIN: slicing sparecode @PLUGIN@ + OPT: -eva @EVA_OPTIONS@ -slice-return main -then-on "Slicing export" -eva -eva-ilevel 16 -eva-show-progress -then-on "default" -eva-ilevel 17 -then -eva-ilevel 48 */ // Test in particular that ilevel is by-project, even though it is an ocaml ref volatile int v; diff --git a/tests/value/redundant_alarms.c b/tests/value/redundant_alarms.c index 6d4f63fb1ed..56c24a7649e 100644 --- a/tests/value/redundant_alarms.c +++ b/tests/value/redundant_alarms.c @@ -1,5 +1,5 @@ /* run.config* - PLUGIN: slicing sparecode + PLUGIN: @EVA_PLUGINS@ slicing sparecode OPT: @EVA_CONFIG@ -eva-warn-copy-indeterminate=-@all,main3 -scope-msg-key rm_asserts -scope-verbose 2 -eva-remove-redundant-alarms -print -slice-threat main1 -then-on 'Slicing export' -print **/ -- GitLab