From da626686733c11f28e860a990dafe5a5ea63cf14 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 6 Oct 2020 17:48:04 +0200
Subject: [PATCH] [PTESTS] simplify the heuristics of ptests
Since we use only `frama-c` which is native of byte when available:
- remove: if frama-c is called add the options
- remove: add PTESTS_FILE if it is not present
Adds variables to replace without hurdles:
- @FRAMA_C_PLUGINS_OPTIONS@: -autoload-plugins -plugins ... -load-module ...
- @OPTIONS@: the OPT
- @frama-c@: frama-c @FRAMA_C_PLUGINS_OPTIONS@ @PTEST_FILE@ @OPTIONS@
---
ptests/ptests.ml | 94 +++++--------------
.../instantiate/tests/options/test_config | 2 +-
.../instantiate/tests/stdlib/test_config | 2 +-
.../instantiate/tests/string/test_config | 2 +-
.../markdown-report/tests/eva/test_config | 2 +-
.../tests/report/oracle/classify.0.res.oracle | 1 -
.../tests/report/oracle/classify.1.res.oracle | 1 -
.../tests/report/oracle/classify.2.res.oracle | 1 -
.../tests/report/oracle/classify.3.res.oracle | 1 -
.../tests/report/oracle/classify.4.res.oracle | 1 -
.../tests/report/oracle/classify.5.res.oracle | 1 -
tests/float/absorb.c | 4 +-
tests/journal/control.i | 10 +-
tests/journal/control2.c | 7 +-
tests/journal/intra.i | 2 +-
tests/journal/oracle/control2.res.oracle | 10 +-
tests/journal/oracle/control2_sav.res | 10 +-
tests/libc/runtime.c | 4 +-
tests/misc/my_visitor.c | 2 +-
tests/pretty_printing/parenthesis.c | 2 +-
tests/pretty_printing/test_config | 2 +-
tests/slicing/select_by_annot.i | 4 +-
tests/sparecode/oracle/intra.2.res.oracle | 2 +-
tests/sparecode/oracle/top.0.res.oracle | 2 +-
tests/sparecode/oracle/top.2.res.oracle | 2 +-
tests/spec/anon_arg_2.i | 3 +-
tests/spec/clash_double_file_bts1598.c | 2 +-
tests/spec/rm_qualifiers.i | 2 +-
tests/syntax/multiple_decls_contracts.c | 1 +
.../multiple_decls_contracts.0.res.oracle | 4 +-
.../multiple_decls_contracts.1.res.oracle | 4 +-
.../multiple_decls_contracts.2.res.oracle | 4 +-
.../typedef_incorrect_pretty_print_bts1518.i | 2 +-
33 files changed, 72 insertions(+), 121 deletions(-)
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 7cc8be13f10..210aa2dde3b 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 abee799913e..b594387946c 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 f3094d70de0..401dafb99f4 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 f3094d70de0..401dafb99f4 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 b9757b17913..c7be0c1d592 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 30ccea3bc06..ebfe0669fdd 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 0453ac2ee2d..92c49e08c37 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 7238c685a85..8b5f49e7c15 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 11079f58648..6568ac0a7d9 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 b4438b9bfb5..e43f8970349 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 d126b08201d..39e627312c3 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 7d284ad6cb7..7a9e3cab596 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 7611474cf1e..0830044b07e 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 674aeb4609c..4271c1d25dd 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 cadfe3ac742..3ece0a57f2b 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 92d19a0804c..02360dafcbc 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 fbebf504547..1734f9bb537 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 ca77f67fa82..8c3522845b4 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 03f2242c110..52aecdc0066 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 fc923fe3d27..9e25bb53be7 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 25d5f233dbc..f5d302bd1d2 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 1a70a1cd5ad..5e40c065648 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 47d7d4b3d04..0a930fe52d1 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 c078269a008..f6425c3ba77 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 6dc821c49b5..600c507df79 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 80197a9b0f7..fad55c929f4 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 f3340e93f69..37446ed82f5 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 d6d739b95cc..a8f58e6e666 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 1b32185cfe8..11e4ec84626 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 49e36a7bc96..4b4eb643785 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 50638f1cb54..c56b7c7de43 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 364dd1fa5a6..15c98417a22 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 6ea6db2214d..e9e92214c8c 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 */
--
GitLab