Merge branch 'fix/andre/ptests-doc' into 'master'

[Doc/Devman] Update ptests section in developer manual

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

doc/developer/advance.tex

@@ -612,6 +612,18 @@ A specific target \texttt{\$(PLUGIN\_NAME)\_TESTS} will specifically run the tes
 of the plugin. One can add new tests as dependencies of this target.
 The default tests are run by the target \texttt{\$(PLUGIN\_NAME)\_DEFAULT\_TESTS}.
 
+Additionally, when running \texttt{make tests} or
+\texttt{make \$(PLUGIN\_NAME)\_TESTS}
+it is possible to pass options to \texttt{ptests.opt} through the
+\texttt{PTESTS\_OPTS} variable.
+
+\begin{example}
+The following command will update the oracles of all tests of the Aoraï plug-in:
+\begin{shell}
+\$ make PTESTS_OPTS=-update Aorai_TESTS
+\end{shell}
+\end{example}
+
 \texttt{ptests.opt} runs tests belonging to a sub-directory 
 of directory \texttt{tests}\codeidx{tests} that is specified in
 \ptests configuration file. This configuration file,
@@ -709,37 +721,36 @@ There is exactly one directive by line. The different directives (\emph{i.e.}
 possibilities for \texttt{CONFIG\_OPTION}) are detailed in
 Section~\ref{ptests:directives}.
 
-\begin{important}
-Note that some specific configurations require dynamic linking, which
-is not available on all platforms for native code. {\tt ptests} takes
-care of reverting to bytecode when it detects that the {\tt OPT},
-{\tt EXECNOW}, or \texttt{EXEC} options of a test require dynamic linking. This
-occurs currently in the following cases:
-\begin{itemize}
-\item {\tt OPT} contains the option {\tt -load-script}
-\item {\tt OPT} contains the option {\tt -load-module}
-\item {\tt EXECNOW} and \texttt{EXEC} use {\tt make} to create a {\tt .cmxs}
-\end{itemize}
-\end{important}
-
 \begin{important}
   \textbf{Concurrency issues:}
   tests using compiled modules ({\tt -load-script} or {\tt -load-module}) may
   lead to concurrency issues when the same module is used in different test
   files, or in different test cases within the same file. One way to avoid
-  issues is to serialize tests via \texttt{EXECNOW} directives, e.g. by using
-  \texttt{make} to compile a \texttt{.cmxs} from the \texttt{.ml} file, and
-  then loading the \texttt{.cmxs} in the test cases, as in the example below.
+  issues is to serialize tests via \texttt{MODULE} directives, which will
+  take care of the compilation and of adding the corresponding
+  \texttt{-load-module} option to further \texttt{OPT} and
+  \texttt{STDOPT} directives:
 
   \begin{listing-nonumber}
-    EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-    STDOPT: #"-load-module @PTEST_DIR@/@PTEST_NAME.cmxs" ...
-    STDOPT: #"-load-module @PTEST_DIR@/@PTEST_NAME.cmxs" ...
+    MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+    STDOPT: +"-opt1" ...
+    STDOPT: #"-opt2" ...
   \end{listing-nonumber}
 
   In addition, if the same script {\tt tests/suite/script.ml}
-  is shared by several test files, the {\tt EXECNOW} directive should be put
-  into {\tt tests/suite/test\_config}.
+  is shared by several test files in {\tt tests/suite},
+  it is necessary to compile the script once
+  when entering the directory hosting the suite. The {\tt MODULE} directive is
+  not well suited for that, and it is thus needed to resort to an {\tt EXECNOW}
+  directive in {\tt tests/suite/test\_config}:
+
+  \begin{listing-nonumber}
+    EXECNOW: make -s @PTEST_DIR@/common_module.cmxs
+  \end{listing-nonumber}
+
+  It is then necessary to explicitly use
+  {\tt -load-module @PTEST\_DIR@/common\_module.cmxs} in the appropriate
+  {\tt OPT} and {\tt STDOPT} directives.
 
 \end{important}
 
@@ -832,9 +843,11 @@ Figure~\ref{fig:ptests-options} details the options of \ptests.
 & \texttt{-byte} & Use bytecode toplevel & no \\
 & \texttt{-opt} & Use native toplevel & yes \\
 & \texttt{-gui} & Use GUI instead of console-based toplevel & no \\
-\hline \multirow{4}{16mm}{\centering{Behavior}}
+\hline \multirow{5}{16mm}{\centering{Behavior}}
 & \texttt{-run} & Delete current results; run tests and examine results & yes
 \\
+& \texttt{-dry-run} & Print commands, but do not execute them & no
+\\
 & \texttt{-examine} & Only examine current results; do not run tests & no \\
 & \texttt{-show} & Run tests and show results, but do not examine
                    them; implies \texttt{-byte} &

doc/developer/architecture.tex

@@ -203,13 +203,6 @@ only possible one to define mutually dependent plug-ins while the third one
 (through module \texttt{Db}) is now fully deprecated even if most of the older
 \framac plug-ins are still defined this way.
 
-Plug-ins are usually dynamically linked when \framac is booting, even if some
-older \framac plug-ins are still statically linked. However it is still possible
-to statically link a dynamic plug-in if wanted or required. In particular,
-\ocaml does not support dynamic linking on some hardware
-architecture~\cite{caml}: in this case, you have to statically link all
-plug-ins.
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \section{Libraries}\label{archi:libraries}

doc/developer/examples/syntactic_check.ml

@@ -31,7 +31,7 @@ class non_zero_divisor prj = object (self)
   (* A division is an expression: we override the vexpr method *)
   method! vexpr e = match e.enode with
   | BinOp((Div|Mod), _, denom, _) ->
-    let logic_denom = Logic_utils.expr_to_term ~cast:true denom in
+    let logic_denom = Logic_utils.expr_to_term ~coerce:false denom in
     let assertion = Logic_const.prel (Rneq, logic_denom, Cil.lzero ()) in
     (* At this point, we have built the assertion we want to insert. It remains
        to attach it to the correct statement. The cil visitor maintains the
@@ -43,7 +43,7 @@ class non_zero_divisor prj = object (self)
       | Kglobal -> assert false
       | Kstmt s -> s
     in
-    let kf = Extlib.the self#current_kf in 
+    let kf = Extlib.the self#current_kf in
     (* The above statement and function are related to the original project. We
        need to attach the new assertion to the corresponding statement and
        function of the new project. Cil provides functions to convert a

ptests/ptests.ml

@@ -163,7 +163,7 @@ let unlink ?(silent = true) file =
     Unix.unlink file
   with
   | Unix_error _ when silent -> ()
-  | Unix_error (ENOENT,_,_) -> () (* Ignore "Not such file or directory" *)
+  | Unix_error (ENOENT,_,_) -> () (* Ignore "No such file or directory" *)
   | Unix_error _ as e -> output_unix_error e
 
 let is_file_empty_or_nonexisting filename =
@@ -338,7 +338,7 @@ let rec argspec =
     "-xunit", Arg.Set xunit,
     " Create a xUnit file named xunit.xml collecting results";
     "-error-code", Arg.Set do_error_code,
-    " Exit with error code 1 if tests failed (useful for scripts";
+    " Exit with error code 1 if tests failed (useful for scripts)";
   ]
 and help_msg () = Arg.usage (Arg.align argspec) umsg;;