diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 91c8e28c36120e62de749eac8174f2c34f15399a..2489c968a1927c694a9065eb189fe51d7caf914d 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -990,6 +990,15 @@ file, run it only once.
test
& \textit{None}
\\
+& \texttt{TIMEOUT}\nscodeidxdef{Test!Directive}{TIMEOUT}
+& kill the test after the given duration and report a failure
+& \textit{None}
+\\
+& \texttt{NOFRAMAC}\nscodeidxdef{Test!Directive}{NOFRAMAC}
+& empty the list of frama-c commands to be launched
+(\texttt{EXEC} and \texttt{EXECNOW} directives are still executed).
+& \textit{None}
+\\
\hline \multirow{2}{23mm}{\centering{Test suite}}
& \texttt{DONTRUN}\nscodeidxdef{Test!Directive}{DONTRUN}
& Do not execute this test
@@ -1017,11 +1026,17 @@ test
Any directive can identify a file using a relative path.
The default directory considered for \texttt{.} is always the parent
directory of directory \texttt{tests}\codeidx{tests}. The
-\texttt{DONTRUN} directive does not need to have any content, but it
-is useful to provide an explanation of why the test should not be run
-({\it e.g} test of a feature that is currently developed and not fully
+\texttt{DONTRUN} and \texttt{NOFRAMAC} directives
+do not need to have any content, but it might be
+useful to provide an explanation of why the test should not be run
+({\it e.g} test of a feature that is under development and not fully
operational yet).
+If there are \texttt{OPT}/\texttt{STDOPT} directives \textit{after} a
+\texttt{NOFRAMAC} directive, they will be executed, unless
+they are themselves discarded by another subsequent \texttt{NOFRAMAC}
+directive.
+
As said in Section~\ref{ptests:configuration}, these directives can be
found in different places:
\begin{enumerate}
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index 8abcd5df6a1cd67926d25c5ce1f67f9767945b43..2230467a8ad62f1b5512330c647279b02c6a2b70 100644
--- a/doc/developer/changes.tex
+++ b/doc/developer/changes.tex
@@ -5,6 +5,12 @@
This chapter summarizes the major changes in this documentation between each
\framac release, from newest to oldest.
+\section*{Frama-C+dev}
+\begin{itemize}
+\item \textbf{Testing}: Document new directives \texttt{TIMEOUT} and
+\texttt{NOFRAMAC}
+\end{itemize}
+
\section*{21.0 Scandium}
\begin{itemize}
\item \textbf{Configure}: Documentation of \texttt{configure\_pkg},
@@ -13,13 +19,13 @@ This chapter summarizes the major changes in this documentation between each
\section*{20.0 Calcium}
\begin{itemize}
-\item \textbf{Ptests}: Documentation of the new directive \texttt{MODULE}.
+\item \textbf{Testing}: Documentation of the new directive \texttt{MODULE}.
\end{itemize}
\section*{19.0 Potassium}
\begin{itemize}
\item \textbf{ACSL Extension}: Document new \texttt{status} flag for registration functions
-\item \textbf{Testing}: Document of usage \texttt{@@} in a directive
+\item \textbf{Testing}: Document usage of \texttt{@@} in a directive
\item \textbf{Profiling with Landmarks}: New section
\end{itemize}
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index 457004dd0a5643c0c65fbd40384b55d8085f3e9c..93fb2b73b8082593784f4a27498f584285773672 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -548,11 +548,11 @@ For this tutorial, there will be no such source code. A file
\texttt{./tests/hello/hello\_test.c} is then created:
\listingname{./tests/hello/hello\_test.c}
-\sscodeidx{Test}{Directive}{OPT}
+\nscodeidx{Test!Directive}{OPT}
\lstinputlisting[style=c]{./tutorial/hello/generated/with_test/tests/hello/hello_test.c}
In this file, there is only one directive
-\texttt{OPT: -hello}\sscodeidx{Test}{Directive}{OPT} which requires
+\texttt{OPT: -hello}\nscodeidx{Test!Directive}{OPT} which requires
to run \framac on this test with the \texttt{-hello} option.
A look at Section~\ref{ptests:directives} gives you an idea of the kind of
directives which can be used to test plug-ins.
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 3202933a25a1a124dc0eda2ae77bae5763a43943..36fb036537e47b8837d792debbd2cbf28806d5d0 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -600,6 +600,7 @@ type config =
(** toplevel full path, options to launch the toplevel on, and list
of output files to monitor beyond stdout and stderr. *)
dc_dont_run : bool;
+ dc_framac : bool;
dc_default_log: string list;
dc_timeout: string
}
@@ -619,6 +620,7 @@ let default_config () =
dc_default_toplevel = !toplevel_path;
dc_toplevels = [ !toplevel_path, default_options, [], Macros.empty, "" ];
dc_dont_run = false;
+ dc_framac = true;
dc_default_log = [];
dc_timeout = "";
}
@@ -802,6 +804,8 @@ let config_options =
{ current with dc_default_log = s :: current.dc_default_log });
"TIMEOUT",
(fun _ s current -> { current with dc_timeout = s });
+ "NOFRAMAC",
+ (fun _ _ current -> { current with dc_toplevels = []; dc_framac = false; });
]
let scan_options dir scan_buffer default =
@@ -835,11 +839,16 @@ let scan_options dir scan_buffer default =
with
End_of_file ->
(match !r.dc_toplevels with
- | [] -> { !r with dc_toplevels = default.dc_toplevels }
+ | [] 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 is_config name =
+ let prefix = "run.config" in
+ let len = String.length prefix in
+ String.length name >= len && String.sub name 0 len = prefix
+
let scan_test_file default dir f =
let f = SubDir.make_file dir f in
let exists_as_file =
@@ -864,9 +873,10 @@ let scan_test_file default dir f =
scan_options dir scan_buffer default
else (* config name does not match: eat config and continue.
But only if the comment is still opened by the end of
- the line...
+ the line and we are indeed reading a config
*)
- (if not (str_string_match end_comment names 0) then
+ (if List.exists is_config configs &&
+ not (str_string_match end_comment names 0) then
ignore (scan_options dir scan_buffer default);
scan_config ()))
in
@@ -1349,6 +1359,7 @@ let do_command command =
if !verbosity >= 1 then begin
lock_printf "%% launch %s@." cmd;
end;
+ shared.summary_run <- succ shared.summary_run;
let r = launch cmd in
(* mark as already executed. For EXECNOW in test_config files,
other instances (for example another test of the same
diff --git a/src/plugins/e-acsl/tests/test_config_dev.in b/src/plugins/e-acsl/tests/test_config_dev.in
index b425a92ef845aa9c2b780656c0a153c19f48ee3b..5319ddedd5a6be13da2dc29af8cc3950e4f83913 100644
--- a/src/plugins/e-acsl/tests/test_config_dev.in
+++ b/src/plugins/e-acsl/tests/test_config_dev.in
@@ -1,3 +1,4 @@
+NOFRAMAC: only the EXEC command below is useful in this config
MACRO: SEDCMD @SEDCMD@
MACRO: DEST @PTEST_RESULT@/@PTEST_NAME@
MACRO: OUT @PTEST_NAME@.res.log
diff --git a/tests/fc_script/main.c b/tests/fc_script/main.c
index 74d57214aa95bddef791ede03759c1a863e371da..74219d5a7189f16ec2c67693fda369b891036493 100644
--- a/tests/fc_script/main.c
+++ b/tests/fc_script/main.c
@@ -1,5 +1,5 @@
/* run.config
- OPT:
+ NOFRAMAC: testing frama-c-script, not frama-c itself
EXECNOW: LOG GNUmakefile LOG make_template.res LOG make_template.err PTESTS_TESTING= bin/frama-c-script make-template @PTEST_DIR@/result < @PTEST_DIR@/make_template.input > @PTEST_DIR@/result/make_template.res 2> @PTEST_DIR@/result/make_template.err
EXECNOW: LOG list_files.res LOG list_files.err bin/frama-c-script list-files @PTEST_DIR@/list_files.json > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err
EXECNOW: LOG flamegraph.html LOG flamegraph.res LOG flamegraph.err NOGUI=1 bin/frama-c-script flamegraph @PTEST_DIR@/flamegraph.txt @PTEST_DIR@/result > @PTEST_DIR@/result/flamegraph.res 2> @PTEST_DIR@/result/flamegraph.err && rm -f @PTEST_DIR@/result/flamegraph.svg
diff --git a/tests/fc_script/oracle/main.res.oracle b/tests/fc_script/oracle/main.res.oracle
deleted file mode 100644
index b704da034a4c3d0c18098123a35deebfdc11adb9..0000000000000000000000000000000000000000
--- a/tests/fc_script/oracle/main.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/fc_script/main.c (with preprocessing)