diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index d6dceaa1bf73026c3a1f3f6ba952b3c59e8b5504..76c7992b5973dc2c528fe850425104d52621f427 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -745,7 +745,7 @@ occurs currently in the following cases:
\begin{example}
Test \texttt{tests/sparecode/calls.c} declares the following directives.
- \sscodeidx{Test}{Directive}{OPT}
+ \nscodeidx{Test!Directive}{OPT}
\begin{listing-nonumber}
/* run.config
OPT: -sparecode-analysis
@@ -895,54 +895,59 @@ the configuration header of a test (or a test suite).
\textbf{Kind} & \textbf{Name} & \textbf{Specification} & \textbf{default}\\
\hline
\hline \multirow{4}{23mm}{\centering{Command}}
-& \texttt{CMD}\sscodeidxdef{Test}{Directive}{CMD}
+& \texttt{CMD}\nscodeidxdef{Test!Directive}{CMD}
& Program to run
& \texttt{./bin/toplevel.opt}
\\
-& \texttt{OPT}\sscodeidxdef{Test}{Directive}{OPT}
+& \texttt{OPT}\nscodeidxdef{Test!Directive}{OPT}
& Options given to the program
& \texttt{-val -out -input -deps}
\\
-& \texttt{STDOPT}\sscodeidxdef{Test}{Directive}{STDOPT}
+& \texttt{STDOPT}\nscodeidxdef{Test!Directive}{STDOPT}
& Add and remove options from the default set
& \textit{None}
\\
-& \texttt{LOG}\sscodeidxdef{Test}{Directive}{LOG}
+& \texttt{LOG}\nscodeidxdef{Test!Directive}{LOG}
& Add an additional file to compare against an oracle
& \textit{None}
\\
-& \texttt{EXECNOW}\sscodeidxdef{Test}{Directive}{EXECNOW}
+& \texttt{EXECNOW}\nscodeidxdef{Test!Directive}{EXECNOW}
& Run a command before the following commands. When specified in a configuration
file, run it only once.
& \textit{None}
\\
-& \texttt{EXEC}\sscodeidxdef{Test}{Directive}{EXEC}
+& \texttt{EXEC}\nscodeidxdef{Test!Directive}{EXEC}
& Similar to \texttt{EXECNOW}, but run it once per testing file.
& \textit{None}
\\
-& \texttt{MACRO}\sscodeidxdef{Test}{Directive}{MACRO}
+& \texttt{MACRO}\nscodeidxdef{Test!Directive}{MACRO}
& Define a new macro
& \textit{None}
\\
-& \texttt{FILTER}\sscodeidxdef{Test}{Directive}{FILTER}
+& \texttt{FILTER}\nscodeidxdef{Test!Directive}{FILTER}
& Command used to filter results
& \textit{None}
\\
+& \texttt{MODULE}\nscodeidxdef{Test!Directive}{MODULE}
+& Register a dynamic module to be built and to be loaded with each subsequent
+test
+& \textit{None}
+\\
\hline \multirow{2}{23mm}{\centering{Test suite}}
-& \texttt{DONTRUN}\sscodeidxdef{Test}{Directive}{DONTRUN}
+& \texttt{DONTRUN}\nscodeidxdef{Test!Directive}{DONTRUN}
& Do not execute this test
& \textit{None}
\\
-& \texttt{FILEREG}\sscodeidxdef{Test}{Directive}{FILEREG}
+& \texttt{FILEREG}\nscodeidxdef{Test!Directive}{FILEREG}
& selects the files to test
& \texttt{.*\bss.\bss(c|i\bss)}
\\
\hline \multirow{2}{23mm}{\centering{Miscellaneous}}
-& \texttt{COMMENT}\sscodeidxdef{Test}{Directive}{COMMENT}
+& \texttt{COMMENT}\nscodeidxdef{Test!Directive}{COMMENT}
& Comment in the configuration
& \textit{None}
\\
-& \texttt{GCC}\sscodeidxdef{Test}{Directive}{GCC}
+& \texttt{GCC}\nscodeidxdef{Test!Directive}{GCC}
& Unused (compatibility only)
& \textit{None}
\\
@@ -988,12 +993,12 @@ the sequence above is read in order and defines a configuration level
\begin{itemize}
\item
- \texttt{CMD} allows to change the command that is used for the
+ \texttt{CMD} allows changing the command that is used for the
following \texttt{OPT} directives (until a new \texttt{CMD}
directive is found). No new test case is generated
if there is no further \texttt{OPT} directive. At a given
configuration level, the default value for directive
- \texttt{CMD}\sscodeidxdef{Test}{Directive}{CMD} is the last
+ \texttt{CMD}\nscodeidx{Test!Directive}{CMD} is the last
\texttt{CMD} directive of the preceding configuration level.
\item \texttt{LOG} adds a file to be compared against an oracle in the
next \texttt{OPT} directive. Several files can be monitored from a single
@@ -1007,7 +1012,7 @@ the sequence above is read in order and defines a configuration level
configuration level, they correspond to different test cases. The
\texttt{OPT} directive(s) of a given configuration level replace(s)
the ones of the preceding level.
-\item The \texttt{STDOPT}\sscodeidxdef{Test}{Directive}{STDOPT}
+\item The \texttt{STDOPT}\nscodeidx{Test!Directive}{STDOPT}
directive takes as default set of options
the last \texttt{OPT} directive(s) of the preceding configuration
level. If the preceding configuration level contains several
@@ -1025,8 +1030,8 @@ options). As with \texttt{OPT}, each \texttt{STDOPT} corresponds to a different
(set of) test case(s). \texttt{LOG} directives preceding an \texttt{STDOPT}
are taken into account.
\item The syntax for directives
- \texttt{EXECNOW}\sscodeidxdef{Test}{Directive}{EXECNOW}
- and \texttt{EXEC}\sscodeidxdef{Test}{Directive}{EXEC} is the following.
+ \texttt{EXECNOW}\nscodeidx{Test!Directive}{EXECNOW}
+ and \texttt{EXEC}\nscodeidxdef{Test!Directive}{EXEC} is the following.
\begin{code}
EXECNOW: [ [ LOG file | BIN file ] ... ] cmd
\end{code}
@@ -1052,7 +1057,7 @@ or
the command is put in a test configuration file:
\texttt{EXECNOW} executes the command only once for the test suite, while
\texttt{EXEC} executes it once per test file of the test suite.
-\item The \texttt{MACRO}\sscodeidxdef{Test}{Directive}{MACRO} directive
+\item The \texttt{MACRO}\nscodeidx{Test!Directive}{MACRO} directive
has the following syntax:
\begin{code}
MACRO: macro-name content
@@ -1063,8 +1068,15 @@ or
\texttt{@macro-name@} in a \texttt{CMD}, \texttt{LOG}, \texttt{OPT},
\texttt{STDOPT} or \texttt{EXECNOW} directive at this configuration level
or in any level below it will be replaced by \texttt{content}. Existing
- pre-defined macros are listed in section~\ref{sec:ptests-macros}.
-\item The \texttt{FILEREG}\sscodeidxdef{Test}{Directive}{FILEREG}
+ pre-defined macros are listed in section~\ref{sec:ptests-macros}.
+\item \texttt{MODULE}\nscodeidx{Test!Directive}{MODULE}
+ directive takes as argument the name of a \texttt{.cmxs}
+ module. It will then add a directive to compile this file with the
+ command \texttt{@PTEST\_MAKE\_MODULE@ <MODULE>} where
+ \texttt{@PTEST\_MAKE\_MODULE@} defaults to \texttt{make -s}. Option
+ \texttt{-load-module <MODULE>} will then be appended to any subsequent Frama-C
+ command triggered by the test.
+\item The \texttt{FILEREG}\nscodeidx{Test!Directive}{FILEREG}
directive contains a regular expression indicating which files in
the directory containing the current test suite are actually part of
the suite. This directive is only
diff --git a/doc/developer/macros.sty b/doc/developer/macros.sty
index bb199c65f158e989e393fe60dc336fbc1a9c5ee1..6a900ed9b7e46e3fa59deceef31ceba2c7a31d3b 100644
--- a/doc/developer/macros.sty
+++ b/doc/developer/macros.sty
@@ -30,7 +30,8 @@
\index{#1@\texttt{#1}!#2@\texttt{\fontsize{8}{10}\selectfont #2}|bfit}}
\newcommand{\sscodeidxdef}[3]{%
\index{#1@\texttt{#1}!#2@\texttt{#2}!#3@\texttt{#3}|bfit}}
-
+\newcommand{\nscodeidx}[2]{\index{#1!#2@\texttt{#2}}}
+\newcommand{\nscodeidxdef}[2]{\index{#1!#2@\texttt{#2}|bfit}}
\makeatletter
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index d99f688a4ac700f140617be5cb866a6d4711002d..79e513c75a36ad5d556520868c82ef411e778ad7 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -493,8 +493,6 @@ end = struct
end
-let macro_regex = Str.regexp "\\([^@]*\\)@\\([^@]*\\)@\\(.*\\)"
-
type execnow =
{
ex_cmd: string; (** command to launch *)
@@ -510,7 +508,77 @@ type execnow =
are duplicated using OCaml 'with' syntax. *)
}
-module StringMap = Map.Make(String)
+
+module Macros =
+struct
+ module StringMap = Map.Make (String)
+ open StringMap
+
+ type t = string StringMap.t
+
+ let empty = StringMap.empty
+
+ let macro_regex = Str.regexp "\\([^@]*\\)@\\([^@]*\\)@\\(.*\\)"
+
+ let does_expand macros s =
+ if !verbosity >=2 then begin
+ lock_printf "looking for macros in string %s\n%!" s;
+ lock_printf "Existing macros:\n%!";
+ iter (fun s1 s2 -> lock_printf "%s => %s\n%!" s1 s2) macros;
+ lock_printf "End macros\n%!";
+ end;
+ let rec aux n (ptest_file_matched,s as acc) =
+ if Str.string_match macro_regex s n then begin
+ let macro = Str.matched_group 2 s in
+ let ptest_file_matched = ptest_file_matched || macro = "PTEST_FILE" in
+ let start = Str.matched_group 1 s in
+ let rest = Str.matched_group 3 s in
+ let new_n = Str.group_end 1 in
+ let n, new_s =
+ if macro = "" then begin
+ new_n + 1, String.sub s 0 new_n ^ "@" ^ rest
+ end else begin
+ try
+ if !verbosity >= 2 then lock_printf "macro is %s\n%!" macro;
+ let replacement = find macro macros in
+ if !verbosity >= 1 then
+ lock_printf "replacement for %s is %s\n%!" macro replacement;
+ new_n,
+ String.sub s 0 n ^ start ^ replacement ^ rest
+ with
+ | Not_found -> Str.group_end 2 + 1, s
+ end
+ in
+ if !verbosity >= 2 then lock_printf "new string is %s\n%!" new_s;
+ let new_acc = ptest_file_matched, new_s in
+ if n <= String.length new_s then aux n new_acc else new_acc
+ end else acc
+ in
+ Mutex.lock str_mutex;
+ try
+ let res = aux 0 (false,s) in
+ Mutex.unlock str_mutex; res
+ with e ->
+ lock_eprintf "Uncaught exception %s\n%!" (Printexc.to_string e);
+ Mutex.unlock str_mutex;
+ raise e
+
+ let expand macros s =
+ snd (does_expand macros s)
+
+ let get ?(default="") name macros =
+ try find name macros with Not_found -> default
+
+ let add_list l map =
+ List.fold_left (fun acc (k,v) -> add k v acc) map l
+
+ let add_expand name def macros =
+ add name (expand macros def) macros
+
+ let append_expand name def macros =
+ add name (get name macros ^ expand macros def) macros
+end
+
(** configuration of a directory/test. *)
type config =
@@ -519,7 +587,7 @@ type config =
dc_execnow : execnow list; (** command to be launched before
the toplevel(s)
*)
- dc_macros: string StringMap.t; (** existing macros. *)
+ dc_macros: Macros.t; (** existing macros. *)
dc_default_toplevel : string;
(** full path of the default toplevel. *)
dc_filter : string option; (** optional filter to apply to
@@ -532,7 +600,11 @@ type config =
}
let default_macros () =
- StringMap.add "frama-c" !toplevel_path StringMap.empty
+ let l = [
+ "frama-c", !toplevel_path;
+ "PTEST_MAKE_MODULE", "make -s"
+ ] in
+ Macros.add_list l Macros.empty
let default_config () =
{ dc_test_regexp = test_file_regexp ;
@@ -570,48 +642,6 @@ let launch command_string =
s command_string;
exit 1
-let replace_macros macros s =
- if !verbosity >=2 then begin
- lock_printf "looking for macros in string %s\n%!" s;
- lock_printf "Existing macros:\n%!";
- StringMap.iter (fun s1 s2 -> lock_printf "%s => %s\n%!" s1 s2) macros;
- lock_printf "End macros\n%!";
- end;
- let rec aux n (ptest_file_matched,s as acc) =
- if Str.string_match macro_regex s n then begin
- let macro = Str.matched_group 2 s in
- let ptest_file_matched = ptest_file_matched || macro = "PTEST_FILE" in
- let start = Str.matched_group 1 s in
- let rest = Str.matched_group 3 s in
- let new_n = Str.group_end 1 in
- let n, new_s =
- if macro = "" then begin
- new_n + 1, String.sub s 0 new_n ^ "@" ^ rest
- end else begin
- try
- if !verbosity >= 2 then lock_printf "macro is %s\n%!" macro;
- let replacement = StringMap.find macro macros in
- if !verbosity >= 1 then
- lock_printf "replacement for %s is %s\n%!" macro replacement;
- new_n,
- String.sub s 0 n ^ start ^ replacement ^ rest
- with
- | Not_found -> Str.group_end 2 + 1, s
- end
- in
- if !verbosity >= 2 then lock_printf "new string is %s\n%!" new_s;
- let new_acc = ptest_file_matched, new_s in
- if n <= String.length new_s then aux n new_acc else new_acc
- end else acc
- in
- Mutex.lock str_mutex;
- try
- let res = aux 0 (false,s) in
- Mutex.unlock str_mutex; res
- with e ->
- lock_eprintf "Uncaught exception %s\n%!" (Printexc.to_string e);
- Mutex.unlock str_mutex;
- raise e
let scan_execnow ~once dir (s:string) =
let rec aux (s:execnow) =
@@ -675,7 +705,12 @@ let make_custom_opts =
(* preserve options ordering *)
List.fold_right (fun x s -> s ^ " " ^ x) opts ""
-let add_macro s macros =
+
+(* how to process options *)
+let config_exec ~once dir s current =
+ { current with dc_execnow = scan_execnow ~once dir s :: current.dc_execnow }
+
+let config_macro _dir s current =
let regex = Str.regexp "[ \t]*\\([^ \t@]+\\)\\([ \t]+\\(.*\\)\\|$\\)" in
Mutex.lock str_mutex;
if Str.string_match regex s 0 then begin
@@ -686,14 +721,20 @@ let add_macro s macros =
Mutex.unlock str_mutex;
if !verbosity >= 1 then
lock_printf "new macro %s with definition %s\n%!" name def;
- StringMap.add name (snd (replace_macros macros def)) macros
+ { current with dc_macros = Macros.add_expand name def current.dc_macros }
end else begin
Mutex.unlock str_mutex;
lock_eprintf "cannot understand MACRO definition: %s\n%!" s;
- macros
+ current
end
-(* how to process options *)
+let config_module dir s current =
+ let make_cmd = "@PTEST_MAKE_MODULE@ " ^ s in
+ let make_cmd = Macros.expand current.dc_macros make_cmd in
+ let current = config_exec ~once:true dir make_cmd current in
+ let k = "PTEST_LOAD_MODULES" and v = " -load-module " ^ s in
+ { current with dc_macros = Macros.append_expand k v current.dc_macros }
+
let config_options =
[ "CMD",
(fun _ s current ->
@@ -733,21 +774,14 @@ let config_options =
"DONTRUN",
(fun _ s current -> { current with dc_dont_run = true });
- "EXECNOW",
- (fun dir s current ->
- let execnow = scan_execnow ~once:true dir s in
- { current with dc_execnow = execnow::current.dc_execnow });
-
- "EXEC",
- (fun dir s current ->
- let execnow = scan_execnow ~once:false dir s in
- { current with dc_execnow = execnow::current.dc_execnow });
-
- "MACRO", (fun _ s current ->
- { current with dc_macros = add_macro s current.dc_macros });
+ "EXECNOW", config_exec ~once:true;
+ "EXEC", config_exec ~once:false;
+ "MACRO", config_macro;
+ "MODULE", config_module;
"LOG",
(fun _ s current ->
{ current with dc_default_log = s :: current.dc_default_log })
+
]
let scan_options dir scan_buffer default =
@@ -825,7 +859,7 @@ let scan_test_file default dir f =
{ default with dc_dont_run = true }
type toplevel_command =
- { macros: string StringMap.t;
+ { macros: Macros.t;
mutable log_files: string list;
file : string ;
nb_files : int ;
@@ -934,9 +968,7 @@ let get_macros cmd =
"PTEST_NUMBER", string_of_int cmd.n;
]
in
- List.fold_left
- (fun acc (macro,replace) -> StringMap.add macro replace acc)
- cmd.macros macros
+ Macros.add_list macros cmd.macros
let basic_command_string =
let contains_toplevel_or_frama_c =
@@ -944,22 +976,19 @@ let basic_command_string =
in
fun command ->
let macros = get_macros command in
- let logfiles =
- List.fold_left
- (fun acc s -> snd (replace_macros macros s) :: acc)
- []
- command.log_files
- in
+ let logfiles = List.map (Macros.expand macros) command.log_files in
command.log_files <- logfiles;
- let has_ptest_file_t, toplevel = replace_macros macros command.toplevel in
- let has_ptest_file_o, options = replace_macros macros command.options in
+ 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 options =
if str_string_match contains_toplevel_or_frama_c command.toplevel 0
then begin
- let opt_pre = snd (replace_macros macros !additional_options_pre) in
- let opt_post = snd (replace_macros macros !additional_options) in
- "-check " ^ opt_pre ^ " " ^ options ^ " " ^ opt_post
+ let opt_modules = Macros.expand macros
+ (Macros.get "PTEST_LOAD_MODULES" macros) in
+ let opt_pre = Macros.expand macros !additional_options_pre in
+ let opt_post = Macros.expand macros !additional_options in
+ "-check " ^ opt_modules ^ " " ^ opt_pre ^ " " ^ options ^ " " ^ opt_post
end else options
in
let options = if !use_byte then opt_to_byte_options options else options in
@@ -1083,11 +1112,7 @@ let update_toplevel_command command =
Unix.Unix_error _ -> ()
end;
let macros = get_macros command in
- let log_files =
- List.fold_left
- (fun acc s -> snd (replace_macros macros s) :: acc)
- []
- command.log_files
+ let log_files = List.map (Macros.expand macros) command.log_files
in
List.iter (update_log_files command.directory) log_files
@@ -1605,7 +1630,7 @@ let dispatcher () =
macros = config.dc_macros;
execnow = true; }
in
- let process_macros s = snd (replace_macros config.dc_macros s) in
+ let process_macros s = Macros.expand config.dc_macros s in
let make_execnow_cmd execnow =
let res =
{
diff --git a/tests/misc/behavior_names.i b/tests/misc/behavior_names.i
index d4e48cb5bf64a0462aa4b9196b3d1dd23f533b9a..20a66a894482270937c3af919cdc95bcc68f1a90 100644
--- a/tests/misc/behavior_names.i
+++ b/tests/misc/behavior_names.i
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -no-autoload-plugins
*/
/*@ behavior foo: ensures \true; */
diff --git a/tests/misc/debug_category.i b/tests/misc/debug_category.i
index 4773466c671722c22fdb1b53992f6073349b9383..5646776c8be6e08df7545b9b872b067995932fa5 100644
--- a/tests/misc/debug_category.i
+++ b/tests/misc/debug_category.i
@@ -1,21 +1,21 @@
/* run.config
-EXECNOW: make -s tests/misc/Debug_category.cmxs
-OPT: -load-module tests/misc/Debug_category.cmxs -test-msg-key help -test-warn-key="a=inactive"
-OPT: -load-module tests/misc/Debug_category.cmxs -test-msg-key a -test-warn-key="a=inactive"
-OPT: -load-module tests/misc/Debug_category.cmxs -test-msg-key a -test-msg-key="-a:b" -test-warn-key="a=inactive"
-OPT: -load-module tests/misc/Debug_category.cmxs -test-msg-key a -test-msg-key="-a:b" -test-msg-key a:b:c -test-warn-key="a=inactive"
-OPT: -load-module tests/misc/Debug_category.cmxs -test-msg-key "a:b:c,d" -test-warn-key="a=inactive"
-OPT: -load-module tests/misc/Debug_category.cmxs -test-msg-key "*" -test-warn-key="a=inactive"
-OPT: -load-module tests/misc/Debug_category.cmxs
-OPT: -load-module tests/misc/Debug_category.cmxs -test-warn-key a=error
-OPT: -load-module tests/misc/Debug_category.cmxs -test-warn-key a=abort
-OPT: -load-module tests/misc/Debug_category.cmxs -test-warn-key a=feedback
-OPT: -load-module tests/misc/Debug_category.cmxs -test-warn-key="*=abort"
-OPT: -load-module tests/misc/Debug_category.cmxs -test-warn-key=a=once
-OPT: -load-module tests/misc/Debug_category.cmxs -test-warn-key a=feedback-once
-OPT: -load-module tests/misc/Debug_category.cmxs -test-warn-key a=err-once
-OPT: -load-module tests/misc/Debug_category.cmxs -test-warn-key test-vis-err
-OPT: -load-module tests/misc/Debug_category.cmxs -test-warn-key test-inv-err
-OPT: -load-module tests/misc/Debug_category.cmxs -test-warn-key test-failure
+MODULE: tests/misc/Debug_category.cmxs
+OPT: -test-msg-key help -test-warn-key="a=inactive"
+OPT: -test-msg-key a -test-warn-key="a=inactive"
+OPT: -test-msg-key a -test-msg-key="-a:b" -test-warn-key="a=inactive"
+OPT: -test-msg-key a -test-msg-key="-a:b" -test-msg-key a:b:c -test-warn-key="a=inactive"
+OPT: -test-msg-key "a:b:c,d" -test-warn-key="a=inactive"
+OPT: -test-msg-key "*" -test-warn-key="a=inactive"
+OPT:
+OPT: -test-warn-key a=error
+OPT: -test-warn-key a=abort
+OPT: -test-warn-key a=feedback
+OPT: -test-warn-key="*=abort"
+OPT: -test-warn-key=a=once
+OPT: -test-warn-key a=feedback-once
+OPT: -test-warn-key a=err-once
+OPT: -test-warn-key test-vis-err
+OPT: -test-warn-key test-inv-err
+OPT: -test-warn-key test-failure
FILTER: sed 's|Your Frama-C version is.*|Your Frama-C version is VERSION|'
*/