Merge branch 'feature/ptests/noframac' into 'master'

Ptests enhancement: new directive NOFRAMAC and fix configuration scanning

Closes #848 and #916

See merge request frama-c/frama-c!2759

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}

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}
 

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.

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

src/plugins/e-acsl/tests/test_config_dev.in

+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

tests/fc_script/main.c

 /* 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

tests/fc_script/oracle/main.res.oracle

-[kernel] Parsing tests/fc_script/main.c (with preprocessing)