diff --git a/ptests/ptests.ml b/ptests/ptests.ml index 7cc8be13f10d51f357be5f3f5ffed59a5b8392fb..210aa2dde3b06f325e742145b3fd8c5ed0bdc8d1 100644 --- a/ptests/ptests.ml +++ b/ptests/ptests.ml @@ -124,28 +124,6 @@ let end_comment = Str.regexp ".*\\*/" let regex_cmxs = Str.regexp ("\\([^/]+\\)[.]cmxs\\($\\|[ \t]\\)") -let opt_to_byte toplevel = - match string_del_suffix "frama-c" toplevel with - | Some path -> path ^ "frama-c.byte" - | None -> - match string_del_suffix "toplevel.opt" toplevel with - | Some path -> path ^ "toplevel.byte" - | None -> - match string_del_suffix "frama-c-gui" toplevel with - | Some path -> path ^ "frama-c-gui.byte" - | None -> - match string_del_suffix "viewer.opt" toplevel with - | Some path -> path ^ "viewer.byte" - | None -> toplevel - -let opt_to_byte_options options = - str_global_replace regex_cmxs "\\1.cmo\\2" options - -let execnow_opt_to_byte cmd = - let cmd = opt_to_byte cmd in - opt_to_byte_options cmd - - let output_unix_error (exn : exn) = match exn with | Unix.Unix_error (error, _function, arg) -> @@ -204,12 +182,6 @@ let do_make = ref "make" let n = ref 4 (* the level of parallelism *) let suites = ref [] -(** options appended to toplevel for all tests *) -let additional_options = ref "" - -(** options prepended to toplevel for all tests *) -let additional_options_pre = ref "" - (** special configuration, with associated oracles *) let special_config = ref "" let do_error_code = ref false @@ -308,14 +280,6 @@ let rec argspec = " Use native toplevel (default)"; "-config", Arg.Set_string special_config, " <name> Use special configuration and oracles"; - "-add-options", Arg.Set_string additional_options, - "<options> Add additional options to be passed to the toplevels \ - that will be launched. <options> are added after standard test options"; - "-add-options-pre", Arg.Set_string additional_options_pre, - "<options> Add additional options to be passed to the toplevels \ - that will be launched. <options> are added before standard test options."; - "-add-options-post", Arg.Set_string additional_options, - "Synonym of -add-options"; "-xunit", Arg.Set xunit, " Create a xUnit file named xunit.xml collecting results"; "-error-code", Arg.Set do_error_code, @@ -582,11 +546,7 @@ type config = dc_timeout: string } -let default_macros () = - let l = [ - "frama-c", "frama-c"; - ] in - Macros.add_list l Macros.empty +let default_macros () = Macros.empty let default_config () = { dc_test_regexp = test_file_regexp ; @@ -597,7 +557,7 @@ let default_config () = dc_plugins = []; dc_load_module = []; dc_filter = None ; - dc_default_toplevel = "frama-c"; + dc_default_toplevel = "@frama-c@"; dc_toplevels = [ "frama-c", default_options, [], Macros.empty, "" ]; dc_dont_run = false; dc_framac = true; @@ -986,38 +946,32 @@ let frama_c_binary_name = let basic_command_string = fun command -> let macros = get_macros command in - let logfiles = List.map (Macros.expand macros) command.log_files in - command.log_files <- logfiles; - let has_ptest_file_t, toplevel = - Macros.does_expand macros command.toplevel - in - let has_ptest_file_o, options = Macros.does_expand macros command.options in - let toplevel = if !use_byte then opt_to_byte toplevel else toplevel in - let toplevel, contains_frama_c_binary = - str_string_match_and_replace contains_frama_c_binary_name - frama_c_binary_name ~suffix:" -check" toplevel + let plugins_options = + let opt_plugin = String.concat " " (List.map (Printf.sprintf "-load-plugin %s") command.plugins) in + let opt_modules = String.concat " " + (List.map (fun s -> Printf.sprintf " -load-module %S" (Macros.expand macros s)) + command.load_module) in + String.concat " " ["-no-autoload-plugins";opt_plugin;opt_modules] in + let options = Macros.expand macros command.options in + let macros = + Macros.add_list [ "OPTIONS", options; + "FRAMA_C_PLUGINS_OPTIONS", plugins_options; + ] macros in + let file = Filename.sanitize @@ get_ptest_file command in let options = - if contains_frama_c_binary - then begin - let opt_modules = String.concat " " - (List.map (fun s -> Printf.sprintf " -load-module %S" (Macros.expand macros s)) - command.load_module) in - let opt_pre = Macros.expand macros !additional_options_pre in - let opt_post = Macros.expand macros !additional_options in - let opt_plugin = String.concat " " (List.map (Printf.sprintf "-load-plugin %s") command.plugins) in - String.concat " " ["-no-autoload-plugins";opt_plugin;opt_modules;opt_pre;options;opt_post] - end else options + String.concat " " [file;plugins_options;options] in - let options = if !use_byte then opt_to_byte_options options else options in - let raw_command = - if has_ptest_file_t || has_ptest_file_o || command.execnow then - toplevel ^ " " ^ options - else begin - let file = Filename.sanitize @@ get_ptest_file command in - toplevel ^ " " ^ file ^ " " ^ options - end + let macros = Macros.add_list [ + "FRAMA_C_DEFAULT_OPTIONS",options; + "frama-c", "frama-c "^options; + ] macros in + let logfiles = List.map (Macros.expand macros) command.log_files in + command.log_files <- logfiles; + let toplevel = + Macros.expand macros command.toplevel in + let raw_command = toplevel in if command.timeout = "" then raw_command else "ulimit -t " ^ command.timeout ^ " && " ^ raw_command diff --git a/src/plugins/instantiate/tests/options/test_config b/src/plugins/instantiate/tests/options/test_config index abee799913e0ea0930f93912396cae4cbf46bb8d..b594387946c30bfe86470abe61791a7fa07451af 100644 --- a/src/plugins/instantiate/tests/options/test_config +++ b/src/plugins/instantiate/tests/options/test_config @@ -1,2 +1,2 @@ PLUGIN: instantiate -OPT: @PTEST_FILE@ -instantiate -check -print +OPT: -instantiate -check -print diff --git a/src/plugins/instantiate/tests/stdlib/test_config b/src/plugins/instantiate/tests/stdlib/test_config index f3094d70de038aa2957a7472287cda20d8ed8570..401dafb99f4190d48eb42e26cf45738ec4bc55bd 100644 --- a/src/plugins/instantiate/tests/stdlib/test_config +++ b/src/plugins/instantiate/tests/stdlib/test_config @@ -1 +1 @@ -OPT: @PTEST_FILE@ -instantiate -print -check -then -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -print -then -no-instantiate ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -ocode="" -print +OPT: -instantiate -print -check -then -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -print -then -no-instantiate ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -ocode="" -print diff --git a/src/plugins/instantiate/tests/string/test_config b/src/plugins/instantiate/tests/string/test_config index f3094d70de038aa2957a7472287cda20d8ed8570..401dafb99f4190d48eb42e26cf45738ec4bc55bd 100644 --- a/src/plugins/instantiate/tests/string/test_config +++ b/src/plugins/instantiate/tests/string/test_config @@ -1 +1 @@ -OPT: @PTEST_FILE@ -instantiate -print -check -then -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -print -then -no-instantiate ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -ocode="" -print +OPT: -instantiate -print -check -then -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -print -then -no-instantiate ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -ocode="" -print diff --git a/src/plugins/markdown-report/tests/eva/test_config b/src/plugins/markdown-report/tests/eva/test_config index b9757b17913cb571acccd8579512c29e0beda242..c7be0c1d592c2a8a8672ecbb3b4f0d06060fe2fe 100644 --- a/src/plugins/markdown-report/tests/eva/test_config +++ b/src/plugins/markdown-report/tests/eva/test_config @@ -1,3 +1,3 @@ PLUGIN: markdown-report eva inout -OPT: -eva @PTEST_FILE@ -then -mdr-gen md -mdr-date="now" -mdr-out @PTEST_NAME@.@PTEST_NUMBER@.md +OPT: -eva -then -mdr-gen md -mdr-date="now" -mdr-out @PTEST_NAME@.@PTEST_NUMBER@.md LOG: @PTEST_NAME@.@PTEST_NUMBER@.md diff --git a/src/plugins/report/tests/report/oracle/classify.0.res.oracle b/src/plugins/report/tests/report/oracle/classify.0.res.oracle index 30ccea3bc0636a1d6b4436166f5c5f1276a67605..ebfe0669fdd5667f0461154506e97e541311e3e9 100644 --- a/src/plugins/report/tests/report/oracle/classify.0.res.oracle +++ b/src/plugins/report/tests/report/oracle/classify.0.res.oracle @@ -1,4 +1,3 @@ -# frama-c -wp [...] [kernel] Parsing classify.c (with preprocessing) [kernel:annot-error] classify.c:27: Warning: unbound logic variable ignored. Ignoring code annotation diff --git a/src/plugins/report/tests/report/oracle/classify.1.res.oracle b/src/plugins/report/tests/report/oracle/classify.1.res.oracle index 0453ac2ee2dc97a9c6ee820e954350f550c9d4ba..92c49e08c37c35f3614f36d43b6cda3601a4cff9 100644 --- a/src/plugins/report/tests/report/oracle/classify.1.res.oracle +++ b/src/plugins/report/tests/report/oracle/classify.1.res.oracle @@ -1,5 +1,4 @@ [report] Monitoring events -# frama-c -wp [...] [kernel] Parsing classify.c (with preprocessing) [kernel:annot-error] classify.c:27: Warning: unbound logic variable ignored. Ignoring code annotation diff --git a/src/plugins/report/tests/report/oracle/classify.2.res.oracle b/src/plugins/report/tests/report/oracle/classify.2.res.oracle index 7238c685a85e12ce8b2655490cdf7f952f904aab..8b5f49e7c1504a0f61f660ea1b4e4fb88fa5d571 100644 --- a/src/plugins/report/tests/report/oracle/classify.2.res.oracle +++ b/src/plugins/report/tests/report/oracle/classify.2.res.oracle @@ -1,5 +1,4 @@ [report] Monitoring events -# frama-c -wp [...] [kernel] Parsing classify.c (with preprocessing) [kernel:annot-error] classify.c:27: Warning: unbound logic variable ignored. Ignoring code annotation diff --git a/src/plugins/report/tests/report/oracle/classify.3.res.oracle b/src/plugins/report/tests/report/oracle/classify.3.res.oracle index 11079f5864811c20f21a3fb4f42125360f189159..6568ac0a7d9954532d4da0a3fd823342efa3878b 100644 --- a/src/plugins/report/tests/report/oracle/classify.3.res.oracle +++ b/src/plugins/report/tests/report/oracle/classify.3.res.oracle @@ -1,6 +1,5 @@ [report] Monitoring events [report] Loading 'classify.json' -# frama-c -wp [...] [kernel] Parsing classify.c (with preprocessing) [kernel:annot-error] classify.c:27: Warning: unbound logic variable ignored. Ignoring code annotation diff --git a/src/plugins/report/tests/report/oracle/classify.4.res.oracle b/src/plugins/report/tests/report/oracle/classify.4.res.oracle index b4438b9bfb5eef32d2e08526686aa0b872e8f4ca..e43f8970349965423132200831e4ac76de669ca2 100644 --- a/src/plugins/report/tests/report/oracle/classify.4.res.oracle +++ b/src/plugins/report/tests/report/oracle/classify.4.res.oracle @@ -1,6 +1,5 @@ [report] Monitoring events [report] Loading 'classify.json' -# frama-c -wp [...] [kernel] Parsing classify.c (with preprocessing) [kernel:annot-error] classify.c:27: Warning: unbound logic variable ignored. Ignoring code annotation diff --git a/src/plugins/report/tests/report/oracle/classify.5.res.oracle b/src/plugins/report/tests/report/oracle/classify.5.res.oracle index d126b08201df9233162514dce94e09c316df7bbd..39e627312c3ed87daad48628e02f719f3f8320aa 100644 --- a/src/plugins/report/tests/report/oracle/classify.5.res.oracle +++ b/src/plugins/report/tests/report/oracle/classify.5.res.oracle @@ -1,6 +1,5 @@ [report] Monitoring events [report] Loading 'classify.json' -# frama-c -wp [...] [kernel] Parsing classify.c (with preprocessing) [kernel:annot-error] classify.c:27: Warning: unbound logic variable ignored. Ignoring code annotation diff --git a/tests/float/absorb.c b/tests/float/absorb.c index 7d284ad6cb7265e0e10232c83e0ac7854524f032..7a9e3cab596155c30ae2a11f31defb1f860a3eba 100644 --- a/tests/float/absorb.c +++ b/tests/float/absorb.c @@ -1,7 +1,7 @@ /* run.config COMMENT: run.config is intentionally not-* - EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err PTESTS_IT_DOESNT_START_WITH_FRAMAC=yes @frama-c@ -no-autoload-plugins -journal-disable -save absorb.sav @PTEST_FILE@ > absorb_sav.res 2> absorb_sav.err - EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err PTESTS_IT_DOESNT_START_WITH_FRAMAC=yes @frama-c@ -load %{dep:absorb.sav} -eva @EVA_CONFIG@ -journal-disable -float-hex -save absorb.sav2 > absorb_sav2.res 2> absorb_sav2.err + EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err frama-c -no-autoload-plugins -journal-disable -save absorb.sav @PTEST_FILE@ > absorb_sav.res 2> absorb_sav.err + EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err frama-c @FRAMA_C_PLUGINS_OPTIONS@ -load %{dep:absorb.sav} -eva @EVA_CONFIG@ -journal-disable -float-hex -save absorb.sav2 > absorb_sav2.res 2> absorb_sav2.err OPT: -load %{dep:absorb.sav2} -deps -out -input */ /* run.config* diff --git a/tests/journal/control.i b/tests/journal/control.i index 7611474cf1ec4219d9a55d56adf74c0f44cfd368..0830044b07ebffc8d9936ce0d3e143aee547af5f 100644 --- a/tests/journal/control.i +++ b/tests/journal/control.i @@ -1,13 +1,13 @@ /* run.config COMMENT: do not compare generated journals since they depend on current time - EXECNOW: BIN control_journal.ml BIN control_journal_bis.ml (frama-c -journal-enable -check -eva -deps -out @EVA_CONFIG@ -main f -journal-name control_journal.ml control.i && cp control_journal.ml control_journal_bis.ml) > /dev/null 2> /dev/null - CMD: frama-c + EXECNOW: BIN control_journal.ml BIN control_journal_bis.ml (frama-c @FRAMA_C_PLUGINS_OPTIONS@ -journal-enable -check -eva -deps -out @EVA_CONFIG@ -main f -journal-name control_journal.ml control.i && cp control_journal.ml control_journal_bis.ml) > /dev/null 2> /dev/null + CMD: @frama-c@ OPT: -load-script %{dep:control_journal.ml} -journal-disable - CMD: frama-c + CMD: @frama-c@ OPT: -load-script %{dep:control_journal_bis.ml} -calldeps -journal-disable CMXS: abstract_cpt - EXECNOW: BIN abstract_cpt_journal.ml frama-c -journal-enable -load-module %{dep:abstract_cpt.cmxs} -load-script %{dep:use_cpt.ml} -journal-name abstract_cpt_journal.ml > /dev/null 2> /dev/null - CMD: frama-c + EXECNOW: BIN abstract_cpt_journal.ml frama-c @FRAMA_C_PLUGINS_OPTIONS@ -journal-enable -load-module %{dep:abstract_cpt.cmxs} -load-script %{dep:use_cpt.ml} -journal-name abstract_cpt_journal.ml > /dev/null 2> /dev/null + CMD: @frama-c@ OPT: -load-script %{dep:abstract_cpt_journal.ml} -load-module abstract_cpt -load-script %{dep:use_cpt.ml} */ diff --git a/tests/journal/control2.c b/tests/journal/control2.c index 674aeb4609c7dde81c8df091224206f6a17a9570..4271c1d25dde76203988d36cfe1cccb8479c0d48 100644 --- a/tests/journal/control2.c +++ b/tests/journal/control2.c @@ -1,11 +1,12 @@ /* 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 - EXECNOW: BIN control_journal2.ml PTESTS_ITS_NOT_FRAMAC=yes frama-c -no-autoload-plugins -load-plugin from,inout,eva,scope,variadic -journal-enable -eva -deps -out -main f -journal-name control_journal2.ml control2.c > /dev/null 2> /dev/null - EXECNOW: LOG control2_sav.res LOG control2_sav.err BIN control_journal_next2.ml PTESTS_ITS_NOT_FRAMAC=yes frama-c -no-autoload-plugins -load-plugin from,inout,eva,scope,variadic -journal-enable -load-script %{dep:control_journal2.ml} -lib-entry -journal-name control_journal_next2.ml control2.c > control2_sav.res 2> control2_sav.err - CMD: PTESTS_ITS_NOT_FRAMAC=yes frama-c -no-autoload-plugins -load-plugin from,inout,eva,scope,variadic,callgraph OPT: -load-script %{dep:control_journal_next2.ml} */ +/* The last OPT was testing reading from byte when generated from native */ + int x,y,c,d; void f() { diff --git a/tests/journal/intra.i b/tests/journal/intra.i index cadfe3ac742a8cb20046d887403e16422bed80e9..3ece0a57f2b2d5cf62af0fdcaf7a17db50bb4abd 100644 --- a/tests/journal/intra.i +++ b/tests/journal/intra.i @@ -1,7 +1,7 @@ /* run.config PLUGIN: sparecode CMXS: @PTEST_NAME@ - EXECNOW: BIN intra_journal.ml PTESTS_IT_IS_NOT_FRAMAC=yes @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 + 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} OPT: -load-script %{dep:intra_journal.ml} -journal-disable */ diff --git a/tests/journal/oracle/control2.res.oracle b/tests/journal/oracle/control2.res.oracle index 92d19a0804ce232020e802275fdf33b02cefac2d..02360dafcbcd947c5433d8da5a563e80a378bd8f 100644 --- a/tests/journal/oracle/control2.res.oracle +++ b/tests/journal/oracle/control2.res.oracle @@ -7,8 +7,8 @@ y ∈ {0} c ∈ {0} d ∈ {0} -[eva] control2.c:13: starting to merge loop iterations -[eva:alarm] control2.c:16: Warning: +[eva] control2.c:14: starting to merge loop iterations +[eva:alarm] control2.c:17: Warning: signed overflow. assert x + 1 ≤ 2147483647; [eva] done for function f [eva] ====== VALUES COMPUTED ====== @@ -37,11 +37,11 @@ y ∈ [--..--] c ∈ [--..--] d ∈ [--..--] -[eva:alarm] control2.c:14: Warning: +[eva:alarm] control2.c:15: Warning: signed overflow. assert y + 1 ≤ 2147483647; -[eva:alarm] control2.c:14: Warning: +[eva:alarm] control2.c:15: Warning: signed overflow. assert x + 1 ≤ 2147483647; -[eva:alarm] control2.c:16: Warning: +[eva:alarm] control2.c:17: Warning: signed overflow. assert x + 1 ≤ 2147483647; [eva] done for function f [eva] ====== VALUES COMPUTED ====== diff --git a/tests/journal/oracle/control2_sav.res b/tests/journal/oracle/control2_sav.res index fbebf504547e529cb7fae1b3d9160662c8288b72..1734f9bb5372539b42ca6899a554625e521d5272 100644 --- a/tests/journal/oracle/control2_sav.res +++ b/tests/journal/oracle/control2_sav.res @@ -7,8 +7,8 @@ y ∈ {0} c ∈ {0} d ∈ {0} -[eva] control2.c:13: starting to merge loop iterations -[eva:alarm] control2.c:16: Warning: +[eva] control2.c:14: starting to merge loop iterations +[eva:alarm] control2.c:17: Warning: signed overflow. assert x + 1 ≤ 2147483647; [eva] done for function f [eva] ====== VALUES COMPUTED ====== @@ -38,11 +38,11 @@ y ∈ [--..--] c ∈ [--..--] d ∈ [--..--] -[eva:alarm] control2.c:14: Warning: +[eva:alarm] control2.c:15: Warning: signed overflow. assert y + 1 ≤ 2147483647; -[eva:alarm] control2.c:14: Warning: +[eva:alarm] control2.c:15: Warning: signed overflow. assert x + 1 ≤ 2147483647; -[eva:alarm] control2.c:16: Warning: +[eva:alarm] control2.c:17: Warning: signed overflow. assert x + 1 ≤ 2147483647; [eva] done for function f [eva] ====== VALUES COMPUTED ====== diff --git a/tests/libc/runtime.c b/tests/libc/runtime.c index ca77f67fa8259ba23d18b8e5fef32e0aad57145f..8c3522845b4a730f3d91a564c707fc7365124237 100644 --- a/tests/libc/runtime.c +++ b/tests/libc/runtime.c @@ -1,8 +1,8 @@ /* run.config* COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...) DEPS: ../../../share/libc/__fc_runtime.c - CMD: gcc -D__FC_MACHDEP_X86_64 ../../../share/libc/__fc_runtime.c -Wno-attributes -std=c99 -o /dev/null - OPT: + CMD: gcc @OPTIONS@ + OPT: -D__FC_MACHDEP_X86_64 ../../../share/libc/__fc_runtime.c -Wno-attributes -std=c99 -o /dev/null @PTEST_FILE@ */ int main() { diff --git a/tests/misc/my_visitor.c b/tests/misc/my_visitor.c index 03f2242c110c60d77feb17defa19f726d66563d0..52aecdc00664b2b1dee7e76e84be2feaa34dbbf6 100644 --- a/tests/misc/my_visitor.c +++ b/tests/misc/my_visitor.c @@ -1,6 +1,6 @@ /* run.config CMXS: @PTEST_NAME@ -EXECNOW: LOG my_visitor_sav.res LOG my_visitor_sav.err BIN my_visitor.sav @frama-c@ @PTEST_FILE@ -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -main f -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err +EXECNOW: LOG my_visitor_sav.res LOG my_visitor_sav.err BIN my_visitor.sav @frama-c@ -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -main f -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err OPT: -load %{dep:@PTEST_NAME@.sav} -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -no-my-visitor -print OPT: -load %{dep:@PTEST_NAME@.sav} -no-autoload-plugins -print */ diff --git a/tests/pretty_printing/parenthesis.c b/tests/pretty_printing/parenthesis.c index fc923fe3d2751e03d3f539ff7c0bac58f5295a8f..9e25bb53be7de6a9479b8354104ce4346c47b27a 100644 --- a/tests/pretty_printing/parenthesis.c +++ b/tests/pretty_printing/parenthesis.c @@ -1,5 +1,5 @@ /* run.config - OPT: -print + OPT: @PTEST_FILE@ -print */ /*@ diff --git a/tests/pretty_printing/test_config b/tests/pretty_printing/test_config index 25d5f233dbc1ea60820a3b195dd1d100d27449cb..f5d302bd1d2de212124d7647c6c235256fc04af6 100644 --- a/tests/pretty_printing/test_config +++ b/tests/pretty_printing/test_config @@ -1,5 +1,5 @@ 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 -CMD: FRAMAC_PLUGIN=tests/.empty @frama-c@ -no-autoload-plugins +CMD: frama-c -no-autoload-plugins @OPTIONS@ OPT: @PTEST_FILE@ -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/select_by_annot.i b/tests/slicing/select_by_annot.i index 1a70a1cd5adb13b8ad4502e25f709d911b955c58..5e40c065648a79682355554a94db5b2da22df65d 100644 --- a/tests/slicing/select_by_annot.i +++ b/tests/slicing/select_by_annot.i @@ -1,8 +1,8 @@ /* run.config - CMD: @frama-c@ -load-plugin slicing -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs} + CMD: frama-c @FRAMA_C_DEFAULT_OPTIONS@ -load-plugin slicing -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs} OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -journal-disable - CMD: frama-c + CMD: frama-c @FRAMA_C_DEFAULT_OPTIONS@ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-assert main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma modifS -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps diff --git a/tests/sparecode/oracle/intra.2.res.oracle b/tests/sparecode/oracle/intra.2.res.oracle index 47d7d4b3d0439b7b5982481bb2dd11bc0f9a7db1..0a930fe52d15f295b7d5230a905fdc4706dd6213 100644 --- a/tests/sparecode/oracle/intra.2.res.oracle +++ b/tests/sparecode/oracle/intra.2.res.oracle @@ -40,7 +40,7 @@ [pdg] Bottom for function spare_called_fct [pdg] computing for function stop [from] Computing for function stop -[kernel:annot:missing-spec] intra.i:110: Warning: +[kernel:annot:missing-spec] intra.i:35: Warning: Neither code nor specification for function stop, generating default assigns from the prototype [from] Done for function stop [pdg] done for function stop diff --git a/tests/sparecode/oracle/top.0.res.oracle b/tests/sparecode/oracle/top.0.res.oracle index c078269a00831d2d1551123b390e21a7749b1790..f6425c3ba77e6b178af1e93ece8dc79a2307d1c9 100644 --- a/tests/sparecode/oracle/top.0.res.oracle +++ b/tests/sparecode/oracle/top.0.res.oracle @@ -45,7 +45,7 @@ [sparecode] look for annotations in function print [pdg] computing for function print [from] Computing for function print -[kernel:annot:missing-spec] top.i:16: Warning: +[kernel:annot:missing-spec] top.i:11: Warning: Neither code nor specification for function print, generating default assigns from the prototype [from] Done for function print [pdg] done for function print diff --git a/tests/sparecode/oracle/top.2.res.oracle b/tests/sparecode/oracle/top.2.res.oracle index 6dc821c49b508e825653952187112df6bc49e527..600c507df795750daf4966d0389e276fc03124b7 100644 --- a/tests/sparecode/oracle/top.2.res.oracle +++ b/tests/sparecode/oracle/top.2.res.oracle @@ -46,7 +46,7 @@ [sparecode] look for annotations in function print [pdg] computing for function print [from] Computing for function print -[kernel:annot:missing-spec] top.i:22: Warning: +[kernel:annot:missing-spec] top.i:11: Warning: Neither code nor specification for function print, generating default assigns from the prototype [from] Done for function print [pdg] done for function print diff --git a/tests/spec/anon_arg_2.i b/tests/spec/anon_arg_2.i index 80197a9b0f7a8f0442765c3be2a4027286a339f0..fad55c929f4e7f07f8be947d1fc83d887158978c 100644 --- a/tests/spec/anon_arg_2.i +++ b/tests/spec/anon_arg_2.i @@ -1,5 +1,6 @@ /* run.config* -STDOPT: #"%{dep:anon_arg_1.i} @PTEST_FILE@" +CMD: frama-c @FRAMA_C_PLUGINS_OPTIONS@ @OPTIONS@ %{dep:anon_arg_1.i} @PTEST_FILE@ +OPT: -pp-annot -print -journal-disable -kernel-warn-key=annot-error=active -check */ /*@ requires \valid(p); diff --git a/tests/spec/clash_double_file_bts1598.c b/tests/spec/clash_double_file_bts1598.c index f3340e93f6983a4750700cf32863b64c9862b583..37446ed82f5aea474053ccc80c95ee554259b8d3 100644 --- a/tests/spec/clash_double_file_bts1598.c +++ b/tests/spec/clash_double_file_bts1598.c @@ -1,7 +1,7 @@ /* run.config COMMENT: checks that linking string.h and its FC-pretty-printed version COMMENT: does not get rejected by name clash in the logic. See bts 1598 -OPT: @PTEST_FILE@ -cpp-extra-args " -Ishare/libc -nostdinc" -print -then -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -print -then @PTEST_FILE@ ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -ocode="" -print +OPT: -cpp-extra-args " -Ishare/libc -nostdinc" -print -then -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -print -then @PTEST_FILE@ ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -ocode="" -print */ #include "__fc_builtin.h" diff --git a/tests/spec/rm_qualifiers.i b/tests/spec/rm_qualifiers.i index d6d739b95cc0027f358736a6e5f9ae367aca9159..a8f58e6e66622b43da2aeb755cc71ccc31f06f90 100644 --- a/tests/spec/rm_qualifiers.i +++ b/tests/spec/rm_qualifiers.i @@ -1,5 +1,5 @@ /* run.config -OPT: @PTEST_FILE@ -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -print -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -ocode="" -print +OPT: -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -print -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -ocode="" -print */ extern void G(const void* p); typedef volatile int ARR[42][3]; diff --git a/tests/syntax/multiple_decls_contracts.c b/tests/syntax/multiple_decls_contracts.c index 1b32185cfe8e78368411c15bda76e5b31ff7cea0..11e4ec8462668d3cb5f2d2f2739e1a9eaeb8ef62 100644 --- a/tests/syntax/multiple_decls_contracts.c +++ b/tests/syntax/multiple_decls_contracts.c @@ -1,4 +1,5 @@ /* run.config +CMD: frama-c @FRAMA_C_PLUGINS_OPTIONS@ @OPTIONS@ OPT:%{read:../framac_share_path}/libc/string.h @PTEST_FILE@ @PTEST_FILE@ -print OPT: @PTEST_FILE@ %{read:../framac_share_path}/libc/string.h @PTEST_FILE@ -print OPT: @PTEST_FILE@ @PTEST_FILE@ %{read:../framac_share_path}/libc/string.h -print diff --git a/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle b/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle index 49e36a7bc9637e4de1698ba1149b6d9ff51b5f64..4b4eb64378562e3e1c2df666a77713a52fcf2359 100644 --- a/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle +++ b/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle @@ -1,8 +1,8 @@ [kernel] Parsing FRAMAC_SHARE/libc/string.h (with preprocessing) [kernel] Parsing multiple_decls_contracts.c (with preprocessing) [kernel] Parsing multiple_decls_contracts.c (with preprocessing) -[kernel] multiple_decls_contracts.c:10: Warning: - dropping duplicate def'n of func strdup at multiple_decls_contracts.c:10 in favor of that at multiple_decls_contracts.c:10 +[kernel] multiple_decls_contracts.c:11: Warning: + dropping duplicate def'n of func strdup at multiple_decls_contracts.c:11 in favor of that at multiple_decls_contracts.c:11 /* Generated by Frama-C */ #include "stddef.h" #include "stdlib.h" diff --git a/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle b/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle index 50638f1cb54fb1518b7f2c83c791765c3baa4be6..c56b7c7de437e7f0c77536924de948efc293a980 100644 --- a/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle +++ b/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle @@ -1,8 +1,8 @@ [kernel] Parsing multiple_decls_contracts.c (with preprocessing) [kernel] Parsing FRAMAC_SHARE/libc/string.h (with preprocessing) [kernel] Parsing multiple_decls_contracts.c (with preprocessing) -[kernel] multiple_decls_contracts.c:10: Warning: - dropping duplicate def'n of func strdup at multiple_decls_contracts.c:10 in favor of that at multiple_decls_contracts.c:10 +[kernel] multiple_decls_contracts.c:11: Warning: + dropping duplicate def'n of func strdup at multiple_decls_contracts.c:11 in favor of that at multiple_decls_contracts.c:11 /* Generated by Frama-C */ #include "stddef.h" #include "stdlib.h" diff --git a/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle b/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle index 364dd1fa5a6fd84939e45f8e31186c0869868d77..15c98417a221dfedba40eee013fdc0cd695c3e31 100644 --- a/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle +++ b/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle @@ -1,8 +1,8 @@ [kernel] Parsing multiple_decls_contracts.c (with preprocessing) [kernel] Parsing multiple_decls_contracts.c (with preprocessing) [kernel] Parsing FRAMAC_SHARE/libc/string.h (with preprocessing) -[kernel] multiple_decls_contracts.c:10: Warning: - dropping duplicate def'n of func strdup at multiple_decls_contracts.c:10 in favor of that at multiple_decls_contracts.c:10 +[kernel] multiple_decls_contracts.c:11: Warning: + dropping duplicate def'n of func strdup at multiple_decls_contracts.c:11 in favor of that at multiple_decls_contracts.c:11 /* Generated by Frama-C */ #include "stddef.h" #include "stdlib.h" diff --git a/tests/syntax/typedef_incorrect_pretty_print_bts1518.i b/tests/syntax/typedef_incorrect_pretty_print_bts1518.i index 6ea6db2214d546cd4ab67bef619a4d2c234892fe..e9e92214c8cb97597524b595c4ba76b80055603c 100644 --- a/tests/syntax/typedef_incorrect_pretty_print_bts1518.i +++ b/tests/syntax/typedef_incorrect_pretty_print_bts1518.i @@ -1,7 +1,7 @@ /* run.config DONTRUN: bug fix in progress MACRO: OUT @PTEST_NAME@_res.i -EXECNOW: LOG @OUT@ @frama-c@ @PTEST_FILE@ -ocode @OUT@ -print -then @OUT@ -print +EXECNOW: LOG @OUT@ @frama-c@ -ocode @OUT@ -print -then @OUT@ -print */ /* Generated by Frama-C */ /* Generated by Frama-C */