diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index db1da3450701a754f0036a5e10e15ff392b7de37..7763e2d7650dbe7d97224e6c16ab0a0dd88b184f 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -949,18 +949,22 @@ Figure~\ref{fig:test-directives} shows all the directives that can be used in
the configuration header of a test (or a test suite).
\begin{figure}[ht]
\begin{center}
-\begin{tabular}{|c|c|p{5cm}|l|}
+\begin{tabular}{|c|c|p{4.5cm}|p{5.2cm}|}
\hline
\textbf{Kind} & \textbf{Name} & \textbf{Specification} & \textbf{default}\\
\hline
\hline \multirow{4}{23mm}{\centering{Command}}
+& \texttt{PLUGIN}\nscodeidxdef{Test!Directive}{PLUGIN}
+& Plugins to be loaded with each subsequent run.
+& \texttt{from inout eva scope variadic} for tests under \texttt{./tests} directory
+\\
& \texttt{CMD}\nscodeidxdef{Test!Directive}{CMD}
& Program to run
& \texttt{./bin/toplevel.opt}
\\
& \texttt{OPT}\nscodeidxdef{Test!Directive}{OPT}
& Options given to the program
-& \texttt{-val -out -input -deps}
+& \texttt{-val -out -input -deps} for tests under \texttt{./tests} directory
\\
& \texttt{STDOPT}\nscodeidxdef{Test!Directive}{STDOPT}
& Add and remove options from the default set
@@ -1015,7 +1019,7 @@ and report a failure
& selects the files to test
& \texttt{.*\bss.\bss(c|i\bss)}
\\
-\hline \multirow{2}{23mm}{\centering{Miscellaneous}}
+\hline \multirow{2}{23mm}{\centering{Misc.}}
& \texttt{COMMENT}\nscodeidxdef{Test!Directive}{COMMENT}
& Comment in the configuration
& \textit{None}
@@ -1175,9 +1179,9 @@ or
In such a directive, the predefined macro \texttt{@PTEST\_ORACLE@} is set to the
basename of the oracle.
That allows running a \texttt{diff} command with the oracle of another
- test configuration:
+ test configuration \texttt{config}:
\begin{code}
- FILTER: diff --new-file @PTEST_DIR@/oracle_configuration/@PTEST_ORACLE@ -
+FILTER: diff --new-file @PTEST_DIR@/oracle_config/@PTEST_ORACLE@ -
\end{code}
Chaining multiple filter commands is possible by defining several \texttt{FILTER} directives (they are applied in the reverse order),
and an empty command drops the previous \texttt{FILTER} directives.
diff --git a/doc/developer/architecture.tex b/doc/developer/architecture.tex
index 7e8c832343a31723a796df600c1139b011e25318..d1de7b6f1945e40f3c2ea63fde9aaae929508afb 100644
--- a/doc/developer/architecture.tex
+++ b/doc/developer/architecture.tex
@@ -48,9 +48,11 @@ documentation generated by \texttt{make doc} for that purpose.
\begin{figure}[htbp]
\begin{center}
-\begin{tikzpicture}[remember picture,scale=0.9, every node/.style={transform shape}]
+\begin{tikzpicture}[remember picture,every node/.style={transform shape}]
+\node (bottom) {
+\begin{tikz-hbox}[node distance=\bigpadding]{bottom}
% kernel internals
-\node[structural] (internals) {
+\node[structural,on chain] (internals) {
\tikztitleboxbig{Kernel Internals}{LightCyan}{
\begin{tikz-hbox}{internals}
\node[on chain,draw,plain]{parsing};
@@ -60,93 +62,22 @@ documentation generated by \texttt{make doc} for that purpose.
}
};
-\node[structural, above=\bigpadding] at (internals.north) (middle) {
- \begin{tikz-hbox}[node distance=\bigpadding]
- {middle}
- % kernel services
- \node[on chain, structural] (services) {
- \tikztitleboxbig{Kernel Services}{darkgreen}{
- \begin{tikz-hbox}{services}
- \node[on chain,structural]{
- \begin{tikz-vbox}{services-left}
- \node[on chain,structural] (traversal){
- \tikztitlebox{AST Traversal}{%
- \begin{tikz-vbox}{traversal}
- \node[on chain,draw,plain] (visitor) {visitor};
- \node[on chain,structural] {
- \begin{tikz-hbox}{traversal-1}
- \node[on chain,draw,plain] (analysis) {analysis};
- \node[on chain,draw,plain] (transfo) {ast\_transformations};
- \end{tikz-hbox}
- };
- \draw[-Latex] (analysis) -- (visitor);
- \draw[-Latex] (transfo) -- (visitor);
- \end{tikz-vbox}
- }
- };
- \node[on chain,structural] (ai) {
- \tikztitlebox{AI}{
- \begin{tikz-vbox}{ai}
- \node[on chain,draw,plain] {abstract\_interp};
- \end{tikz-vbox}
- }
- };
- \end{tikz-vbox}
- };
- \node[on chain,structural] {
- \begin{tikz-vbox}{services-right}
- \node[on chain,structural](ast){
- \tikztitlebox{ASTs}{%
- \begin{tikz-vbox}{ast}
- \node[on chain,draw,plain] (data) {ast\_data};
- \node[on chain,draw,plain] (queries) {ast\_queries};
- \node[on chain,draw,plain] (parsetree) {parsetree};
- \draw[-Latex] (queries) -- (data);
- \end{tikz-vbox}
- }
- };
- \node[on chain,structural] (interactions) {
- \tikztitlebox{Plug-in Interactions}{
- \begin{tikz-vbox}{plugin-api}
- \node[on chain,draw,plain] {cmdline\_parameters};
- \node[on chain,draw,plain] {plugin\_entry\_points};
- \end{tikz-vbox}
- }
- };
- \draw[bigarrow,<->] (ast.south) -- (interactions.north);
- \end{tikz-vbox}
- };
+% libraries
+\node[structural, on chain] (libraries) {%
+ \tikztitleboxbig{Libraries}{Orange}{
+ \begin{tikz-vbox}[node distance=\bigpadding]{libraries}
+ \node[on chain,draw,plain] (stdlib){stdlib};
+ \node[on chain,structural]{
+ \begin{tikz-hbox}{lib-middle}
+ \node[on chain,draw,plain] (datatype) {datatype};
+ \node[on chain,draw,plain] (project) {project};
\end{tikz-hbox}
- \begin{tikzpicture}[overlay]
- \coordinate (ai2) at ($(ai.north east)!.75!(ai.south east)$);
- \coordinate (traversal1) at
- ($(traversal.south east)!0.2!(traversal.south west)$);
- \coordinate (interactions1) at
- ($(interactions.north west)!0.2!(interactions.south west)$);
- \draw[bigarrow,->] (traversal.east) -- (ast.west);
- \draw[bigarrow,->] (traversal1) -- (interactions1);
- \draw[bigarrow,bend right,->] (ai.east) to[in=170] (ast.west);
- \draw[bigarrow,->] (ai.east) -- (interactions.west);
- \end{tikzpicture}
- }
- };
- %libraries
- \node[on chain, structural] (libraries) {%
- \tikztitleboxbig{Libraries}{Orange}{
- \begin{tikz-vbox}[node distance=\bigpadding]{libraries}
- \node[on chain,draw,plain] (stdlib){stdlib};
- \node[on chain,structural]{
- \begin{tikz-hbox}{lib-middle}
- \node[on chain,draw,plain] (datatype) {datatype};
- \node[on chain,draw,plain] (project) {project};
- \end{tikz-hbox}
- };
- \node[on chain,draw,plain] (utils) {utils};
- \end{tikz-vbox}%
- }
- };
- \draw[bigarrow,->] (services.east) -- (libraries.west);
- \end{tikz-hbox}
+ };
+ \node[on chain,draw,plain] (utils) {utils};
+ \end{tikz-vbox}%
+ }
+};
+\end{tikz-hbox}
\begin{tikzpicture}[overlay]
\draw[Latex-Latex] (stdlib.south) -- (datatype);
\draw[Latex-Latex] (datatype) -- (utils);
@@ -157,8 +88,76 @@ documentation generated by \texttt{make doc} for that purpose.
\end{tikzpicture}
};
+\node[structural, above=\bigpadding] at (bottom.north) (services) {
+ % kernel services
+ \tikztitleboxbig{Kernel Services}{darkgreen}{
+ \begin{tikz-hbox}{services}
+ \node[on chain,structural]{
+ \begin{tikz-vbox}{services-left}
+ \node[on chain,structural] (traversal){
+ \tikztitlebox{AST Traversal}{%
+ \begin{tikz-vbox}{traversal}
+ \node[on chain,draw,plain] (visitor) {visitor};
+ \node[on chain,structural] {
+ \begin{tikz-hbox}{traversal-1}
+ \node[on chain,draw,plain] (analysis) {analysis};
+ \node[on chain,draw,plain] (transfo) {ast\_transformations};
+ \end{tikz-hbox}
+ };
+ \draw[-Latex] (analysis) -- (visitor);
+ \draw[-Latex] (transfo) -- (visitor);
+ \end{tikz-vbox}
+ }
+ };
+ \node[on chain,structural] (ai) {
+ \tikztitlebox{AI}{
+ \begin{tikz-vbox}{ai}
+ \node[on chain,draw,plain] {abstract\_interp};
+ \end{tikz-vbox}
+ }
+ };
+ \end{tikz-vbox}
+ };
+ \node[on chain,structural] {
+ \begin{tikz-vbox}{services-right}
+ \node[on chain,structural](ast){
+ \tikztitlebox{ASTs}{%
+ \begin{tikz-vbox}{ast}
+ \node[on chain,draw,plain] (data) {ast\_data};
+ \node[on chain,draw,plain] (queries) {ast\_queries};
+ \node[on chain,draw,plain] (parsetree) {parsetree};
+ \draw[-Latex] (queries) -- (data);
+ \end{tikz-vbox}
+ }
+ };
+ \node[on chain,structural] (interactions) {
+ \tikztitlebox{Plug-in Interactions}{
+ \begin{tikz-vbox}{plugin-api}
+ \node[on chain,draw,plain] {cmdline\_parameters};
+ \node[on chain,draw,plain] {plugin\_entry\_points};
+ \end{tikz-vbox}
+ }
+ };
+ \draw[bigarrow,<->] (ast.south) -- (interactions.north);
+ \end{tikz-vbox}
+ };
+ \end{tikz-hbox}
+ \begin{tikzpicture}[overlay]
+ \coordinate (ai2) at ($(ai.north east)!.75!(ai.south east)$);
+ \coordinate (traversal1) at
+ ($(traversal.south east)!0.2!(traversal.south west)$);
+ \coordinate (interactions1) at
+ ($(interactions.north west)!0.2!(interactions.south west)$);
+ \draw[bigarrow,->] (traversal.east) -- (ast.west);
+ \draw[bigarrow,->] (traversal1) -- (interactions1);
+ \draw[bigarrow,bend right, ->] (ai.east) to[in=170] (ast.west);
+ \draw[bigarrow,->] (ai.east) -- (interactions.west);
+ \end{tikzpicture}
+ }
+};
+
%plugins
-\node[above=\bigpadding,structural] at (middle.north) (plugins) {
+\node[above=\bigpadding,structural] at (services.north) (plugins) {
\tikztitleboxbig{Plug-ins}{palered}{
\begin{tikz-hbox}{plugins}
\node[on chain,draw,plain] (pi1) {plug-in 1};
@@ -174,10 +173,11 @@ documentation generated by \texttt{make doc} for that purpose.
\end{tikz-hbox}
}
};
+
\draw[bigarrow,<->] (services.south) -- (internals.north);
- %TODO: understand why remembered nodes are not accurate.
- \draw[bigarrow,->] (plugins.south) -- ($(services.north)+(0,-28pt)$);
- \draw[bigarrow,->,bend right] (internals.east) to ($(libraries.south west)+(0,-5pt)$);
+ \draw[bigarrow,->] (plugins.south) -- (services.north);
+ \draw[bigarrow,->] (internals.east) -- (libraries.west);
+ \draw[bigarrow,->] (services.south) to (libraries.north);
\end{tikzpicture}
\caption{Frama-C Architecture Design.}\label{fig:architecture}
\end{center}
diff --git a/doc/developer/developer.tex b/doc/developer/developer.tex
index af1cae1b8bbc1809deaef9e64c559332154206f1..26c80c5c03c60cfee2b45abf3c31300abf7acb5e 100644
--- a/doc/developer/developer.tex
+++ b/doc/developer/developer.tex
@@ -4,7 +4,7 @@
%%MODERN \documentclass[a4paper,11pt,twoside,openright]{report}
\documentclass[web,svgnames]{frama-c-book}
-\usepackage{xspace,alltt,calc,multirow,tabularx,bigdelim}
+\usepackage{xspace,alltt,calc,multirow,tabularx,bigdelim,spverbatim}
\usepackage{amsmath}
\IfFileExists{diagbox.sty} % Compatibility with newer diagbox and older slashbox
{\usepackage{diagbox}
diff --git a/doc/developer/examples/syntactic_check.ml b/doc/developer/examples/syntactic_check.ml
index f99b0921fc07f060eabba009751658119adab29b..02350a04f73e7e2a1e810fa45987b5fbb1e04f1a 100644
--- a/doc/developer/examples/syntactic_check.ml
+++ b/doc/developer/examples/syntactic_check.ml
@@ -18,8 +18,8 @@ module M = Plugin.Register
(* Each annotation in Frama-C has an emitter, for traceability.
We create thus our own, and says that it will only be used to emit code
- annotations, and that these annotations do not depend on Frama-C's command
- line parameters.
+ annotations, and that these annotations do not depend
+ on Frama-C's command line parameters.
*)
let syntax_alarm =
Emitter.create
diff --git a/doc/developer/macros.sty b/doc/developer/macros.sty
index 5ffdaac2edd1bb37828ab23e18c696dbab0fef83..86469e96b81d7243fb571078f0fb284983601754 100644
--- a/doc/developer/macros.sty
+++ b/doc/developer/macros.sty
@@ -208,12 +208,14 @@ bigarrow/.style={thick,>=Latex,red}
start chain=#2 going below,
node distance=\padding,
every on chain/.style={rectangle},
+ remember picture,
#1]
}
{\end{tikzpicture}}
\newenvironment{tikz-hbox}[2][]
{\begin{tikzpicture}[
+ remember picture,
inner sep=0pt,
every node/.style={transform shape},
start chain=#2 going right,
@@ -223,7 +225,7 @@ bigarrow/.style={thick,>=Latex,red}
{\end{tikzpicture}}
\newcommand{\tikztitlebox}[3][]{%
-\begin{tikzpicture}[every node/.style={transform shape},#1,inner sep=0pt]
+\begin{tikzpicture}[every node/.style={transform shape},#1,inner sep=0pt,remember picture]
\node[structural] (#2-content) {#3};
\node[structural,above=\bigpaddelta,small-title] at (#2-content.north) (#2-title) {#2};
\node[fit=(#2-content) (#2-title),
@@ -231,11 +233,12 @@ bigarrow/.style={thick,>=Latex,red}
\end{tikzpicture}%
}
\newcommand{\tikztitleboxbig}[4][]{%
-\begin{tikzpicture}[inner sep=0pt,every node/.style={transform shape},#1]
-\node[structural] (#2-content) {#4};
-\node[above=1.5\bigpaddelta,big-title,structural] at (#2-content.north) (#2-title) {#2};
+\def\name{\detokenize{#2}}
+\begin{tikzpicture}[inner sep=0pt,every node/.style={transform shape},#1,remember picture]
+\node[structural] (\name-content) {#4};
+\node[above=1.5\bigpaddelta,big-title,structural,align=center] at (\name-content.north) (\name-title) {#2};
\begin{scope}[on background layer]
-\node[fit=(#2-content) (#2-title), fill=#3,
+\node[fit=(\name-content) (\name-title), fill=#3,
inner xsep=\padding, inner ysep=\bigpaddelta, draw, rounded corners=20pt,
outer sep=0pt] {};
\end{scope}
diff --git a/doc/developer/refman.tex b/doc/developer/refman.tex
index 2b6313b3054f87c4c3e786ea4006fd99b8dddc46..222fd58a7509a24fefe4b47c07ca1a06134bb1e5 100644
--- a/doc/developer/refman.tex
+++ b/doc/developer/refman.tex
@@ -185,10 +185,10 @@ generation/.style={-Latex,very thick,dashed,fill=none},
\node[on chain,opt,draw=black] (user) {.Makefile.user};
}
{[start chain=specific going right,node distance=\bigpaddelta]
- \node[on chain,plugin,draw=black,anchor=north east,yshift=-\largepadding]
- at (opt-begin.south east) { specific Makefile for plug-in 1 };
+ \node[on chain,plugin,draw=black,anchor=north east,xshift=-\largepadding,yshift=-\largepadding]
+ at (opt-begin.south east) {Makefile for plug-in 1 };
\node[on chain] {\ldots};
- \node[on chain,plugin,draw=black] {specific Makefile for plugin $n$};
+ \node[on chain,plugin,draw=black] {Makefile for plugin $n$};
}
\end{scope}
\matrix[anchor=north east,yshift=-\bigpadding,matrix of nodes,
@@ -225,7 +225,7 @@ Makefile $m_1$ is included in Makefile $m_2$
\draw[plugin,include,bend right] (generated.north west) to (makefile.north east);
\draw[generated,generation] (template) -- (generated);
\draw[kernel,include] (generated) -- (dynamic);
-\draw[plugin,include] (dynamic) -- (node cs:name=specific-begin,angle=10);
+\draw[plugin,include,bend left] (dynamic) to (node cs:name=specific-begin,angle=10);
\draw[plugin,include] (dynamic) -- (specific-end);
\draw[opt,include] (user) -- (makefile);
\draw[opt,include] (clean) -- (makefile);
@@ -842,7 +842,7 @@ to your needs. See \texttt{ocamlmerlin -help} for the list of flags.
Ptests pre-defines a certain number of macros for each test about to be run.
Figure~\ref{fig:ptests-macros} gives their definition.
\begin{figure}[htbp]
-\begin{tabular}{|p{3cm}|p{10cm}|}
+\begin{tabular}{|p{4.5cm}|p{10cm}|}
\hline
Name & Expansion \\
\hline
@@ -864,6 +864,31 @@ name of the current alternative configuration
fact two independent numbering schemes: one for \verb|EXECNOW| commands and
one for regular tests (if more than one \verb|OPT|).\\
\hline
+\verb|PTEST_RESULT| & shorthand alias to \verb|@PTEST_DIR@/result@PTEST_CONFIG@|
+(the result directory dedicated to the tested configuration)\\
+\hline
+\verb|PTEST_ORACLE| & basename of the current oracle file (macro only usable in FILTER directives)\\
+\hline
+\verb|PTEST_MODULE| & current list of module defined by the \verb|MODULE| directive\\
+\hline
+\verb|PTEST_PLUGIN| & current list of plugins defined by the \verb|PLUGIN| directive\\
+\hline
+\verb|PTEST_DEFAULT_OPTIONS| & the default option list: \verb|-journal-disable| \verb|-check| \verb|-no-autoload-plugins|\\
+\hline
+\verb|PTEST_LOAD_MODULE| & the \verb|-load-module| option related to the \verb|MODULE| directive\\
+\hline
+\verb|PTEST_LOAD_PLUGIN| & the \verb|-load-module| option related to the \verb|PLUGIN| directive\\
+\hline
+\verb|PTEST_LOAD_OPTIONS| & shorthand alias to \spverb|@PTEST_LOAD_PLUGIN@ @PTEST_LOAD_MODULE@|\\
+\hline
+\verb|PTEST_OPTIONS| & the current list of options related to \verb|OPT| and \verb|STDOPT| directives (for \verb|CMD| directives)\\
+\hline
+\verb|frama-c| & shortcut defined as follows: \spverb|@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@|\\
+\hline
+\verb|frama-c-cmd| & shortcut defined as follows: \spverb|@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@|\\
+\hline
+\verb|frama-c-exe| & set to the value of the \verb|TOPLEVEL_PATH| variable from \verb|./tests/ptests_config| file\\
+\hline
\end{tabular}
\caption{Predefined macros for ptests}\label{fig:ptests-macros}
\end{figure}
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index fa627601a68dcf5bf21d649ff493b4f1000290ff..832fee3fcc70f60857c2526e8fe0df54c365887e 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -109,7 +109,7 @@ platform. This tutorial focuses on specific parts of this figure.
\newlength{\captionheight}\settototalheight{\captionheight}{\captionbox}
\begin{tikzpicture}[remember picture,txt/.style={inner xsep=3pt}]
\node[inner sep=0pt] (implem) {
- \tikztitleboxbig{Plug-in implementation}{darkgreen}{
+ \tikztitleboxbig{Plug-in\\implementation}{darkgreen}{
\begin{tikz-vbox}{plugin-text}
\node[on chain, draw, txt,minimum height=\designheight](register){Register};
\node[on chain, draw, txt,minimum height=\designheight](options){Options};
@@ -556,12 +556,12 @@ directives which can be used to test plug-ins.
Once the \texttt{run.config} has been configured, it becomes possible to
get the output generated by the plug-in:
-\begin{shell}
+\begin{shell}[breaklines=true]
\$ ptests.opt -show
Env:
<...>
Command:
-/usr/local/bin/frama-c.byte tests/hello/hello_test.c -check -hello 2>tests/hello/result/hello_test.err.log >tests/hello/result/hello_test.res.log
+/usr/local/bin/frama-c.byte tests/hello/hello_test.c -check -hello 2>tests/hello/result/hello_test.err.log >tests/hello/result/hello_test.res.log
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/hello/hello_test.c (with preprocessing)
[hello] Hello, world!
@@ -610,7 +610,7 @@ Let's now assume the plug-in is later erroneously modified as follows:
where \texttt{Hello, world!} is incorrectly changed to \texttt{Hello world!}.
Running the command:
-\begin{shell}
+\begin{shell}[breaklines=true]
\$ make
<...>
\$ make tests
diff --git a/doc/frama-c-book.cls b/doc/frama-c-book.cls
index 2dce074dba3e88dfbdcbf4accf40649dc42ece9e..e2d476f9ae44f43b4c17f7d5099d33bb1fd0be9e 100644
--- a/doc/frama-c-book.cls
+++ b/doc/frama-c-book.cls
@@ -10,7 +10,6 @@
% --------------------------------------------------------------------------
\makeatletter
\RequirePackage{kvoptions}
-\RequirePackage{kvoptions-patch}
\SetupKeyvalOptions{
family=framacbook,
prefix=framacbook@,
@@ -18,7 +17,7 @@ prefix=framacbook@,
\RequirePackage{ifthen}
\DeclareVoidOption{web}{\PassOptionsToPackage{colorlinks,urlcolor=blue}{hyperref}}
\DeclareVoidOption{paper}{\PassOptionsToPackage{pdfborder=0 0 0}{hyperref}}
-\DeclareStringOption[{version=4.0,modifier=by-sa}]{license}
+\DeclareStringOption[{type=CC,version=4.0,modifier=by-sa}]{license}
\DeclareStringOption[english]{lang}
\DeclareDefaultOption{\PassOptionsToClass{\CurrentOption}{report}}
\PassOptionsToClass{a4paper,11pt,twoside,openright}{report}
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index e945f7923794f1bc819cbb5c5b36befa230546af..b8ac6adfa6d8d664e3dc23938619a1bca3348e7a 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -20,10 +20,6 @@
(* *)
(**************************************************************************)
-(** the options to launch the toplevel with if the test file is not
- annotated with test options *)
-let default_options = "-journal-disable -check"
-
let system =
if Sys.os_type = "Win32" then
fun f ->
@@ -195,24 +191,6 @@ let opt_to_byte_options =
let regex_cmxs = Str.regexp ("\\([^/]+\\)[.]cmxs\\($\\|[ \t]\\)") in
fun options -> str_global_replace regex_cmxs "\\1.cmo\\2" options
-let opt_to_byte cmd =
- 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
- in
- let cmdname, options = command_partition cmd in
- (opt_to_byte cmdname) ^ (opt_to_byte_options options)
-
let output_unix_error (exn : exn) =
match exn with
| Unix.Unix_error (error, _function, arg) ->
@@ -269,20 +247,11 @@ let do_cmp = ref (if Sys.os_type="Win32" then !do_diffs
else "cmp -s")
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
-let exclude_suites = ref []
-
-let exclude s = exclude_suites := s :: !exclude_suites
-
let xunit = ref false
let io_mutex = Mutex.create ()
@@ -294,71 +263,88 @@ let lock_fprintf f =
let lock_printf s = lock_fprintf Format.std_formatter s
let lock_eprintf s = lock_fprintf Format.err_formatter s
+let suites = ref []
let make_test_suite s =
suites := s :: !suites
+let exclude_suites = ref []
+let exclude s = exclude_suites := s :: !exclude_suites
+
+let macro_post_options = ref "" (* value set to @PTEST_POST_OPTIONS@ macro *)
+let macro_pre_options = ref "" (* value set to @PTEST_PRE_OPTIONS@ macro *)
+let macro_options = ref "@PTEST_PRE_OPTIONS@ @PTEST_OPT@ @PTEST_POST_OPTIONS@"
+let macro_default_options = ref "-journal-disable -check -no-autoload-plugins"
+
+let macro_frama_c_cmd = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@"
+let macro_frama_c = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@"
+let default_toplevel = ref "@frama-c@"
+
(* Those variables are read from a ptests_config file *)
+let toplevel_path = ref "" (* value set to @frama-c-exe@ macro *)
let default_suites = ref []
-let toplevel_path = ref ""
-
-let change_toplevel_to_gui () =
- let s = !toplevel_path in
- match string_del_suffix "toplevel.opt" s with
- | Some s -> toplevel_path := s ^ "viewer.opt"
- | None ->
- match string_del_suffix "toplevel.byte" s with
- | Some s -> toplevel_path := s ^ "viewer.byte"
- | None ->
- match string_del_suffix "frama-c" s with
- | Some s -> toplevel_path := s ^ "frama-c-gui"
- | None ->
- match string_del_suffix "frama-c.byte" s with
- | Some s -> toplevel_path := s ^ "frama-c-gui.byte"
- | None -> ()
-
let () =
- Unix.putenv "LC_ALL" "C" (* some oracles, especially in Jessie, depend on the
- locale *)
+ Unix.putenv "LC_ALL" "C" (* for oracles that depend on the locale *)
+
let example_msg =
Format.sprintf
"@.@[<v 0>\
A test suite can be the name of a directory in ./tests or \
the path to a file.@ @ \
Directives of \"test_config[_<mode>]\" files:@ \
- COMMENT: <comment> @[<v 0># Just a comment line.@]@ \
- FILEREG: <regexp> @[<v 0># Ignores the files in suites whose name doesn't matche the pattern.@]@ \
- DONTRUN: @[<v 0># Ignores the file.@]@ \
+ COMMENT: <comment> @[<v 0># Just a comment line.@]@ \
+ FILEREG: <regexp> @[<v 0># Ignores the files in suites whose name doesn't matche the pattern.@]@ \
+ DONTRUN: @[<v 0># Ignores the file.@]@ \
EXECNOW: ([LOG|BIN] <file>)+ <command> @[<v 0># Defines the command to execute to build a 'LOG' (textual) 'BIN' (binary) targets.@ \
# Note: the textual targets are compared to oracles.@]@ \
- MODULE: <module>... @[<v 0># Compile the module and adds the corresponding '-load-module' option to all sub-test commands.@]@ \
- LOG: <file>... @[<v 0># Defines targets built by the next sub-test command.@]@ \
- CMD: <command> @[<v 0># Defines the command to execute for all tests in order to get results to be compared to oracles.@]@ \
- OPT: <options> @[<v 0># Defines a sub-test using the 'CMD' definition: <command> <options>@]@ \
- STDOPT: +<extra> @[<v 0># Defines a sub-test and append the extra to the current option.@]@ \
- STDOPT: #<extra> @[<v 0># Defines a sub-test and prepend the extra to the current option.@]@ \
- EXIT: <number> @[<v 0># Defines the exit code required for the next sub-test commands.@]@ \
- FILTER: <cmd> @[<v 0># Performs a transformation on the test result files before the comparison from the oracles.@ \
+ MODULE: <module>... @[<v 0># Compile the module and set the @PTEST_MODULE@ macro@]@ \
+ PLUGIN: <plugin>... @[<v 0># Set the @PTEST_PLUGIN@ macro.@]@ \
+ LOG: <file>... @[<v 0># Defines targets built by the next sub-test command.@]@ \
+ CMD: <command> @[<v 0># Defines the command to execute for all tests in order to get results to be compared to oracles.@]@ \
+ OPT: <options> @[<v 0># Defines a sub-test using the 'CMD' definition: <command> <options>@]@ \
+ STDOPT: +<extra> @[<v 0># Defines a sub-test and append the extra to the current option.@]@ \
+ STDOPT: #<extra> @[<v 0># Defines a sub-test and prepend the extra to the current option.@]@ \
+ EXIT: <number> @[<v 0># Defines the exit code required for the next sub-test commands.@]@ \
+ FILTER: <cmd> @[<v 0># Performs a transformation on the test result files before the comparison from the oracles.@ \
# The oracle will be compared from the standard output of the command: cat <test-output-file> | <cmd> .@ \
# Chaining multiple filter commands is possible by defining several FILTER directives.@ \
# An empty command drops the previous FILTER directives.@ \
# Note: in such a command, the @@PTEST_ORACLE@@ macro is set to the basename of the oracle.@ \
# This allows running a 'diff' command with the oracle of another test configuration:@ \
# FILTER: diff --new-file @@PTEST_DIR@@/oracle_configuration/@@PTEST_ORACLE@@ @]@ \
- TIMEOUT: <delay> @[<v 0># Set a timeout for all sub-test.@]@ \
- NOFRAMAC: @[<v 0># Drops previous sub-test definitions and considers that there is no defined default sub-test.@]@ \
- GCC: @[<v 0># Deprecated.@]@ \
- MACRO: <name> <def> @[<v 0># Set a definition to the macro @@<name>@@.@]@ \
+ TIMEOUT: <delay> @[<v 0># Set a timeout for all sub-test.@]@ \
+ NOFRAMAC: @[<v 0># Drops previous sub-test definitions and considers that there is no defined default sub-test.@]@ \
+ GCC: @[<v 0># Deprecated.@]@ \
+ MACRO: <name> <def> @[<v 0># Set a definition to the macro @@<name>@@.@]@ \
+ @]@ \
+ @[<v 1>\
+ Default directive values:@ \
+ FILEREG: %s@ \
+ CMD: %s@ \
+ EXIT: 0@ \
@]@ \
@[<v 1>\
- Some predefined macros can be used in test commands:@ \
- @@PTEST_DIR@@ # Dirname of the test file.@ \
- @@PTEST_FILE@@ # Substituted by the test filename.@ \
- @@PTEST_NAME@@ # Basename of the test file.@ \
- @@PTEST_NUMBER@@ # Test command number.@ \
- @@PTEST_CONFIG@@ # Test configuration suffix.@ \
- @@PTEST_RESULT@@ # Shorthand alias to @@PTEST_DIR@@/result@@PTEST_CONFIG@@ (the result directory dedicated to the tested configuration).@ \
- @@PTEST_ORACLE@@ # Basename of the current oracle file (macro only usable in FILTER directives).@ \
+ Some predefined macros can be used in test commands:@ \
+ @@PTEST_DIR@@ # Dirname of the test file.@ \
+ @@PTEST_FILE@@ # Substituted by the test filename.@ \
+ @@PTEST_NAME@@ # Basename of the test file.@ \
+ @@PTEST_NUMBER@@ # Test command number.@ \
+ @@PTEST_CONFIG@@ # Test configuration suffix.@ \
+ @@PTEST_RESULT@@ # Shorthand alias to '@@PTEST_DIR@@/result@@PTEST_CONFIG@@' (the result directory dedicated to the tested configuration).@ \
+ @@PTEST_ORACLE@@ # Basename of the current oracle file (macro only usable in FILTER directives).@ \
+ @@PTEST_MODULE@@ # Current list of module defined by the MODULE directive.@ \
+ @@PTEST_PLUGIN@@ # Current list of plugins defined by the PLUGIN directive.@ \
+ @]@ \
+ Other macros can only be used in test commands (CMD and EXECNOW directives):@ \
+ @@PTEST_DEFAULT_OPTIONS@@ # The default option list: %s@ \
+ @@PTEST_LOAD_MODULE@@ # The '-load-module' option related to the MODULE directive.@ \
+ @@PTEST_LOAD_PLUGIN@@ # The '-load-module' option related to the PLUGIN directive.@ \
+ @@PTEST_LOAD_OPTIONS@@ # Shorthand alias to '@@PTEST_LOAD_PLUGIN@@ @@PTEST_LOAD_MODULE@@' .@ \
+ @@PTEST_OPTIONS@@ # The current list of options related to OPT and STDOPT directives (for CMD directives).@ \
+ @@frama-c@@ # Shortcut defined as follow: %s@ \
+ @@frama-c-cmd@@ # Shortcut defined as follow: %s@ \
+ @@frama-c-exe@@ # set to the value of the 'TOPLEVEL_PATH' variable from './tests/ptests_config' file.@ \
+ @]@ \
@[<v 1>\
Examples:@ \
ptests@ \
@@ -373,7 +359,11 @@ let example_msg =
ptests -v -j 1 \
# to check the time taken by each test\
@]@ @]"
-;;
+ test_file_regexp
+ !default_toplevel
+ !macro_default_options
+ !macro_frama_c
+ !macro_frama_c_cmd
let umsg = "Usage: ptests [options] [names of test suites]";;
@@ -419,13 +409,13 @@ 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,
+ "-add-options", Arg.Set_string macro_post_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,
+ "-add-options-pre", Arg.Set_string macro_pre_options,
"<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,
+ "-add-options-post", Arg.Set_string macro_post_options,
"Synonym of -add-options";
"-exclude", Arg.String exclude,
"<name> Exclude a test or a suite from the run";
@@ -535,7 +525,35 @@ let () =
end
(** Must be done after reading config *)
-let () = if !behavior = Gui then change_toplevel_to_gui ()
+let () =
+ if !use_byte then begin
+ match string_del_suffix "frama-c" !toplevel_path with
+ | Some path -> toplevel_path := path ^ "frama-c.byte"
+ | None ->
+ match string_del_suffix "toplevel.opt" !toplevel_path with
+ | Some path -> toplevel_path := path ^ "toplevel.byte"
+ | None ->
+ match string_del_suffix "frama-c-gui" !toplevel_path with
+ | Some path -> toplevel_path := path ^ "frama-c-gui.byte"
+ | None ->
+ match string_del_suffix "viewer.opt" !toplevel_path with
+ | Some path -> toplevel_path := path ^ "viewer.byte"
+ | None -> ()
+ end;
+ if !behavior = Gui then begin
+ match string_del_suffix "toplevel.opt" !toplevel_path with
+ | Some s -> toplevel_path := s ^ "viewer.opt"
+ | None ->
+ match string_del_suffix "toplevel.byte" !toplevel_path with
+ | Some s -> toplevel_path := s ^ "viewer.byte"
+ | None ->
+ match string_del_suffix "frama-c" !toplevel_path with
+ | Some s -> toplevel_path := s ^ "frama-c-gui"
+ | None ->
+ match string_del_suffix "frama-c.byte" !toplevel_path with
+ | Some s -> toplevel_path := s ^ "frama-c-gui.byte"
+ | None -> ()
+ end
(* redefine name if special configuration expected *)
let redefine_name name =
@@ -588,6 +606,12 @@ end = struct
end
+type does_expand = {
+ has_ptest_file : bool;
+ has_ptest_opt : bool;
+ has_frama_c_exe : bool;
+}
+
module Macros =
struct
module StringMap = Map.Make (String)
@@ -612,6 +636,9 @@ struct
let macro_regex = Str.regexp "@\\([-A-Za-z_0-9]+\\)@" in
fun macros s ->
let has_ptest_file = ref false in
+ let has_ptest_opt = ref false in
+ let has_ptest_options = ref false in
+ let has_frama_c_exe = ref false in
if !verbosity >= 3 then lock_printf "%% Expand: %s@." s;
if !verbosity >= 4 then print_macros macros;
let rec aux s =
@@ -621,9 +648,14 @@ struct
if Str.string_match macro_regex s 0 then begin
let macro = Str.matched_group 1 s in
try
+ (match macro with
+ | "PTEST_FILE" -> has_ptest_file := true
+ | "PTEST_OPT" -> has_ptest_opt := true
+ | "PTEST_OPTIONS" -> has_ptest_options := true
+ | "frama-c-exe" -> has_frama_c_exe := true
+ | _ -> ());
if !verbosity >= 4 then lock_printf "%% - macro is %s\n%!" macro;
let replacement = find macro macros in
- if String.(macro = "PTEST_FILE") then has_ptest_file := true;
if !verbosity >= 3 then
lock_printf "%% - replacement for %s is %s\n%!" macro replacement;
aux replacement
@@ -639,7 +671,10 @@ struct
let r = aux s in
Mutex.unlock str_mutex;
if !verbosity >= 3 then lock_printf "%% Expansion result: %s@." r;
- !has_ptest_file, r
+ { has_ptest_file= !has_ptest_file;
+ has_ptest_opt= !has_ptest_opt;
+ has_frama_c_exe= !has_frama_c_exe;
+ }, r
with e ->
lock_eprintf "Uncaught exception %s\n%!" (Printexc.to_string e);
Mutex.unlock str_mutex;
@@ -652,7 +687,10 @@ struct
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
+ List.fold_left (fun acc (k,v) ->
+ if !verbosity >= 3 then
+ lock_printf "%% - Adds macro %s with definition %s@." k v;
+ add k v acc) map l
let add_expand name def macros =
add name (expand macros def) macros
@@ -661,7 +699,6 @@ struct
add name (get name macros ^ expand macros def) macros
end
-
type execnow =
{
ex_cmd: string; (** command to launch *)
@@ -748,9 +785,16 @@ end = struct
let default_macros () =
let l = [
- "frama-c", !toplevel_path;
+ "frama-c-exe", !toplevel_path;
+ "frama-c-cmd", !macro_frama_c_cmd;
+ "frama-c", !macro_frama_c;
+ "PTEST_DEFAULT_OPTIONS", !macro_default_options;
+ "PTEST_OPTIONS", !macro_options;
+ "PTEST_PRE_OPTIONS", !macro_pre_options;
+ "PTEST_POST_OPTIONS", !macro_post_options;
"PTEST_MAKE_MODULE", "make -s";
- "PTEST_LOAD_MODULES", ""
+ "PTEST_MODULE", "";
+ "PTEST_PLUGIN", "";
]
in
Macros.add_list l Macros.empty
@@ -761,8 +805,8 @@ end = struct
dc_execnow = [];
dc_filter = None ;
dc_exit_code = None;
- dc_default_toplevel = !toplevel_path;
- dc_commands = [ { toplevel= !toplevel_path; opts=default_options; macros=Macros.empty; exit_code=None; logs= []; timeout= ""} ];
+ dc_default_toplevel = !default_toplevel;
+ dc_commands = [ { toplevel= !default_toplevel; opts=""; macros=Macros.empty; exit_code=None; logs= []; timeout= ""} ];
dc_dont_run = false;
dc_load_module = "";
dc_cmxs_module = StringSet.empty;
@@ -850,7 +894,6 @@ end = struct
(* preserve options ordering *)
List.fold_right (fun x s -> s ^ " " ^ x) opts ""
-
(* how to process options *)
let config_exec ~once ~file:_ dir s current =
{ current with
@@ -875,33 +918,51 @@ end = struct
current
end
- let set_load_modules deps macros =
- let name = "PTEST_LOAD_MODULES" in
- let def = String.concat "," deps in
- if !verbosity >= 3 then
- lock_printf "%% - Macro %s for -load-module with definition %s@." name def;
- Macros.add_list [name, def] macros
+ let update_module s =
+ "@PTEST_DIR@/" ^ (Filename.remove_extension s) ^ (if !use_byte then ".cmo" else ".cmxs")
let add_make_modules ~file dir deps current =
let deps,current = List.fold_left (fun ((deps,curr) as acc) s ->
+ let s = update_module s in
if StringSet.mem s curr.dc_cmxs_module then acc
else
- (s ^ " " ^ deps),
+ (deps ^ " " ^ s),
{ curr with dc_cmxs_module = StringSet.add s curr.dc_cmxs_module })
("",current) deps
in
if String.(deps = "") then current
- else
+ else begin
let make_cmd = Macros.expand current.dc_macros "@PTEST_MAKE_MODULE@" in
- config_exec ~once:true ~file dir (make_cmd ^ " " ^ deps) current
+ config_exec ~once:true ~file dir (make_cmd ^ deps) current
+ end
+
+ let update_module_macros modules macros =
+ let def = String.concat "," modules in
+ let load_def = if String.(def = "") then "" else
+ "-load-module=" ^ (String.concat "," (List.map update_module modules))
+ in
+ Macros.add_list [ "PTEST_MODULE", def ;
+ "PTEST_LOAD_MODULE", load_def ;
+ ] macros
let config_module ~file dir s current =
- let s = Macros.expand current.dc_macros s in
- let deps = List.map (fun s -> "@PTEST_DIR@/" ^ (Filename.remove_extension s) ^ ".cmxs")
- (str_split_list s)
+ let deps = str_split_list (Macros.expand current.dc_macros s) in
+ let current = { current with dc_macros = update_module_macros deps current.dc_macros } in
+ add_make_modules ~file dir deps current
+
+ let update_plugin_macros plugins macros =
+ let def = String.concat "," plugins in
+ let load_def = if String.(def = "") then "" else
+ (* the option "-load-plugin" will be used in a future version for PLUGIN *)
+ "-load-module=" ^ def
in
- let current = add_make_modules ~file dir deps current in
- { current with dc_macros = set_load_modules deps current.dc_macros }
+ Macros.add_list [ "PTEST_PLUGIN", def ;
+ "PTEST_LOAD_PLUGIN", load_def ;
+ ] macros
+
+ let config_plugins ~file dir s current =
+ let deps = str_split_list (Macros.expand current.dc_macros s) in
+ { current with dc_macros = update_plugin_macros deps current.dc_macros }
let config_options =
[ "CMD",
@@ -978,6 +1039,8 @@ end = struct
"MODULE", config_module;
+ "PLUGIN", config_plugins;
+
"LOG",
(fun ~file:_ _ s current -> { current with dc_default_log = s :: current.dc_default_log });
@@ -1217,21 +1280,49 @@ end = struct
try Filename.chop_extension cmd.file
with Invalid_argument _ -> cmd.file
in
+ let ptest_file = Filename.sanitize ptest_file in
+ let ptest_load_plugin = Macros.get "PTEST_LOAD_PLUGIN" cmd.macros in
+ let ptest_load_module = Macros.get "PTEST_LOAD_MODULE" cmd.macros in
let macros =
[ "PTEST_CONFIG", ptest_config;
"PTEST_DIR", SubDir.get cmd.directory;
"PTEST_RESULT",
SubDir.get cmd.directory ^ "/" ^ redefine_name "result";
- "PTEST_FILE", Filename.sanitize ptest_file;
+ "PTEST_FILE", ptest_file;
"PTEST_NAME", ptest_name;
"PTEST_NUMBER", string_of_int cmd.n;
+ "PTEST_OPT", cmd.options;
+ "PTEST_LOAD_OPTIONS", (String.concat " "
+ [ ptest_load_plugin ;
+ ptest_load_module ])
]
in
let macros = Macros.add_list macros cmd.macros in
let macros = Macros.add_defaults ~defaults macros in
let process_macros s = Macros.expand macros s in
+ let toplevel =
+ let in_toplevel,toplevel= Macros.does_expand macros cmd.toplevel in
+ if not cmd.execnow then begin
+ let has_ptest_file, options =
+ if in_toplevel.has_ptest_opt then in_toplevel.has_ptest_file, []
+ else
+ let in_option,options= Macros.does_expand macros cmd.options in
+ (in_option.has_ptest_file || in_toplevel.has_ptest_file),
+ (if in_toplevel.has_frama_c_exe then
+ [ process_macros "@PTEST_PRE_OPTIONS@" ;
+ options ;
+ process_macros "@PTEST_POST_OPTIONS@" ;
+ ]
+ else [ options ])
+ in
+ String.concat " " (toplevel::(if has_ptest_file then options else ptest_file::options))
+ end
+ else toplevel
+ in
{ cmd with
macros;
+ toplevel;
+ options = ""; (* no more usable *)
log_files = List.map process_macros cmd.log_files;
filter =
match cmd.filter with
@@ -1239,45 +1330,12 @@ end = struct
| Some filter -> Some (process_macros filter)
}
- let contains_frama_c_binary_name =
- Str.regexp "[^( ]*\\(toplevel\\|viewer\\|frama-c-gui\\|frama-c[^-]\\).*"
-
- let frama_c_binary_name =
- Str.regexp "\\([^ ]*\\(toplevel\\|viewer\\|frama-c-gui\\|frama-c\\)\\(\\.opt\\|\\.byte\\|\\.exe\\)?\\)"
-
let basic_command_string =
fun command ->
- let macros = command.macros 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 toplevel, contains_frama_c_binary =
- str_string_match_and_replace contains_frama_c_binary_name
- frama_c_binary_name ~suffix:" -check" toplevel
- in
- let options =
- if contains_frama_c_binary
- then begin
- let opt_modules = match Macros.expand macros
- (Macros.get "PTEST_LOAD_MODULES" macros) with
- | "" -> ""
- | s -> "-load-module=" ^ s ^ ""
- in
- let opt_pre = Macros.expand macros !additional_options_pre in
- let opt_post = Macros.expand macros !additional_options in
- 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
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
+ (* necessary until OPT are using direct -load-module option *)
+ if !use_byte then opt_to_byte_options command.toplevel
+ else command.toplevel
in
if command.timeout = "" then raw_command
else "ulimit -t " ^ command.timeout ^ " && " ^ raw_command
@@ -1521,12 +1579,7 @@ let do_command command =
if !behavior <> Examine && not (!(execnow.ex_done) && execnow.ex_once)
then begin
remove_execnow_results execnow;
- let cmd =
- if !use_byte then
- opt_to_byte execnow.ex_cmd
- else
- execnow.ex_cmd
- in
+ let cmd = execnow.ex_cmd in
if !verbosity >= 1 || !behavior = Show then begin
lock_printf "%% launch %s@." cmd;
end;
diff --git a/src/plugins/aorai/tests/test_config b/src/plugins/aorai/tests/test_config
index 68cdb87e735aee9026598e4f773117fd73492efd..c8feb6120b561b4eb45efc918a4a79b4f992de3d 100644
--- a/src/plugins/aorai/tests/test_config
+++ b/src/plugins/aorai/tests/test_config
@@ -1 +1,6 @@
+PLUGIN: aorai eva,from,scope report wp,rtegen
+
+COMMENT: work around to allow the loading of the aorai_test lib
+MACRO: PTEST_DEFAULT_OPTIONS -check -journal-disable
+
MACRO: PROVE_OPTIONS
diff --git a/src/plugins/aorai/tests/test_config_prove.in b/src/plugins/aorai/tests/test_config_prove.in
index 8875fe9a4de64611beee7a96c8a56fda2ff051ef..2e96488c0c4f976ca795877722a23d9fe8f139ef 100644
--- a/src/plugins/aorai/tests/test_config_prove.in
+++ b/src/plugins/aorai/tests/test_config_prove.in
@@ -1 +1,6 @@
+PLUGIN: aorai eva,from,scope report wp,rtegen
+
+COMMENT: work around to allow the loading of the aorai_test lib
+MACRO: PTEST_DEFAULT_OPTIONS -check -journal-disable
+
MACRO: PROVE_OPTIONS @AORAI_WP_SHARE@ -aorai-test-prove-aux-spec
diff --git a/src/plugins/e-acsl/tests/test_config_ci.in b/src/plugins/e-acsl/tests/test_config_ci.in
index 9b58fc5a4a9550952da1aaca405d6aec67e4899c..3f61a9a95f6c298c32d76b9bc59425a1aba9e566 100644
--- a/src/plugins/e-acsl/tests/test_config_ci.in
+++ b/src/plugins/e-acsl/tests/test_config_ci.in
@@ -1,9 +1,14 @@
MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
MACRO: MACHDEP -machdep gcc_x86_64
MACRO: GLOBAL @MACHDEP@ -remove-unused-specified-functions -verbose 0
+
MACRO: EACSL -e-acsl -e-acsl-share ./share/e-acsl -e-acsl-verbose 1
MACRO: EVA -eva -eva-no-alloc-returns-null -eva-no-results -eva-no-print -eva-warn-key libc:unsupported-spec=inactive
+
MACRO: EVENTUALLY -print -ocode @DEST@.c -load-script ./tests/print.cmxs
+
+PLUGIN: E_ACSL eva,scope,variadic rtegen
+
LOG: gen_@PTEST_NAME@.c
OPT: @GLOBAL@ @EACSL@ -then-last @EVA@ @EVENTUALLY@
FILTER:@SEDCMD@ -e "s|[a-zA-Z/\\]\+frama_c_project_e-acsl_[a-z0-9]*|PROJECT_FILE|" -e "s|$FRAMAC_SHARE|FRAMAC_SHARE|g" -e "s|../../share|FRAMAC_SHARE|g" -e "s|./share/e-acsl|FRAMAC_SHARE/e-acsl|g" -e "s|share/e-acsl|FRAMAC_SHARE/e-acsl|g"
diff --git a/src/plugins/e-acsl/tests/test_config_dev.in b/src/plugins/e-acsl/tests/test_config_dev.in
index 045e0fac2c994cb0d4fe5edc094ed3ddfb5b5a62..6c7b2aca44643307f328535feb302172ef21c182 100644
--- a/src/plugins/e-acsl/tests/test_config_dev.in
+++ b/src/plugins/e-acsl/tests/test_config_dev.in
@@ -12,7 +12,9 @@ MACRO: ROOT_EACSL_GCC_MISC_OPTS -q -X
COMMENT: Default options for the frama-c invocation
MACRO: ROOT_EACSL_GCC_FC_EXTRA -journal-disable -verbose 0
-EXEC: LOG @EACSL_ERR@ if test "@ROOT_EACSL_GCC_ENABLE@" = "yes"; then ./scripts/e-acsl-gcc.sh -I @frama-c@ -c @ROOT_EACSL_GCC_MISC_OPTS@ --frama-c-extra="@ROOT_EACSL_GCC_FC_EXTRA@ @ROOT_EACSL_GCC_FC_EXTRA_EXT@" @ROOT_EACSL_GCC_OPTS_EXT@ -o @DEST@.gcc.c -O @DEST@ @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl 2>&1 1>/dev/null | @ROOT_EACSL_EXEC_FILTER@ > @PTEST_RESULT@/@EACSL_ERR@; fi
+PLUGIN: E_ACSL eva,scope,variadic rtegen
+
+EXEC: LOG @EACSL_ERR@ if test "@ROOT_EACSL_GCC_ENABLE@" = "yes"; then ./scripts/e-acsl-gcc.sh -I @frama-c-exe@ -c @ROOT_EACSL_GCC_MISC_OPTS@ --frama-c-extra="@PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@ @ROOT_EACSL_GCC_FC_EXTRA@ @ROOT_EACSL_GCC_FC_EXTRA_EXT@" @ROOT_EACSL_GCC_OPTS_EXT@ -o @DEST@.gcc.c -O @DEST@ @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl 2>&1 1>/dev/null | @ROOT_EACSL_EXEC_FILTER@ > @PTEST_RESULT@/@EACSL_ERR@; fi
COMMENT: These next macros can be redefined in a test file
COMMENT: Define the following macro in a test to pass extra options to the frama-c invocation
diff --git a/src/plugins/instantiate/tests/test_config b/src/plugins/instantiate/tests/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..e76859ce46eb70cae21c0221ee19cde81dda11f4
--- /dev/null
+++ b/src/plugins/instantiate/tests/test_config
@@ -0,0 +1 @@
+PLUGIN: instantiate
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/with_value.i b/src/plugins/loop_analysis/tests/loop_analysis/with_value.i
index b030fa5e58dbcbe8a8d388fcc49097265f53ec38..66a5ec6025be62fb11852a4cd88c80cab1d764e4 100644
--- a/src/plugins/loop_analysis/tests/loop_analysis/with_value.i
+++ b/src/plugins/loop_analysis/tests/loop_analysis/with_value.i
@@ -1,7 +1,7 @@
/*run.config
-OPT: -no-autoload-plugins -load-module from,inout,loopanalysis,eva,scope -eva -eva-show-progress -then -loop
+PLUGIN: from,inout,loopanalysis,eva,scope
+OPT: -eva -eva-show-progress -then -loop
*/
-
void f1(int n) {
for (int i = 1; i < n+2; i++); // i IN [1..6] (6)
}
diff --git a/src/plugins/loop_analysis/tests/test_config b/src/plugins/loop_analysis/tests/test_config
index 4d0023c27475cdf9b242f862679fa8375c351218..f5a7fe2c3073d7012157044a16ee50637344ba4e 100644
--- a/src/plugins/loop_analysis/tests/test_config
+++ b/src/plugins/loop_analysis/tests/test_config
@@ -1 +1,2 @@
-OPT: -no-autoload-plugins -load-module loopanalysis -loop
+PLUGIN: loopanalysis
+OPT: -loop
diff --git a/src/plugins/markdown-report/tests/md/test_config b/src/plugins/markdown-report/tests/md/test_config
index 2d99fda9914fe40e3d6dad849ead724f9a88ec2e..a6de95a18b6e6ac762b8988ba15d90f1dd4ac8d4 100644
--- a/src/plugins/markdown-report/tests/md/test_config
+++ b/src/plugins/markdown-report/tests/md/test_config
@@ -1,2 +1,3 @@
+PLUGIN: eva,inout,scope markdown_report
CMD: @frama-c@ -eva @PTEST_FILE@ -mdr-gen md -mdr-date="now" -mdr-out @PTEST_DIR@/result/@PTEST_NAME@.@PTEST_NUMBER@.md
LOG: @PTEST_NAME@.@PTEST_NUMBER@.md
diff --git a/src/plugins/markdown-report/tests/sarif/cwe125.c b/src/plugins/markdown-report/tests/sarif/cwe125.c
index 4e3013719a1b91a9d99f904c7fc30fc044683df5..be4e873fb8849e996300279cb3406d967de04147 100644
--- a/src/plugins/markdown-report/tests/sarif/cwe125.c
+++ b/src/plugins/markdown-report/tests/sarif/cwe125.c
@@ -4,8 +4,8 @@ EXECNOW: LOG @PTEST_NAME@.parse.log @frama-c@ @PTEST_FILE@ -save @PTEST_DIR@/res
EXECNOW: LOG @PTEST_NAME@.eva.log @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@_parse.sav -eva -save @PTEST_DIR@/result/@PTEST_NAME@_eva.sav > @PTEST_DIR@/result/@PTEST_NAME@.eva.log
EXECNOW: LOG @PTEST_NAME@.sarif @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@_eva.sav -then -mdr-out @PTEST_DIR@/result/@PTEST_NAME@.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic
*/
-#include "__fc_builtin.h"
+#include "__fc_builtin.h"
#define LENGTH 10
int getValueFromArray(int *array, int len, int index) {
diff --git a/src/plugins/markdown-report/tests/sarif/libc.c b/src/plugins/markdown-report/tests/sarif/libc.c
index 2f7438beff35d307549bdbe6d896110fa98956c0..ebddde12484e96c3ce1921fe5432db3d83d87a5b 100644
--- a/src/plugins/markdown-report/tests/sarif/libc.c
+++ b/src/plugins/markdown-report/tests/sarif/libc.c
@@ -1,5 +1,5 @@
/* run.config
- CMD: @frama-c@ @PTEST_FILE@ -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic
+ CMD: @frama-c@ -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic
LOG: with-libc.sarif
OPT: -mdr-out @PTEST_DIR@/result/with-libc.sarif
LOG: without-libc.sarif
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
index 01038bb8a72d1d607ca386bebf1c5ed0289b8063..05cf14524c10a6fb740df19c593e92e62f0eb406 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
@@ -16,9 +16,11 @@
"invocations": [
{
"commandLine":
- "frama-c -check tests/sarif/cwe125.c -save tests/sarif/result/cwe125_parse.sav",
+ "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report tests/sarif/cwe125.c -save tests/sarif/result/cwe125_parse.sav",
"arguments": [
- "-check", "tests/sarif/cwe125.c", "-save",
+ "-journal-disable", "-check", "-no-autoload-plugins",
+ "-load-module=eva,from,scope,markdown_report",
+ "tests/sarif/cwe125.c", "-save",
"tests/sarif/result/cwe125_parse.sav"
],
"exitCode": 0,
@@ -26,21 +28,25 @@
},
{
"commandLine":
- "frama-c -check -load tests/sarif/result/cwe125_parse.sav -eva -save tests/sarif/result/cwe125_eva.sav",
+ "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report -load tests/sarif/result/cwe125_parse.sav -eva -save tests/sarif/result/cwe125_eva.sav",
"arguments": [
- "-check", "-load", "tests/sarif/result/cwe125_parse.sav", "-eva",
- "-save", "tests/sarif/result/cwe125_eva.sav"
+ "-journal-disable", "-check", "-no-autoload-plugins",
+ "-load-module=eva,from,scope,markdown_report", "-load",
+ "tests/sarif/result/cwe125_parse.sav", "-eva", "-save",
+ "tests/sarif/result/cwe125_eva.sav"
],
"exitCode": 0,
"executionSuccessful": true
},
{
"commandLine":
- "frama-c -check -load tests/sarif/result/cwe125_eva.sav -then -mdr-out tests/sarif/result/cwe125.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic",
+ "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report -load tests/sarif/result/cwe125_eva.sav -then -mdr-out tests/sarif/result/cwe125.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic",
"arguments": [
- "-check", "-load", "tests/sarif/result/cwe125_eva.sav", "-then",
- "-mdr-out", "tests/sarif/result/cwe125.sarif", "-mdr-gen",
- "sarif", "-mdr-no-print-libc", "-mdr-sarif-deterministic"
+ "-journal-disable", "-check", "-no-autoload-plugins",
+ "-load-module=eva,from,scope,markdown_report", "-load",
+ "tests/sarif/result/cwe125_eva.sav", "-then", "-mdr-out",
+ "tests/sarif/result/cwe125.sarif", "-mdr-gen", "sarif",
+ "-mdr-no-print-libc", "-mdr-sarif-deterministic"
],
"exitCode": 0,
"executionSuccessful": true
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
index 92989f9ff24ed46cd969d699cbe957a4e091c99f..09463aba3706bc50f7c4ddc224a7f773ee9389a6 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
@@ -16,9 +16,11 @@
"invocations": [
{
"commandLine":
- "frama-c -check tests/sarif/std_string.c -eva -then -mdr-sarif-deterministic -mdr-gen sarif -mdr-out tests/sarif/result/std_string.sarif",
+ "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report tests/sarif/std_string.c -eva -then -mdr-sarif-deterministic -mdr-gen sarif -mdr-out tests/sarif/result/std_string.sarif",
"arguments": [
- "-check", "tests/sarif/std_string.c", "-eva", "-then",
+ "-journal-disable", "-check", "-no-autoload-plugins",
+ "-load-module=eva,from,scope,markdown_report",
+ "tests/sarif/std_string.c", "-eva", "-then",
"-mdr-sarif-deterministic", "-mdr-gen", "sarif", "-mdr-out",
"tests/sarif/result/std_string.sarif"
],
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
index 2e65770160b67d52666d872c32c3ccff177cf6d1..1c47d708f582d55b6f2214609000909f832b3abe 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
@@ -16,12 +16,12 @@
"invocations": [
{
"commandLine":
- "frama-c -check tests/sarif/libc.c -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic -mdr-out tests/sarif/result/with-libc.sarif",
+ "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic tests/sarif/libc.c -mdr-out tests/sarif/result/with-libc.sarif",
"arguments": [
- "-check", "tests/sarif/libc.c", "-no-autoload-plugins",
- "-load-module", "eva,from,scope,markdown_report", "-eva",
+ "-journal-disable", "-check", "-no-autoload-plugins",
+ "-load-module=eva,from,scope,markdown_report", "-eva",
"-eva-no-results", "-mdr-gen", "sarif",
- "-mdr-sarif-deterministic", "-mdr-out",
+ "-mdr-sarif-deterministic", "tests/sarif/libc.c", "-mdr-out",
"tests/sarif/result/with-libc.sarif"
],
"exitCode": 0,
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif b/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
index b22b1bf8f4209a3f890c272cdee6d5470526ac48..0772f06e8dc221cd8bf486cbcd3a21702bf27055 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
@@ -16,12 +16,13 @@
"invocations": [
{
"commandLine":
- "frama-c -check tests/sarif/libc.c -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic -mdr-no-print-libc -mdr-out tests/sarif/result/without-libc.sarif",
+ "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic tests/sarif/libc.c -mdr-no-print-libc -mdr-out tests/sarif/result/without-libc.sarif",
"arguments": [
- "-check", "tests/sarif/libc.c", "-no-autoload-plugins",
- "-load-module", "eva,from,scope,markdown_report", "-eva",
+ "-journal-disable", "-check", "-no-autoload-plugins",
+ "-load-module=eva,from,scope,markdown_report", "-eva",
"-eva-no-results", "-mdr-gen", "sarif",
- "-mdr-sarif-deterministic", "-mdr-no-print-libc", "-mdr-out",
+ "-mdr-sarif-deterministic", "tests/sarif/libc.c",
+ "-mdr-no-print-libc", "-mdr-out",
"tests/sarif/result/without-libc.sarif"
],
"exitCode": 0,
diff --git a/src/plugins/markdown-report/tests/test_config b/src/plugins/markdown-report/tests/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..d8bce8de28a2aa935d226e8561a3097808500d60
--- /dev/null
+++ b/src/plugins/markdown-report/tests/test_config
@@ -0,0 +1 @@
+PLUGIN: eva,from,scope markdown_report
diff --git a/src/plugins/nonterm/tests/test_config b/src/plugins/nonterm/tests/test_config
index 91f0e5ec1ff948b34ba561fc9d7369be7fd38b87..521ad6d1a0c2ee0cdd8963bbf7f80c5a0f35f524 100644
--- a/src/plugins/nonterm/tests/test_config
+++ b/src/plugins/nonterm/tests/test_config
@@ -1 +1,2 @@
-OPT: -no-autoload-plugins -load-module from,inout,nonterm,scope -eva -eva-show-progress -eva-msg-key=-summary -then -nonterm -nonterm-verbose 2
+PLUGIN: from,inout,nonterm,scope
+OPT: -eva -eva-show-progress -eva-msg-key=-summary -then -nonterm -nonterm-verbose 2
diff --git a/src/plugins/report/tests/report/classify.c b/src/plugins/report/tests/report/classify.c
index 59d10572d66174086765df608e8473c6ad2c2f62..53068d1fb7a6bb272020cde4a7cf821693cf6e5b 100644
--- a/src/plugins/report/tests/report/classify.c
+++ b/src/plugins/report/tests/report/classify.c
@@ -1,5 +1,6 @@
/* run.config
- CMD: @frama-c@ -kernel-warn-key=annot-error=active -no-autoload-plugins -load-module wp,report -report-output @PTEST_RESULT@/classified.@PTEST_NUMBER@.json -wp -wp-msg-key shell
+ CMD: @frama-c@ -kernel-warn-key=annot-error=active -report-output @PTEST_RESULT@/classified.@PTEST_NUMBER@.json -wp -wp-msg-key shell
+PLUGIN: wp,rtegen,report
LOG: classified.@PTEST_NUMBER@.json
OPT: -wp-prover qed -report-unclassified-untried REVIEW -then -report-classify
EXIT: 1
@@ -18,7 +19,6 @@ EXIT: 1
int a ;
-
/*@
requires a >= 0 ;
ensures a > 0 ;
diff --git a/src/plugins/report/tests/report/csv.c b/src/plugins/report/tests/report/csv.c
index 536cfb432f2702af8035011868cad8ee785095d9..c9e27daea85800e65c791ee988974205ca027585 100644
--- a/src/plugins/report/tests/report/csv.c
+++ b/src/plugins/report/tests/report/csv.c
@@ -1,10 +1,10 @@
/* run.config
+PLUGIN: report from,inout,scope,eva
LOG: csv.csv
- OPT: -no-autoload-plugins -load-module from,inout,report,scope,eva -eva-warn-copy-indeterminate=-main4 -eva -eva-show-progress -eva-remove-redundant-alarms -eva-warn-key=alarm=inactive -then -report-csv @PTEST_RESULT@/csv.csv -report-no-proven -then -report-csv= -eva-warn-key=alarm -eva-slevel 1
+ OPT: -eva-warn-copy-indeterminate=-main4 -eva -eva-show-progress -eva-remove-redundant-alarms -eva-warn-key=alarm=inactive -then -report-csv @PTEST_RESULT@/csv.csv -report-no-proven -then -report-csv= -eva-warn-key=alarm -eva-slevel 1
COMMENT: first, do an analysis without any message, but check that the .csv is complete. Then, redo the analysis with value warnings. slevel 1 is just there to force Value to restart
*/
volatile v;
-
void main1(int x) {
int t[10];
int u[15];
diff --git a/src/plugins/report/tests/report/hyp.i b/src/plugins/report/tests/report/hyp.i
index e8181b82a7f38bea8a94a56acc0a8545eee610df..8c448f2f02063d8dfc837607137387266ff1841f 100644
--- a/src/plugins/report/tests/report/hyp.i
+++ b/src/plugins/report/tests/report/hyp.i
@@ -1,6 +1,6 @@
/* run.config
- OPT: -no-autoload-plugins -load-module report -load-script tests/report/one_hyp.ml
- OPT: -no-autoload-plugins -load-module report -load-script tests/report/several_hyps.ml
+ OPT: -load-script tests/report/one_hyp.ml
+ OPT: -load-script tests/report/several_hyps.ml
*/
void f(void);
diff --git a/src/plugins/report/tests/report/single.i b/src/plugins/report/tests/report/single.i
index 5f152e86922de3c4d21e6dd15371cf24d9b75e89..ee9b1b4359d8283a9ec3f48769c6e35c9462127d 100644
--- a/src/plugins/report/tests/report/single.i
+++ b/src/plugins/report/tests/report/single.i
@@ -1,7 +1,7 @@
/* run.config
- OPT: -no-autoload-plugins -load-module report -load-script tests/report/projectified_status.ml
- OPT: -no-autoload-plugins -load-module report -load-script tests/report/no_hyp.ml
- OPT: -no-autoload-plugins -load-module report -load-script tests/report/multi_emitters.ml
+ OPT: -load-script tests/report/projectified_status.ml
+ OPT: -load-script tests/report/no_hyp.ml
+ OPT: -load-script tests/report/multi_emitters.ml
*/
void main() {
diff --git a/src/plugins/report/tests/test_config b/src/plugins/report/tests/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..3c86d70370368197bb9b50d59a1557c9e37bf46a
--- /dev/null
+++ b/src/plugins/report/tests/test_config
@@ -0,0 +1 @@
+PLUGIN: report
diff --git a/src/plugins/server/tests/batch/test_config b/src/plugins/server/tests/batch/test_config
index 4addf96dff82842ab79ae170fda242244765a7c0..38b36108cbd35f2b835cf9811ca9d0af06f960ab 100644
--- a/src/plugins/server/tests/batch/test_config
+++ b/src/plugins/server/tests/batch/test_config
@@ -1,2 +1,3 @@
+PLUGIN: server
LOG: @PTEST_NAME@.out.json
-OPT: -no-autoload-plugins -load-module server -check -server-batch @PTEST_DIR@/@PTEST_NAME@.json -server-batch-output-dir @PTEST_RESULT@ -server-msg-key use-relative-filepath
+OPT: -server-batch @PTEST_DIR@/@PTEST_NAME@.json -server-batch-output-dir @PTEST_RESULT@ -server-msg-key use-relative-filepath
diff --git a/src/plugins/studia/tests/test_config b/src/plugins/studia/tests/test_config
index dc79c97068c8125cbff6a916b7fed6d7b881d5f2..75c01a81568f5bd37820738e9a6fffd25798a21f 100644
--- a/src/plugins/studia/tests/test_config
+++ b/src/plugins/studia/tests/test_config
@@ -1 +1,2 @@
+PLUGIN: eva,inout,deps
OPT: -eva -journal-disable -out -input -deps
diff --git a/src/plugins/variadic/tests/known/print_libc.c b/src/plugins/variadic/tests/known/print_libc.c
index 265018f2c74c6d406a2f0b2e28e6866fe3dc03af..a7df6ff263a8daff3f836fa14a1d98b4e2e585ea 100644
--- a/src/plugins/variadic/tests/known/print_libc.c
+++ b/src/plugins/variadic/tests/known/print_libc.c
@@ -1,6 +1,7 @@
/* run.config
+PLUGIN: variadic
LOG: print_libc.pretty.c
- OPT: @PTEST_DIR@/empty.c -no-autoload-plugins -load-module variadic -no-print-libc -print -ocode @PTEST_DIR@/result/@PTEST_NAME@.pretty.c -then @PTEST_DIR@/result/@PTEST_NAME@.pretty.c
+ OPT: @PTEST_DIR@/empty.c -no-print-libc -print -ocode @PTEST_DIR@/result/@PTEST_NAME@.pretty.c -then @PTEST_DIR@/result/@PTEST_NAME@.pretty.c
*/
#include <stdio.h>
diff --git a/src/plugins/variadic/tests/test_config b/src/plugins/variadic/tests/test_config
index e076935b23463006f8f89ffcddb93f7f2748c691..e93c90a92be816e38e26da50679fb9e4a0a0fcb7 100644
--- a/src/plugins/variadic/tests/test_config
+++ b/src/plugins/variadic/tests/test_config
@@ -1 +1,2 @@
-OPT: -no-autoload-plugins -load-module from,inout,eva,variadic,scope -check -print -kernel-verbose 0 -variadic-verbose 2 -eva -eva-slevel 10 -eva-msg-key=-initial-state,-summary -eva-no-show-progress -eva-print
+PLUGIN: variadic from,inout,eva,scope
+OPT: -print -kernel-verbose 0 -variadic-verbose 2 -eva -eva-slevel 10 -eva-msg-key=-initial-state,-summary -eva-no-show-progress -eva-print
diff --git a/src/plugins/wp/tests/test_config b/src/plugins/wp/tests/test_config
index 51675fdbc52d819cf3c99c4480b3130bd0fa64f3..122bc50aadc0af5e1a21b2b2baf4703d6955ef59 100644
--- a/src/plugins/wp/tests/test_config
+++ b/src/plugins/wp/tests/test_config
@@ -1,2 +1,3 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-prover none -wp-print -wp-share ./share -wp-msg-key shell -wp-warn-key "pedantic-assigns=inactive"
+PLUGIN: wp
+CMD: @frama-c@ -wp -wp-prover none -wp-print -wp-share ./share -wp-msg-key shell -wp-warn-key "pedantic-assigns=inactive"
OPT:
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index f5f56f99251f2a4100444ab7bb74b0abc2128e07..f0225eb3f9a0c31d90b77761394778c3a2268793 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,2 +1,3 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
+PLUGIN: wp
+CMD: @frama-c@ -wp -wp-par 1 -wp-share ./share -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
OPT:
diff --git a/src/plugins/wp/tests/wp_acsl/checks.i b/src/plugins/wp/tests/wp_acsl/checks.i
index f3fdcbfcab8f623e1c5393ae7e7b4b977300a6c2..c55cf4d5c8907db89f1cb70eb449041ace623a33 100644
--- a/src/plugins/wp/tests/wp_acsl/checks.i
+++ b/src/plugins/wp/tests/wp_acsl/checks.i
@@ -1,14 +1,14 @@
/* run.config
- OPT: -eva -load-module scope,eva,report -then -report
+PLUGIN: wp,rtegen,scope,eva,report
+ OPT: -then -eva -then -report
+PLUGIN: wp,rtegen
OPT: -wp-prop=@check
OPT: -wp-prop=-@check
*/
/* run.config_qualif
- OPT: -load-module report -wp-steps 5 -then -report
+PLUGIN: wp,rtegen,report
+ OPT: -wp-steps 5 -then -report
*/
-
-// note: eva and wp gives the same reporting
-
//@ axiomatic A { predicate P reads \nothing ; }
void main() {
//@check c1: P;
@@ -17,3 +17,4 @@ void main() {
//@assert a2: P;
;
}
+// note: eva and wp gives the same reporting
diff --git a/src/plugins/wp/tests/wp_manual/manual.i b/src/plugins/wp/tests/wp_manual/manual.i
index 11a04e0783ab7854b9dcb873766eaa739de19bfa..9f3afd5d3ae753eb86fa336712f033cf4b64a825 100644
--- a/src/plugins/wp/tests/wp_manual/manual.i
+++ b/src/plugins/wp/tests/wp_manual/manual.i
@@ -4,6 +4,7 @@
/* run.config_qualif
OPT: -wp-msg-key shell @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap1.h
OPT: -wp-msg-key shell -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h
- OPT: -load-module report -kernel-verbose 0 -wp-msg-key shell -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h -wp-verbose 0 -then -no-unicode -report
+PLUGIN: wp,rtegen,report
+ OPT: -kernel-verbose 0 -wp-msg-key shell -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h -wp-verbose 0 -then -no-unicode -report
*/
void look_at_working_dir(void);
diff --git a/src/plugins/wp/tests/wp_plugin/nosession.i b/src/plugins/wp/tests/wp_plugin/nosession.i
index bb038ffd831fcb13d4ecbfeeef7154c92d576820..d1873a1222997221ed75c281b72bb3663ce61eeb 100644
--- a/src/plugins/wp/tests/wp_plugin/nosession.i
+++ b/src/plugins/wp/tests/wp_plugin/nosession.i
@@ -1,9 +1,9 @@
/* run.config
DONTRUN:
*/
-
/* run.config_qualif
- CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp-share ./share -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive
+ CMD: @frama-c@ -wp-share ./share -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive
+PLUGIN: wp,rtegen
OPT: -wp -wp-prover alt-ergo -wp-session shall_not_exists_dir -wp-cache offline -wp-no-cache-env
COMMENT: The session directory shall not be created
*/
diff --git a/src/plugins/wp/tests/wp_plugin/removed.i b/src/plugins/wp/tests/wp_plugin/removed.i
index 9a4824f460e97fc22bacd03aae895c0e4c6147eb..08ad6804231703160d824e710dd98a9abfbc47f0 100644
--- a/src/plugins/wp/tests/wp_plugin/removed.i
+++ b/src/plugins/wp/tests/wp_plugin/removed.i
@@ -1,7 +1,7 @@
/* run.config_qualif
- OPT: -load-module eva,scope -no-wp -eva -eva-msg-key=-summary -then -wp -then -no-eva -warn-unsigned-overflow -wp
+PLUGIN: wp,rtegen,eva,scope
+ OPT: -no-wp -eva -eva-msg-key=-summary -then -wp -then -no-eva -warn-unsigned-overflow -wp
*/
-
/* run.config
DONTRUN:
*/
diff --git a/src/plugins/wp/tests/wp_region/test_config b/src/plugins/wp/tests/wp_region/test_config
index 57d4ae071a433f4d3cecca0d8a218c0557f02e6d..c85101d0b58d18ca145d6963a56e1163ad1a7a0e 100644
--- a/src/plugins/wp/tests/wp_region/test_config
+++ b/src/plugins/wp/tests/wp_region/test_config
@@ -1,3 +1,4 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp
+PLUGIN: wp,rtegen
+CMD: @frama-c@
LOG: @PTEST_NAME@/region/job.dot
OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-warn-key pedantic-assigns=inactive -wp-out @PTEST_DIR@/result/@PTEST_NAME@ -wp-fct job
diff --git a/src/plugins/wp/tests/wp_usage/save_load.i b/src/plugins/wp/tests/wp_usage/save_load.i
index 8e908e8b69636dbd586fb832035975253a0cb13f..72e3c2595a6d9d9bf219e0b22aa4cbe494b9cb4c 100644
--- a/src/plugins/wp/tests/wp_usage/save_load.i
+++ b/src/plugins/wp/tests/wp_usage/save_load.i
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: LOG save_load.sav.res LOG save_load.sav.err BIN @PTEST_NAME@.sav @frama-c@ -no-autoload-plugins -load-module wp -wp-warn-key pedantic-assigns=inactive -wp-share ./share -wp -wp-print -wp-prover none @PTEST_FILE@ -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@.sav.res 2> @PTEST_DIR@/result/@PTEST_NAME@.sav.err
- CMD: @frama-c@ -no-autoload-plugins -load-module wp -load @PTEST_DIR@/@PTEST_NAME@.sav -wp-warn-key pedantic-assigns=inactive
+ EXECNOW: LOG save_load.sav.res LOG save_load.sav.err BIN @PTEST_NAME@.sav @frama-c@ -wp-warn-key pedantic-assigns=inactive -wp-share ./share -wp -wp-print -wp-prover none @PTEST_FILE@ -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@.sav.res 2> @PTEST_DIR@/result/@PTEST_NAME@.sav.err
+ CMD: @frama-c@ -load @PTEST_DIR@/@PTEST_NAME@.sav -wp-warn-key pedantic-assigns=inactive
OPT: -print
OPT: -wp -wp-prover none -wp-print
*/
diff --git a/tests/builtins/big_local_array.i b/tests/builtins/big_local_array.i
index 83bb0fda45a32a5472b6aed4986d7fd80fa2cc0b..7c0854e14ae028bfb36a286b0aff0c94f6139784 100644
--- a/tests/builtins/big_local_array.i
+++ b/tests/builtins/big_local_array.i
@@ -1,7 +1,9 @@
/* run.config*
+ PLUGIN: @EVA_PLUGINS@ report
OPT: @EVA_OPTIONS@ -print -journal-disable -eva -report
MODULE: big_local_array_script
OPT: @EVA_OPTIONS@ -then-on prj -print -report
+ PLUGIN: @EVA_PLUGINS@
MODULE:
OPT: @EVA_OPTIONS@ -print -journal-disable -no-initialized-padding-locals -eva
*/
@@ -12,7 +14,7 @@ struct S {
};
int main () {
- struct S x[32] =
+ struct S x[32] =
{ [0] = { .a = { 1,2,3 }, .b = { [5] = 5, 6, 7 }},
[3] = { 0,1,2,3,.b = { [17]=17 } }
};
diff --git a/tests/builtins/test_config b/tests/builtins/test_config
index 365fdc8d48cbda0c83335a388b0cf9b0d7ceb848..0264f96531357bbcf6c3f754e378dae60f5d84b8 100644
--- a/tests/builtins/test_config
+++ b/tests/builtins/test_config
@@ -1,3 +1,4 @@
MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
-OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -out -input -deps
diff --git a/tests/callgraph/issue_55_iter_over_unregistered_function.i b/tests/callgraph/issue_55_iter_over_unregistered_function.i
index a39e29e042e8c876ef5338610289c83d56478cd0..535d2f3c5494e545651504c2b5e5e0bf88018e1c 100644
--- a/tests/callgraph/issue_55_iter_over_unregistered_function.i
+++ b/tests/callgraph/issue_55_iter_over_unregistered_function.i
@@ -1,8 +1,8 @@
/* run.config
+PLUGIN: @PTEST_PLUGIN@ eva,scope,inout
COMMENT: Test call to Callgraph.Uses.iter_on_callers/callees (through Inout)
OPT: -inout
*/
-
/*@ assigns *p \from x; */
extern void f(int x, int *p);
diff --git a/tests/callgraph/no_fp_unsound_warning.i b/tests/callgraph/no_fp_unsound_warning.i
index f841a6e1821b5c00be834118f3cd6a8594a9c59f..dcb0da94e41ae1c1c33a964b1015767b78cb163b 100644
--- a/tests/callgraph/no_fp_unsound_warning.i
+++ b/tests/callgraph/no_fp_unsound_warning.i
@@ -1,8 +1,8 @@
/* run.config
+PLUGIN: @PTEST_PLUGIN@ eva,scope,inout
COMMENT: Test that callgraph users are warned about -cg-no-function-pointers
OPT: -cg-function-pointers -out
OPT: -cg-no-function-pointers -out
*/
-
void main() {
}
diff --git a/tests/callgraph/test_config b/tests/callgraph/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..0757d9602b453e52bac8b869d4f07371c66d6a89
--- /dev/null
+++ b/tests/callgraph/test_config
@@ -0,0 +1,5 @@
+PLUGIN: callgraph
+STDOPT:
+
+# COMMENT: Directive to add in your test file when using STDOPT:
+# COMMENT: PLUGIN: @PTEST_PLUGIN@ @EVA_PLUGINS@
diff --git a/tests/compliance/test_config b/tests/compliance/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..2454128362a6b8b71db649b6d45f3baf2b6df496
--- /dev/null
+++ b/tests/compliance/test_config
@@ -0,0 +1 @@
+PLUGIN:
diff --git a/tests/constant_propagation/bts117.c b/tests/constant_propagation/bts117.c
index 420cd12e426c82096ca8e4d57efc742b1e5258c8..5d0662f5a3382c3daa5aa7ce45acb44717853194 100644
--- a/tests/constant_propagation/bts117.c
+++ b/tests/constant_propagation/bts117.c
@@ -1,9 +1,13 @@
/* run.config
-OPT: -journal-disable -print
-OPT: -journal-disable -semantic-const-folding @EVA_OPTIONS@
-OPT: -journal-disable -sparecode-analysis @EVA_OPTIONS@
+PLUGIN:
+ OPT: -print
+PLUGIN: @CONSTANT_PROPAGATION_PLUGINS@
+ OPT: -semantic-const-folding @EVA_OPTIONS@
+PLUGIN: @PTEST_PLUGIN@ sparecode
+ OPT: -sparecode-analysis @EVA_OPTIONS@
*/
+
int main1 (void) {
int r ;
if (1) r = 0; else r = 2;
@@ -15,6 +19,7 @@ int main2 (void){
if (r) r = 0; else r = 2;
return r;
}
+
int main (void) {
int x1 = main1();
int x2 = main2();
diff --git a/tests/constant_propagation/const_propagate.c b/tests/constant_propagation/const_propagate.c
index 064fee49c0ef0e892a9850a3d8acc80e410265bb..2e5e3f728eb889020c6c3f66a94155cfb7eecb2b 100644
--- a/tests/constant_propagation/const_propagate.c
+++ b/tests/constant_propagation/const_propagate.c
@@ -1,9 +1,9 @@
/* run.config
- OPT: -eva @EVA_OPTIONS@ -deps -out -input -scf -journal-disable
- OPT: -scf @EVA_OPTIONS@ -cast-from-constant -semantic-const-fold add3 -main init -journal-disable
+PLUGIN: @CONSTANT_PROPAGATION_PLUGINS@ from inout
+ OPT: -eva @EVA_OPTIONS@ -deps -out -input -scf
+ OPT: -scf @EVA_OPTIONS@ -main init -journal-disable -cast-from-constant -semantic-const-fold add3
*/
-int x,y,z;
-int TAB[10];
+int x,y,z, TAB[10];
struct st { int a, b ; } s1, s2;
typedef struct st ST ;
void test_struct (void) {
diff --git a/tests/constant_propagation/oracle/bts117.1.res.oracle b/tests/constant_propagation/oracle/bts117.1.res.oracle
index d496d1cea9692624bbb6b2c2f995932ef05c64d9..a918171fe0348838a78e2a483c3ee8dc38bc022a 100644
--- a/tests/constant_propagation/oracle/bts117.1.res.oracle
+++ b/tests/constant_propagation/oracle/bts117.1.res.oracle
@@ -6,11 +6,11 @@
[eva:initial-state] Values of globals at initialization
[eva] computing for function main1 <- main.
- Called from tests/constant_propagation/bts117.c:19.
+ Called from tests/constant_propagation/bts117.c:24.
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from tests/constant_propagation/bts117.c:20.
+ Called from tests/constant_propagation/bts117.c:25.
[eva] Recording results for main2
[eva] Done for function main2
[eva] Recording results for main
diff --git a/tests/constant_propagation/oracle/bts117.2.res.oracle b/tests/constant_propagation/oracle/bts117.2.res.oracle
index c4fe5b334c660df8b4797674fe3eb150bf073a10..493c47fa83c80699c7fe64a78162c6f389e49e39 100644
--- a/tests/constant_propagation/oracle/bts117.2.res.oracle
+++ b/tests/constant_propagation/oracle/bts117.2.res.oracle
@@ -6,11 +6,11 @@
[eva:initial-state] Values of globals at initialization
[eva] computing for function main1 <- main.
- Called from tests/constant_propagation/bts117.c:19.
+ Called from tests/constant_propagation/bts117.c:24.
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from tests/constant_propagation/bts117.c:20.
+ Called from tests/constant_propagation/bts117.c:25.
[eva] Recording results for main2
[eva] Done for function main2
[eva] Recording results for main
diff --git a/tests/constant_propagation/test_config b/tests/constant_propagation/test_config
index c9ce20f05d9b350fd5d065e1d08f26e53fc065b6..b3a8965ab1afefa926424d9f4730c5832a90b05a 100644
--- a/tests/constant_propagation/test_config
+++ b/tests/constant_propagation/test_config
@@ -1 +1,3 @@
+MACRO: CONSTANT_PROPAGATION_PLUGINS constant_propagation eva,scope
+PLUGIN: @CONSTANT_PROPAGATION_PLUGINS@
OPT: -journal-disable -scf @EVA_OPTIONS@ -machdep x86_32
diff --git a/tests/dynamic/test_config b/tests/dynamic/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..2454128362a6b8b71db649b6d45f3baf2b6df496
--- /dev/null
+++ b/tests/dynamic/test_config
@@ -0,0 +1 @@
+PLUGIN:
diff --git a/tests/float/absorb.c b/tests/float/absorb.c
index a71117b1674d5f6ba2b6dc97aeacd836c6f275cd..dbc2c9be16eb08e8623adacb43484cee5e14f4b2 100644
--- a/tests/float/absorb.c
+++ b/tests/float/absorb.c
@@ -1,16 +1,16 @@
/* run.config
COMMENT: run.config is intentionally not-*
- EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err FRAMAC_PLUGIN=tests/.empty @frama-c@ -journal-disable -save @PTEST_DIR@/result/absorb.sav @PTEST_FILE@ > @PTEST_DIR@/result/absorb_sav.res 2> @PTEST_DIR@/result/absorb_sav.err
- EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err @frama-c@ -load @PTEST_DIR@/result/absorb.sav -eva @EVA_CONFIG@ -journal-disable -float-hex -save @PTEST_DIR@/result/absorb.sav2 > @PTEST_DIR@/result/absorb_sav2.res 2> @PTEST_DIR@/result/absorb_sav2.err
+PLUGIN:
+ EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err @frama-c@ -save @PTEST_DIR@/result/absorb.sav @PTEST_FILE@ > @PTEST_DIR@/result/absorb_sav.res 2> @PTEST_DIR@/result/absorb_sav.err
+PLUGIN: @EVA_PLUGINS@
+ EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err @frama-c@ -load @PTEST_DIR@/result/absorb.sav -eva @EVA_CONFIG@ -float-hex -save @PTEST_DIR@/result/absorb.sav2 > @PTEST_DIR@/result/absorb_sav2.res 2> @PTEST_DIR@/result/absorb_sav2.err
OPT: -load @PTEST_DIR@/result/absorb.sav2 -deps -out -input
*/
/* run.config*
DONTRUN:
*/
#include "__fc_builtin.h"
-
float x = 1.0, y = 0.0, z, t, min_f, min_fl, den;
-
void main() {
long long b = Frama_C_interval(-2000000001, 2000000001);
b = b * b;
diff --git a/tests/impact/test_config b/tests/impact/test_config
index c449d18f602ef2fe815b38e0f2cdc3d467e1c815..953d2049ccde9dd0f40d5b3d195c5e3eb371b070 100644
--- a/tests/impact/test_config
+++ b/tests/impact/test_config
@@ -1 +1,2 @@
-OPT: -journal-disable -impact-print @EVA_OPTIONS@
+PLUGIN: @EVA_PLUGINS@ impact
+OPT: -impact-print @EVA_OPTIONS@
diff --git a/tests/jcdb/jcdb.c b/tests/jcdb/jcdb.c
index 13af9552975e857f6e062cd3068b82e98d9a33bd..c35dc80b7bfb0406a6653fcd8891cb2d7063b2a4 100644
--- a/tests/jcdb/jcdb.c
+++ b/tests/jcdb/jcdb.c
@@ -5,7 +5,7 @@
OPT: -json-compilation-database @PTEST_DIR@/with_arguments.json -no-autoload-plugins
MODULE:
EXECNOW: LOG list_files.res LOG list_files.err share/analysis-scripts/list_files.py @PTEST_DIR@/compile_commands_working.json > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err
- EXECNOW: LOG logic-pp-include.res LOG logic-pp-include.err @frama-c@ -json-compilation-database @PTEST_DIR@/logic-pp-include @PTEST_DIR@/logic-pp-include/no-stdio.c -print -no-autoload-plugins > @PTEST_DIR@/result/logic-pp-include.res 2> @PTEST_DIR@/result/logic-pp-include.err
+ EXECNOW: LOG logic-pp-include.res LOG logic-pp-include.err @frama-c@ -json-compilation-database @PTEST_DIR@/logic-pp-include @PTEST_DIR@/logic-pp-include/no-stdio.c -print > @PTEST_DIR@/result/logic-pp-include.res 2> @PTEST_DIR@/result/logic-pp-include.err
*/
#include <stdio.h>
diff --git a/tests/jcdb/test_config b/tests/jcdb/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..2454128362a6b8b71db649b6d45f3baf2b6df496
--- /dev/null
+++ b/tests/jcdb/test_config
@@ -0,0 +1 @@
+PLUGIN:
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
index 71676ee94fde86777dcac52dfb32ac462dbeba74..274b87c862bf5786beffcb180565eb82d3ddda93 100644
--- a/tests/journal/intra.i
+++ b/tests/journal/intra.i
@@ -1,5 +1,6 @@
/* run.config
- MODULE: @PTEST_NAME@
+ PLUGIN: @EVA_PLUGINS@ sparecode
+ MODULE: @PTEST_NAME@
EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -journal-enable -journal-name tests/journal/result/intra_journal.ml @PTEST_DIR@/@PTEST_NAME@.i > /dev/null 2> /dev/null
CMD: @frama-c@
OPT: -load-script tests/journal/result/intra_journal -journal-disable
@@ -12,7 +13,6 @@
* slicing analysis removes statement having variables with
* prefix "spare_" and "any_"
*/
-
int G;
int tmp (int a) {
diff --git a/tests/journal/test_config b/tests/journal/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..5b4e9a8bdd2b7dce5f1cd2d18923ecc5f7519b56
--- /dev/null
+++ b/tests/journal/test_config
@@ -0,0 +1,2 @@
+PLUGIN:
+STDOPT:
diff --git a/tests/libc/coverage.c b/tests/libc/coverage.c
index 342d79af62894d72d30d5a03c8e9c215baf37229..8f628572259c0844ff92bea687695c87757e4cd1 100644
--- a/tests/libc/coverage.c
+++ b/tests/libc/coverage.c
@@ -1,7 +1,7 @@
/* run.config*
+PLUGIN: @PTEST_PLUGIN@ metrics
OPT: -eva-no-builtins-auto @EVA_OPTIONS@ share/libc/string.c -eva -eva-slevel 6 -metrics-eva-cover -then -metrics-libc
*/
-
#include "string.h"
void main() {
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index a4bf6fc2786257dcf7d1e638573ac0698478a1a6..c222f77c8033529b9f07801298f9ab474d5dc783 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -1,6 +1,7 @@
/* run.config*
+ PLUGIN: @EVA_PLUGINS@ metrics
MODULE: check_libc_naming_conventions, check_const
- OPT: -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -load-module metrics -eva @EVA_CONFIG@ -then -lib-entry -no-print -metrics-no-libc
+ OPT: -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -eva @EVA_CONFIG@ -then -lib-entry -no-print -metrics-no-libc
MODULE:
OPT: -print -print-libc -machdep x86_32
MODULE: check_parsing_individual_headers
@@ -152,7 +153,6 @@
#include "utmpx.h"
#include "wchar.h"
#include "wctype.h"
-
void main() {
/* The variables below must be const; otherwise the preconditions
and the assigns/from of some functions will not match */
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 2cb4208b4b8543fdc33daf7ffb990420c03315a2..e52007ddeeca10602d81f5e6517071ed5aa43d5f 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -1,7 +1,4 @@
[kernel] Parsing tests/libc/fc_libc.c (with preprocessing)
-[kernel] :0: Warning: unnamed requires
-[kernel] share/libc/sys/socket.h:451: Warning:
- clause with '\initialized' must contain name 'initialization'
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -201,6 +198,9 @@
Function call = 98
Pointer dereferencing = 161
Cyclomatic complexity = 299
+[kernel] :0: Warning: unnamed requires
+[kernel] share/libc/sys/socket.h:451: Warning:
+ clause with '\initialized' must contain name 'initialization'
/* Generated by Frama-C */
#include "__fc_builtin.c"
#include "__fc_builtin.h"
diff --git a/tests/libc/test_config b/tests/libc/test_config
index cf5c5bb18359425ba47e530ac8c06c936f24d7e8..069a4888d38f81544d6797ecad65e1e1070e3198 100644
--- a/tests/libc/test_config
+++ b/tests/libc/test_config
@@ -1 +1,2 @@
+PLUGIN: @EVA_PLUGINS@
OPT: -eva @EVA_CONFIG@ -cpp-extra-args='-nostdinc -Ishare/libc'
diff --git a/tests/metrics/test_config b/tests/metrics/test_config
index de6ff0089d8e793cb118e41d7cf4db48f4dfd3d6..b528a2dd90282d3f8f7655c1da9554b390f84662 100644
--- a/tests/metrics/test_config
+++ b/tests/metrics/test_config
@@ -1 +1,2 @@
-OPT: -no-autoload-plugins -load-module metrics,scope -metrics
+PLUGIN: metrics,scope
+OPT: -metrics
diff --git a/tests/misc/audit.c b/tests/misc/audit.c
index 094beded8fc1e0ed11bd9f1b31a8ffd134e870de..40a9e6b9f1b3e13039be451f6027cd259e0c055e 100644
--- a/tests/misc/audit.c
+++ b/tests/misc/audit.c
@@ -1,8 +1,8 @@
/* run.config
+PLUGIN: @EVA_PLUGINS@
LOG: audit-out.json
STDOPT: #"-audit-check @PTEST_DIR@/audit-in.json -audit-prepare @PTEST_RESULT@/audit-out.json -kernel-warn-key audit=active"
*/
-
#include "audit_included.h"
#include "audit_included_but_not_listed.h"
diff --git a/tests/misc/booleans.i b/tests/misc/booleans.i
index 08cbc6cbd89c770448b363d827b620424faf1faa..224a393116b2932b4f29075fbb35705e354b3ca6 100644
--- a/tests/misc/booleans.i
+++ b/tests/misc/booleans.i
@@ -1,6 +1,8 @@
/*run.config
+PLUGIN: @EVA_PLUGINS@
OPT: -eva -print
*/
+
int main (void) {
int x = 42;
/*@ check (boolean)x == 17; */
diff --git a/tests/misc/bts0541.c b/tests/misc/bts0541.c
index 6bbabaaa30cadda796dfc7d69e53074fb4058368..a8dd2eebf5d3e4c744ef72e7eabf100b2c8241e2 100644
--- a/tests/misc/bts0541.c
+++ b/tests/misc/bts0541.c
@@ -1,7 +1,7 @@
/* run.config
+PLUGIN: @EVA_PLUGINS@
OPT: -pp-annot -cpp-extra-args="-I./share/libc" -pp-annot -eva @EVA_CONFIG@
*/
-
#include <stdbool.h>
#include <stdint.h>
#include <stdlib.h>
diff --git a/tests/misc/bts1201.i b/tests/misc/bts1201.i
index dda5727fbcd2222c91dcb711d8d75098afd97857..9f4c1d1506d94d42df8fd76ff4a6317639b94298 100644
--- a/tests/misc/bts1201.i
+++ b/tests/misc/bts1201.i
@@ -1,8 +1,11 @@
/* run.config
+ PLUGIN: @EVA_PLUGINS@
MODULE: @PTEST_NAME@
OPT: -eva-verbose 2 -print
*/
-void main() { //@ assert \true;
+
+void main() {
+ //@ assert \true;
}
void main2() {
diff --git a/tests/misc/bts1347.i b/tests/misc/bts1347.i
index 2cb8c609baa0dfb5d506d7f24694408d1363f62e..f4f0441da5a6fc233463f202e6e1f8dee7175314 100644
--- a/tests/misc/bts1347.i
+++ b/tests/misc/bts1347.i
@@ -1,6 +1,13 @@
/* run.config
+ PLUGIN: @EVA_PLUGINS@ report
MODULE: @PTEST_NAME@
OPT: @EVA_OPTIONS@ -then -report
*/
-int f(int *x) { return *x; }
-int g(int *x) { return *(x++); }
+
+int f(int *x) {
+ return *x;
+}
+
+int g(int *x) {
+ return *(x++);
+}
diff --git a/tests/misc/change_main.i b/tests/misc/change_main.i
index 374658f38ce3c2823acdbe90a413a4b8e17deb55..49e603b43cdee671bad07b0047e70732f9dfa92e 100644
--- a/tests/misc/change_main.i
+++ b/tests/misc/change_main.i
@@ -1,6 +1,6 @@
/* run.config*
+ PLUGIN: @EVA_PLUGINS@
MODULE: @PTEST_NAME@
OPT: -eva -main f -then-on change_main -main g -eva
*/
-
int f(int x) { return x; }
diff --git a/tests/misc/char_ampamp.c b/tests/misc/char_ampamp.c
index aaa77b01d752f75c7487100266144678c766550b..ca336e60b0d24d6dfb1619fbc1e9f1d20f2b08eb 100644
--- a/tests/misc/char_ampamp.c
+++ b/tests/misc/char_ampamp.c
@@ -1,3 +1,8 @@
+/* run.config
+ PLUGIN: @EVA_PLUGINS@
+STDOPT:
+*/
+
char c=1;
int y;
diff --git a/tests/misc/ensures.i b/tests/misc/ensures.i
index 88df7e52cee82769532184b9ea77ea1b73d27644..876ba0671a7ffc352a9dab685b156152be9df7f2 100644
--- a/tests/misc/ensures.i
+++ b/tests/misc/ensures.i
@@ -1,6 +1,11 @@
/* run.config
+PLUGIN: @EVA_PLUGINS@
MODULE: @PTEST_NAME@
OPT:
*/
+
+
//@ ensures *p==1;
-void main(int * p){ *p = 0; }
+void main(int * p) {
+ *p = 0;
+}
diff --git a/tests/misc/fam_with_init.i b/tests/misc/fam_with_init.i
index d7e8c5463b4468718e08c0388284d369ee08f7d5..72e16cb63b0b2b40dd11e64a6053fae0e56a64ca 100644
--- a/tests/misc/fam_with_init.i
+++ b/tests/misc/fam_with_init.i
@@ -1,7 +1,7 @@
/* run.config
-STDOPT: +"-print"
+PLUGIN: @EVA_PLUGINS@
+ STDOPT: +"-print"
*/
-
struct s {
int a;
char data[]; // FAM
diff --git a/tests/misc/function_ptr_alignof.i b/tests/misc/function_ptr_alignof.i
index 1f4b218d0bfd2f02b8e5d3e152eb1177fb4ddf75..deda78cccb535cb02e4055951cb34c12529b6f1f 100644
--- a/tests/misc/function_ptr_alignof.i
+++ b/tests/misc/function_ptr_alignof.i
@@ -1,9 +1,9 @@
/* run.config*
+PLUGIN: @EVA_PLUGINS@
EXIT: 1
STDOPT:
*/
-
void f(void) { }
int main(void)
diff --git a/tests/misc/function_ptr_lvalue_1.i b/tests/misc/function_ptr_lvalue_1.i
index b48ddbd09f7be85d24a13b2f581addd5a8a8fbae..3659b05aae347cae3631c649ef9e531f4d060b19 100644
--- a/tests/misc/function_ptr_lvalue_1.i
+++ b/tests/misc/function_ptr_lvalue_1.i
@@ -1,9 +1,9 @@
/* run.config*
+PLUGIN: @EVA_PLUGINS@
EXIT: 1
STDOPT:
*/
-
void f(void) {}
int main()
diff --git a/tests/misc/function_ptr_lvalue_2.i b/tests/misc/function_ptr_lvalue_2.i
index 333304c449f7728babafb3871439aa92bae480a3..a8e98ba4c41961fd96211487a1f5e990c9893a57 100644
--- a/tests/misc/function_ptr_lvalue_2.i
+++ b/tests/misc/function_ptr_lvalue_2.i
@@ -1,8 +1,8 @@
/* run.config*
+PLUGIN: @EVA_PLUGINS@
EXIT: 1
STDOPT:
*/
-
void f(void) {}
int main()
diff --git a/tests/misc/function_ptr_sizeof.i b/tests/misc/function_ptr_sizeof.i
index 36558b8808f5835948fe3bbe775dda0db517ad39..da0a6d2b8aebecdd7093f6127f843562df543e36 100644
--- a/tests/misc/function_ptr_sizeof.i
+++ b/tests/misc/function_ptr_sizeof.i
@@ -1,9 +1,9 @@
/* run.config*
+PLUGIN: @EVA_PLUGINS@
EXIT: 1
STDOPT:
*/
-
void f(void) { }
int main(void)
diff --git a/tests/misc/issue109.i b/tests/misc/issue109.i
index 4a6e475212ebf15e558888920e4c8e3600bc84fa..60b50daf93dd13b0f37f6a83faf4d3b9fcac4a2a 100644
--- a/tests/misc/issue109.i
+++ b/tests/misc/issue109.i
@@ -1,11 +1,17 @@
/* run.config
+ PLUGIN: @EVA_PLUGINS@
MODULE: @PTEST_NAME@
OPT: -eva @EVA_CONFIG@ -eva-slevel-function main:10
*/
+
void main() {
+
int i, j = 0;
+
for (i=0; i<10; i++) {
j++;
}
+
//@ assert i == j;
+
}
diff --git a/tests/misc/log-file.i b/tests/misc/log-file.i
index 498e4e0654ef12260798992d0ea71fcc66f73fd8..09a77cc462d57fc1678e9f1263f47bbdbece0569 100644
--- a/tests/misc/log-file.i
+++ b/tests/misc/log-file.i
@@ -6,6 +6,7 @@
LOG: log-file-value-all.txt
LOG: log-file-value-default.txt
LOG: plugin-log-all.txt
+PLUGIN: @EVA_PLUGINS@
STDOPT: #"-kernel-log w:@PTEST_RESULT@/log-file-kernel-warnings.txt,r:@PTEST_RESULT@/log-file-kernel-results.txt -eva-log f:@PTEST_RESULT@/log-file-feedback.txt,afewr:@PTEST_RESULT@/log-file-value-all.txt -eva-log :@PTEST_RESULT@/log-file-value-default.txt -then -kernel-log f:@PTEST_RESULT@/log-file-feedback.txt"
MODULE: plugin_log
OPT: -kernel-msg-key foo-category -kernel-log=a:@PTEST_RESULT@/plugin-log-all.txt
diff --git a/tests/misc/log_selfrec.i b/tests/misc/log_selfrec.i
index e7a647f6e453e88b9a63b844539f12d718e9cfbe..46e688a3e3faf0fd1daada2cb54d82835b03a70a 100644
--- a/tests/misc/log_selfrec.i
+++ b/tests/misc/log_selfrec.i
@@ -1,5 +1,5 @@
/* run.config*
-
+PLUGIN: report
EXIT: 1
OPT: -foobar -report-unclassified-error jazz
*/
diff --git a/tests/misc/log_twice.i b/tests/misc/log_twice.i
index 06a2ebcceeb318a91580fa7d4fb7bab6b922a72f..5a43817b8e49604810dddffb5a010641b79962ae 100644
--- a/tests/misc/log_twice.i
+++ b/tests/misc/log_twice.i
@@ -1,8 +1,8 @@
/* run.config
+ PLUGIN: @EVA_PLUGINS@
MODULE: @PTEST_NAME@
OPT: @EVA_CONFIG@
*/
-
int* f() {
int x;
return &x;
diff --git a/tests/misc/long_ident.c b/tests/misc/long_ident.c
index e0ebb31439ac8df4662bbc3106d93d620ff94a9b..58136fd73650e7c2a9171d569c57cf3a9c6e1600 100644
--- a/tests/misc/long_ident.c
+++ b/tests/misc/long_ident.c
@@ -1,4 +1,5 @@
/* run.config
+PLUGIN: obfuscator
OPT: -obfuscate -journal-disable
*/
diff --git a/tests/misc/obfuscate.c b/tests/misc/obfuscate.c
index f993479d0f78d337c57155e20dd3cddbf06a6228..0fb0323afb82e831788ae82bd525b0934b68d17f 100644
--- a/tests/misc/obfuscate.c
+++ b/tests/misc/obfuscate.c
@@ -1,4 +1,5 @@
/* run.config
+PLUGIN: obfuscator
OPT: -obfuscate
*/
diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index b7d55c35d2b08c652da0b87c0ac9f06e6d2abe66..8c4217e9169d95b3ceb869fb45f8a1fd96ec8877 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -69,7 +69,7 @@
}
},
"sources": {
- "tests/misc/audit.c": "aec49f030fcf92bc135bd75e7088194f",
+ "tests/misc/audit.c": "f94ce1c8f5e5911260931783495e2c88",
"tests/misc/audit_included.h": "c2cc488143a476f69cf2ed04c3439e6e",
"tests/misc/audit_included_but_not_listed.h":
"c2cc488143a476f69cf2ed04c3439e6e"
diff --git a/tests/misc/oracle/audit.res.oracle b/tests/misc/oracle/audit.res.oracle
index 40464f54b363d2da4daa36ed357da2364c3f944e..6894ada7dc21fb8274b4aa5db6dd57ce025f0ecd 100644
--- a/tests/misc/oracle/audit.res.oracle
+++ b/tests/misc/oracle/audit.res.oracle
@@ -1,5 +1,5 @@
[kernel:audit] Warning:
- different hashes for tests/misc/audit.c: got aec49f030fcf92bc135bd75e7088194f, expected 01010101010101010101010101010101
+ different hashes for tests/misc/audit.c: got f94ce1c8f5e5911260931783495e2c88, expected 01010101010101010101010101010101
[kernel:audit] Warning:
different hashes for tests/misc/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list)
[kernel:audit] Warning:
diff --git a/tests/misc/oracle/booleans.res.oracle b/tests/misc/oracle/booleans.res.oracle
index 8f7927c6bceb80d83a27026a4ecd2ad4e9c7862b..fbf91d58dadbc18ce9f145ce98f9aaa7d2edc5e3 100644
--- a/tests/misc/oracle/booleans.res.oracle
+++ b/tests/misc/oracle/booleans.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/misc/booleans.i:7: Warning: check got status invalid.
+[eva:alarm] tests/misc/booleans.i:9: Warning: check got status invalid.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
diff --git a/tests/misc/oracle/bts1201.res.oracle b/tests/misc/oracle/bts1201.res.oracle
index 5d683d1decf911024bb296418d7fb0ea6661b50a..312abde0a4dbef5bb0cce723708e27bb0d10f80b 100644
--- a/tests/misc/oracle/bts1201.res.oracle
+++ b/tests/misc/oracle/bts1201.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/misc/bts1201.i:5: assertion got status valid.
+[eva] tests/misc/bts1201.i:8: assertion got status valid.
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
diff --git a/tests/misc/oracle/bts1347.res.oracle b/tests/misc/oracle/bts1347.res.oracle
index 63b1624064934b9b4fb599dc919fbe8c4e922b4e..bd052d2107e24b757eecbc4a414c8824ad152de7 100644
--- a/tests/misc/oracle/bts1347.res.oracle
+++ b/tests/misc/oracle/bts1347.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/misc/bts1347.i:5: Warning:
+[eva:alarm] tests/misc/bts1347.i:8: Warning:
out of bounds read. assert \valid_read(x);
[eva] Recording results for f
[eva] done for function f
@@ -13,7 +13,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/misc/bts1347.i:6: Warning:
+[eva:alarm] tests/misc/bts1347.i:12: Warning:
out of bounds read. assert \valid_read(tmp);
(tmp from x++)
[eva] Recording results for g
@@ -24,22 +24,22 @@
--- Properties of Function 'f'
--------------------------------------------------------------------------------
-[ Dead ] Assertion 'emitter' (file tests/misc/bts1347.i, line 5)
+[ Dead ] Assertion 'emitter' (file tests/misc/bts1347.i, line 8)
Locally valid, but unreachable.
By Eva because:
- - Unreachable return (file tests/misc/bts1347.i, line 5)
-[Unreachable] Unreachable return (file tests/misc/bts1347.i, line 5)
+ - Unreachable return (file tests/misc/bts1347.i, line 8)
+[Unreachable] Unreachable return (file tests/misc/bts1347.i, line 8)
by Eva.
--------------------------------------------------------------------------------
--- Properties of Function 'g'
--------------------------------------------------------------------------------
-[ - ] Assertion 'Eva,mem_access' (file tests/misc/bts1347.i, line 6)
+[ - ] Assertion 'Eva,mem_access' (file tests/misc/bts1347.i, line 12)
tried with Eva.
-[ Partial ] Assertion 'emitter' (file tests/misc/bts1347.i, line 6)
+[ Partial ] Assertion 'emitter' (file tests/misc/bts1347.i, line 12)
By emitter, with pending:
- - Assertion 'Eva,mem_access' (file tests/misc/bts1347.i, line 6)
+ - Assertion 'Eva,mem_access' (file tests/misc/bts1347.i, line 12)
--------------------------------------------------------------------------------
--- Status Report Summary
@@ -55,9 +55,9 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/misc/bts1347.i:5: Warning:
+[eva:alarm] tests/misc/bts1347.i:8: Warning:
out of bounds read. assert \valid_read(x);
-[eva] tests/misc/bts1347.i:5: assertion 'emitter' got status valid.
+[eva] tests/misc/bts1347.i:8: assertion 'emitter' got status valid.
[eva] Recording results for f
[eva] done for function f
[eva] Analyzing an incomplete application starting at g
@@ -65,9 +65,9 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/misc/bts1347.i:6: Warning:
+[eva:alarm] tests/misc/bts1347.i:12: Warning:
out of bounds read. assert \valid_read(tmp);
(tmp from x++)
-[eva] tests/misc/bts1347.i:6: assertion 'emitter' got status valid.
+[eva] tests/misc/bts1347.i:12: assertion 'emitter' got status valid.
[eva] Recording results for g
[eva] done for function g
diff --git a/tests/misc/oracle/char_ampamp.res.oracle b/tests/misc/oracle/char_ampamp.res.oracle
index e48fc08714ecef939dbe64b842387547d45fee89..9b826050d9f6813368d462f3cbcf42717a2a6068 100644
--- a/tests/misc/oracle/char_ampamp.res.oracle
+++ b/tests/misc/oracle/char_ampamp.res.oracle
@@ -6,8 +6,8 @@
c ∈ {1}
y ∈ {0}
[eva] computing for function g <- main.
- Called from tests/misc/char_ampamp.c:12.
-[eva] tests/misc/char_ampamp.c:6: Frama_C_show_each_x: {1}
+ Called from tests/misc/char_ampamp.c:17.
+[eva] tests/misc/char_ampamp.c:11: Frama_C_show_each_x: {1}
[eva] Recording results for g
[eva] Done for function g
[eva] Recording results for main
diff --git a/tests/misc/oracle/ensures.res.oracle b/tests/misc/oracle/ensures.res.oracle
index ee0832cdeffc1cc003c4ae54db0a7947af527c57..395d3e8484bed83286957dc88b9227ac3313e961 100644
--- a/tests/misc/oracle/ensures.res.oracle
+++ b/tests/misc/oracle/ensures.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/misc/ensures.i:5: Warning:
+[eva:alarm] tests/misc/ensures.i:8: Warning:
function main: postcondition got status invalid.
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
diff --git a/tests/misc/oracle/issue109.res.oracle b/tests/misc/oracle/issue109.res.oracle
index 6282ea4acd8c628f4af05e21d7bda570ddfb96c3..b31581fd4bb2e915ffde47bdaafa44636ea3b54b 100644
--- a/tests/misc/oracle/issue109.res.oracle
+++ b/tests/misc/oracle/issue109.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/misc/issue109.i:10: assertion got status valid.
+[eva] tests/misc/issue109.i:15: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -17,7 +17,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/misc/issue109.i:10: assertion got status valid.
+[eva] tests/misc/issue109.i:15: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/misc/oracle/well_typed_alarm.res.oracle b/tests/misc/oracle/well_typed_alarm.res.oracle
index cff9cdaaa88971d0ae07d576c88835d8e353efe0..5eaf869164e05b944de3f4d17b8ca5c8cc1947d5 100644
--- a/tests/misc/oracle/well_typed_alarm.res.oracle
+++ b/tests/misc/oracle/well_typed_alarm.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/misc/well_typed_alarm.i:11: Warning:
+[eva:alarm] tests/misc/well_typed_alarm.i:16: Warning:
pointer comparison. assert \pointer_comparable((void *)p, (void *)q);
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
diff --git a/tests/misc/pragma-pack.c b/tests/misc/pragma-pack.c
index b2e44f3f65464fb533c965f48beb09ce1d9be20a..0eda8ce2f0b4ba0a2e56bab74f6477e2ea5780b4 100644
--- a/tests/misc/pragma-pack.c
+++ b/tests/misc/pragma-pack.c
@@ -1,9 +1,9 @@
/*run.config
+ PLUGIN: @EVA_PLUGINS@
STDOPT: +"-machdep gcc_x86_64 -kernel-msg-key typing:pragma"
STDOPT: +"-machdep gcc_x86_32"
STDOPT: +"-machdep msvc_x86_64"
*/
-
#include "pragma-pack-utils.h"
#include <stdint.h>
diff --git a/tests/misc/pragma_pack_zero.c b/tests/misc/pragma_pack_zero.c
index 22f956bd3c37c453f011aee30726b8f443dfd79e..52c5a87ad91f6edc44b368af7a0119cd9402e5e6 100644
--- a/tests/misc/pragma_pack_zero.c
+++ b/tests/misc/pragma_pack_zero.c
@@ -1,4 +1,5 @@
/* run.config
+PLUGIN: @EVA_PLUGINS@
STDOPT: +"-machdep gcc_x86_64"
STDOPT: +"-machdep msvc_x86_64"
*/
@@ -7,7 +8,6 @@
// In GCC, its current (undocumented) behavior is equivalent to #pragma pack(),
// that is, disable packing (reset to default). We emulate this behavior,
// but with a warning.
-
#include "pragma-pack-utils.h"
#include <stdint.h>
diff --git a/tests/misc/test_config b/tests/misc/test_config
index 111c347883729eb88f73d71774c9496d687e21fb..2cfb7e2f9204e5c904f80f601742facf6608faaa 100644
--- a/tests/misc/test_config
+++ b/tests/misc/test_config
@@ -1,2 +1,7 @@
+PLUGIN:
MODULE: global_decl_loc
MODULE:
+STDOPT:
+
+# COMMENT: Directive to add in your test file when using STDOPT:
+# COMMENT: PLUGIN: @EVA_PLUGINS@
diff --git a/tests/misc/well_typed_alarm.i b/tests/misc/well_typed_alarm.i
index 11ac1cd00a1cd0e5ec6f93c00a59b6e0e3ecc00c..dcbe3dacc09f3599f32413e4ae8537b6c61b33b2 100644
--- a/tests/misc/well_typed_alarm.i
+++ b/tests/misc/well_typed_alarm.i
@@ -1,13 +1,19 @@
/* run.config*
+ PLUGIN: @EVA_PLUGINS@
MODULE: @PTEST_NAME@
OPT:
*/
+
int main(int c) {
+
int x = 0;
int y = 0;
+
int *p = &x;
int *q = &y;
+
if (c) q = &x;
if (p<=q) x++;
+
return *q;
}
diff --git a/tests/misc/widen_hints.c b/tests/misc/widen_hints.c
index fca1b6e7e6ef953b698c6d2fa04bee2193bd889c..0148d513d8cad7072b213dc38041fa8d3a85163e 100644
--- a/tests/misc/widen_hints.c
+++ b/tests/misc/widen_hints.c
@@ -1,4 +1,5 @@
/* run.config
+PLUGIN: @EVA_PLUGINS@
EXIT:1
OPT: -eva @EVA_CONFIG@ -cpp-extra-args=-DSYNTAX_ERRORS -kernel-warn-key=annot-error=active
OPT: -eva @EVA_CONFIG@ -cpp-extra-args=-DNONCONST
@@ -7,7 +8,6 @@
OPT: -eva @EVA_CONFIG@ -cpp-extra-args=-DALLGLOBAL -eva-msg-key widen-hints
*/
#define N 2
-
const int x = 9;
int not_const = 42; // cannot be used as widen hint
diff --git a/tests/misc/widen_hints2.c b/tests/misc/widen_hints2.c
index bc457535df6b9a0d18e9f93e5a1767dbbaad438d..9d35092bfb98ff4599952dc315eac04772ee74de 100644
--- a/tests/misc/widen_hints2.c
+++ b/tests/misc/widen_hints2.c
@@ -1,8 +1,8 @@
/* run.config
+ PLUGIN: @EVA_PLUGINS@
STDOPT: #"-eva-msg-key widen-hints"
OPT: -print
*/
-
#include <stdlib.h>
#define N 2
diff --git a/tests/misc/widen_hints_float.c b/tests/misc/widen_hints_float.c
index a01f0a357842a423528cc508dfc39663b307f0a8..13326812adfc4ab8d1637b3955172fc71a77cdff 100644
--- a/tests/misc/widen_hints_float.c
+++ b/tests/misc/widen_hints_float.c
@@ -1,8 +1,8 @@
/* run.config*
+ PLUGIN: @EVA_PLUGINS@
STDOPT: #"-eva-subdivide-non-linear 20"
*/
-
#include "__fc_builtin.h"
#include <math.h>
diff --git a/tests/misc/wstring_phase6.c b/tests/misc/wstring_phase6.c
index f9884778c87c760721d9a3f9616e909abe1f9ff0..c364cd912c972d11721d70b0295354cd5e22d3b5 100644
--- a/tests/misc/wstring_phase6.c
+++ b/tests/misc/wstring_phase6.c
@@ -1,9 +1,9 @@
/* run.config
+PLUGIN: variadic
MODULE: @PTEST_NAME@
OPT: -journal-disable -print -variadic-no-translation
*/
#include <stdio.h>
-
// See http://stackoverflow.com/questions/18102502/mixing-wide-and-narrow-string-literals-in-c
int main(){
printf( "%s\n", "123" "456" );
diff --git a/tests/occurrence/test_config b/tests/occurrence/test_config
index 5e291a6ae016a6564af7152faf5f6ea67f58a94f..54290ebd2d68ef9aecc5959967d39d46a61ec28b 100644
--- a/tests/occurrence/test_config
+++ b/tests/occurrence/test_config
@@ -1 +1,2 @@
-STDOPT: +"-load-module" +"occurrence" -"-eva" -"-out" -"-input" -"-deps" +"-occurrence-verbose 1"
+PLUGIN: eva,scope occurrence
+STDOPT: -"-eva" -"-out" -"-input" -"-deps" +"-occurrence-verbose 1"
diff --git a/tests/pdg/bts1194.c b/tests/pdg/bts1194.c
index baa829837c3a54216aac8310f110bc0ee53fb35d..37d50ee5443a96ae718e5d645d5540edaea18da3 100644
--- a/tests/pdg/bts1194.c
+++ b/tests/pdg/bts1194.c
@@ -1,7 +1,7 @@
/* run.config
+PLUGIN: @EVA_PLUGINS@ pdg slicing
STDOPT: +"-eva -inout -pdg -calldeps -deps -then -slice-return main -then-last -print @EVA_OPTIONS@"
*/
-
int Y, X;
volatile v;
diff --git a/tests/pdg/test_config b/tests/pdg/test_config
index d9d741191d10ade715f1080b42b4a421d0d5e4c1..1f84f4645e5d2c1d56c903c01d91046a298c11c2 100644
--- a/tests/pdg/test_config
+++ b/tests/pdg/test_config
@@ -1 +1,2 @@
-OPT: -journal-disable @EVA_OPTIONS@ -pdg-print -pdg-verbose 2
+PLUGIN: @EVA_PLUGINS@ pdg
+OPT: @EVA_OPTIONS@ -pdg-print -pdg-verbose 2
diff --git a/tests/pretty_printing/test_config b/tests/pretty_printing/test_config
index c43ca10542958476406623d6a34d4049fce20852..3ef00bad562303349e568b77920e4499cd980972 100644
--- a/tests/pretty_printing/test_config
+++ b/tests/pretty_printing/test_config
@@ -1,5 +1,6 @@
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
+PLUGIN:
CMD: FRAMAC_PLUGIN=tests/.empty @frama-c@
-OPT: @PTEST_FILE@ -print -journal-disable -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print
+OPT: @PTEST_FILE@ -print -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print
diff --git a/tests/rte/oracle/unspecified_sequence.res.oracle b/tests/rte/oracle/unspecified_sequence.res.oracle
index 3df3256fe5fa9550c8fbe3a96a7c7e8522fd9561..2d9f1c127532b318461b9faaeb99c1befaf198b5 100644
--- a/tests/rte/oracle/unspecified_sequence.res.oracle
+++ b/tests/rte/oracle/unspecified_sequence.res.oracle
@@ -4,15 +4,15 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
t[0..9] ∈ {0}
-[eva:alarm] tests/rte/unspecified_sequence.i:7: Warning:
+[eva:alarm] tests/rte/unspecified_sequence.i:12: Warning:
function main: precondition got status unknown.
[eva] computing for function f <- main.
- Called from tests/rte/unspecified_sequence.i:10.
+ Called from tests/rte/unspecified_sequence.i:15.
[eva] Recording results for f
[eva] Done for function f
-[eva] tests/rte/unspecified_sequence.i:11: Reusing old results for call to f
+[eva] tests/rte/unspecified_sequence.i:16: Reusing old results for call to f
[eva] computing for function f <- main.
- Called from tests/rte/unspecified_sequence.i:11.
+ Called from tests/rte/unspecified_sequence.i:16.
[eva] Recording results for f
[eva] Done for function f
[eva] Recording results for main
diff --git a/tests/rte/test_config b/tests/rte/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..8351f51e855ecf8f8f4951813caf7b5d2bdbc455
--- /dev/null
+++ b/tests/rte/test_config
@@ -0,0 +1,2 @@
+PLUGIN: rtegen
+STDOPT:
diff --git a/tests/rte/unspecified_sequence.i b/tests/rte/unspecified_sequence.i
index bf067c5a072b4f58f001aa60f53788177cf504ce..63e60f119cf1b11b66d6bd7f0736be514624a28a 100644
--- a/tests/rte/unspecified_sequence.i
+++ b/tests/rte/unspecified_sequence.i
@@ -1,3 +1,8 @@
+/* run.config
+ PLUGIN: @EVA_PLUGINS@
+ STDOPT:
+*/
+
unsigned long long f(int x) {
return 0;
}
diff --git a/tests/rte/value_rte.c b/tests/rte/value_rte.c
index 0587fca439d1864503ee51cac0cbafb41e217127..9d2ee91f6686a741f5b2dcb0fd5e23e0fad09c30 100644
--- a/tests/rte/value_rte.c
+++ b/tests/rte/value_rte.c
@@ -1,7 +1,7 @@
/* run.config
+PLUGIN: eva,scope rtegen report
OPT: -rte -then -eva @EVA_OPTIONS@ -then -report
*/
-
#include "stdio.h"
int main(){
diff --git a/tests/rte_manual/test_config b/tests/rte_manual/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..7455cf5899e3ce3e7270344ef8217b1c06f9f2ee
--- /dev/null
+++ b/tests/rte_manual/test_config
@@ -0,0 +1,2 @@
+PLUGIN: @EVA_PLUGINS@ rtegen
+STDOPT:
diff --git a/tests/saveload/bool.c b/tests/saveload/bool.c
index f90635c4440b48bc7fdd4446bd6f9adadd8a22a6..f942a8cae78be9b6917f8909f0d2349e818aaee5 100644
--- a/tests/saveload/bool.c
+++ b/tests/saveload/bool.c
@@ -1,5 +1,5 @@
/* run.config
- EXECNOW: BIN bool.sav LOG bool_sav.res LOG bool_sav.err ./bin/toplevel.opt -save ./tests/saveload/result/bool.sav -machdep x86_32 -eva @EVA_OPTIONS@ ./tests/saveload/bool.c > tests/saveload/result/bool_sav.res 2> tests/saveload/result/bool_sav.err
+ EXECNOW: BIN bool.sav LOG bool_sav.res LOG bool_sav.err @frama-c@ -save ./tests/saveload/result/bool.sav -machdep x86_32 -eva @EVA_OPTIONS@ ./tests/saveload/bool.c > tests/saveload/result/bool_sav.res 2> tests/saveload/result/bool_sav.err
STDOPT: +"-load ./tests/saveload/result/bool.sav -out -input -deps"
STDOPT: +"-load ./tests/saveload/result/bool.sav -eva @EVA_OPTIONS@"
*/
diff --git a/tests/saveload/callbacks.i b/tests/saveload/callbacks.i
index b1fe21aabd15e996e1b84a7ba90ab7025dcd4cdb..672fc08788ee5ecc689372682a92e5814c3faa0e 100644
--- a/tests/saveload/callbacks.i
+++ b/tests/saveload/callbacks.i
@@ -1,5 +1,5 @@
/* run.config
- EXECNOW: LOG callbacks_initial.res LOG callbacks_initial.err BIN callbacks.sav ./bin/toplevel.opt tests/saveload/callbacks.i -out -calldeps -eva-show-progress -main main1 -save ./tests/saveload/result/callbacks.sav > ./tests/saveload/result/callbacks_initial.res 2> ./tests/saveload/result/callbacks_initial.err
+ EXECNOW: LOG callbacks_initial.res LOG callbacks_initial.err BIN callbacks.sav @frama-c@ tests/saveload/callbacks.i -out -calldeps -eva-show-progress -main main1 -save ./tests/saveload/result/callbacks.sav > ./tests/saveload/result/callbacks_initial.res 2> ./tests/saveload/result/callbacks_initial.err
STDOPT: +"-load ./tests/saveload/result/callbacks.sav -main main2 -then -main main3"
*/
diff --git a/tests/saveload/isset.c b/tests/saveload/isset.c
index 720c3d635f2f3bc362c24fe83422bf51766ddfa6..8cdfc876ef88218d1f1c70f547bd2254820fd3e2 100644
--- a/tests/saveload/isset.c
+++ b/tests/saveload/isset.c
@@ -1,5 +1,5 @@
/* run.config
- EXECNOW: LOG isset_sav.res LOG isset_sav.err BIN isset.sav ./bin/toplevel.opt -quiet -eva @EVA_OPTIONS@ -save tests/saveload/result/isset.sav tests/saveload/isset.c > ./tests/saveload/result/isset_sav.res 2> ./tests/saveload/result/isset_sav.err
+ EXECNOW: LOG isset_sav.res LOG isset_sav.err BIN isset.sav @frama-c@ -quiet -eva @EVA_OPTIONS@ -save tests/saveload/result/isset.sav tests/saveload/isset.c > ./tests/saveload/result/isset_sav.res 2> ./tests/saveload/result/isset_sav.err
STDOPT: +"-quiet -load ./tests/saveload/result/isset.sav"
STDOPT: +"-load ./tests/saveload/result/isset.sav"
STDOPT: +"-eva @EVA_OPTIONS@ -load ./tests/saveload/result/isset.sav"
diff --git a/tests/saveload/load_one.i b/tests/saveload/load_one.i
index 75dde3f72926e6957c0fdfb898dbd3c3ba37932d..6eb0a89c1bd111ae094950e02c6e9ad00eee110e 100644
--- a/tests/saveload/load_one.i
+++ b/tests/saveload/load_one.i
@@ -1,6 +1,7 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- STDOPT: +"-load-module @PTEST_DIR@/@PTEST_NAME@.cmxs"
+ PLUGIN: @EVA_PLUGINS@ sparecode
+ MODULE: @PTEST_NAME@
+ STDOPT:
*/
int G;
@@ -12,7 +13,6 @@ int f (int x, int y) {
int main (void) {
int a = 1;
int b = 1;
-
/*@ assert a == 1; */
f (0, 0); /* this call is useless : should be removed */
diff --git a/tests/saveload/multi_project.i b/tests/saveload/multi_project.i
index ab0d9a44fd15de6c80394627618705578bd54744..acdf9a01fe1bca09b9aa63049dca4f9180e00298 100644
--- a/tests/saveload/multi_project.i
+++ b/tests/saveload/multi_project.i
@@ -1,8 +1,8 @@
/* run.config
- EXECNOW: BIN multi_project.sav LOG multi_project_sav.res LOG multi_project_sav.err ./bin/toplevel.opt -save ./tests/saveload/result/multi_project.sav @EVA_OPTIONS@ -semantic-const-folding @PTEST_DIR@/@PTEST_NAME@.i > tests/saveload/result/multi_project_sav.res 2> tests/saveload/result/multi_project_sav.err
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- STDOPT: +"-load ./tests/saveload/result/multi_project.sav -journal-disable"
- CMD: @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ PLUGIN: @EVA_PLUGINS@ constant_propagation
+ EXECNOW: BIN multi_project.sav LOG multi_project_sav.res LOG multi_project_sav.err @frama-c@ -save ./tests/saveload/result/multi_project.sav @EVA_OPTIONS@ -semantic-const-folding @PTEST_DIR@/@PTEST_NAME@.i > tests/saveload/result/multi_project_sav.res 2> tests/saveload/result/multi_project_sav.err
+ STDOPT: +"-load ./tests/saveload/result/multi_project.sav"
+ MODULE: @PTEST_NAME@
OPT: -eva @EVA_OPTIONS@
*/
int f(int x) {
diff --git a/tests/saveload/segfault_datatypes.i b/tests/saveload/segfault_datatypes.i
index 021df2f49372ecd4d9633a5c9dc94a9f945fa341..af9a24fbb57274f132682e759096ddd5ebb3aa62 100644
--- a/tests/saveload/segfault_datatypes.i
+++ b/tests/saveload/segfault_datatypes.i
@@ -1,10 +1,10 @@
/* run.config*
- EXECNOW: make -s ./tests/saveload/segfault_datatypes_A.cmxs ./tests/saveload/segfault_datatypes_B.cmxs
- EXECNOW: LOG segfault_datatypes_sav.res LOG segfault_datatypes_sav.err BIN segfault_datatypes.sav @frama-c@ -load-module ./tests/saveload/segfault_datatypes_A -eva @EVA_OPTIONS@ -out -input -deps ./tests/saveload/segfault_datatypes.i -save ./tests/saveload/result/segfault_datatypes.sav > ./tests/saveload/result/segfault_datatypes_sav.res 2> ./tests/saveload/result/segfault_datatypes_sav.err
- STDOPT: +"-load-module ./tests/saveload/segfault_datatypes_B -load ./tests/saveload/result/segfault_datatypes.sav -eva -out -input -deps -journal-disable"
+ MODULE: segfault_datatypes_A
+ EXECNOW: LOG segfault_datatypes_sav.res LOG segfault_datatypes_sav.err BIN segfault_datatypes.sav @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save ./tests/saveload/result/segfault_datatypes.sav > ./tests/saveload/result/segfault_datatypes_sav.res 2> ./tests/saveload/result/segfault_datatypes_sav.err
+ MODULE: segfault_datatypes_B
+ STDOPT: +"-load ./tests/saveload/result/segfault_datatypes.sav -eva -out -input -deps"
*/
-
int main() {
int i, j;
diff --git a/tests/saveload/sparecode.i b/tests/saveload/sparecode.i
index 33d1776ddc1ace121e6c617062505c43b4219b3d..b82bea7578da014e9734244c1d6f95a0e62e3b30 100644
--- a/tests/saveload/sparecode.i
+++ b/tests/saveload/sparecode.i
@@ -1,9 +1,9 @@
/* run.config
- EXECNOW: BIN sparecode.sav LOG sparecode_sav.res LOG sparecode_sav.err ./bin/toplevel.opt -slicing-level 2 -slice-return main -eva-show-progress -save ./tests/saveload/result/sparecode.sav tests/saveload/sparecode.i -then-on 'Slicing export' -print > tests/saveload/result/sparecode_sav.res 2> tests/saveload/result/sparecode_sav.err
+ PLUGIN: @EVA_PLUGINS@ slicing
+ EXECNOW: BIN sparecode.sav LOG sparecode_sav.res LOG sparecode_sav.err @frama-c@ -slicing-level 2 -slice-return main -eva-show-progress -save ./tests/saveload/result/sparecode.sav tests/saveload/sparecode.i -then-on 'Slicing export' -print > tests/saveload/result/sparecode_sav.res 2> tests/saveload/result/sparecode_sav.err
STDOPT: +"-load ./tests/saveload/result/sparecode.sav"
*/
int G;
-
int f (int x, int y) {
G = y;
return x;
diff --git a/tests/saveload/test_config b/tests/saveload/test_config
index 1712a20359b38feaedc7a61eec51ffa3aebc9879..0fb1ff9fa15158c8174c8231a22976557eb4dd40 100644
--- a/tests/saveload/test_config
+++ b/tests/saveload/test_config
@@ -1 +1,2 @@
+PLUGIN: @EVA_PLUGINS@
OPT: @EVA_OPTIONS@
diff --git a/tests/scope/bts971.c b/tests/scope/bts971.c
index 24716e1928853c5f80851385f3bd06a00519ae20..968ca119f331972615296755979e780362adc72f 100644
--- a/tests/scope/bts971.c
+++ b/tests/scope/bts971.c
@@ -1,11 +1,11 @@
/* run.config
- MODULE: @PTEST_NAME@
- OPT: -journal-disable -then -main main2
+ PLUGIN: @EVA_PLUGINS@ pdg
+ MODULE: @PTEST_NAME@
+ OPT: -then -main main2
*/
/* bug 971: */
volatile foo;
int v;
-
void f1 () {
v += 1;
}
diff --git a/tests/scope/test_config b/tests/scope/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..55b824af6be4dcc6553df43fd37dc898a4e4845f
--- /dev/null
+++ b/tests/scope/test_config
@@ -0,0 +1,2 @@
+PLUGIN: @EVA_PLUGINS@
+STDOPT:
diff --git a/tests/scope/zones.c b/tests/scope/zones.c
index e8808595b16aee5132fb1348e55883ea9f6552d1..b60b239a0fcd7922d9cee94203c6c2f1594f6630 100644
--- a/tests/scope/zones.c
+++ b/tests/scope/zones.c
@@ -1,9 +1,9 @@
/* run.config
-# MODULE: @PTEST_NAME@
- OPT: -load-module @PTEST_DIR@/@PTEST_NAME@ -eva @EVA_OPTIONS@ -journal-disable
+ PLUGIN: @EVA_PLUGINS@ pdg
+ MODULE: @PTEST_NAME@
+ OPT: -eva @EVA_OPTIONS@
*/
-
/* bin/viewer.opt -eva @PTEST_DIR@/@PTEST_NAME@.c */
int T [10];
diff --git a/tests/slicing/combine.i b/tests/slicing/combine.i
index 704851ba39349b0e151e4a225cdb9ef865970fc9..05589afc7c888447f562aa65a4c850539bb99790 100644
--- a/tests/slicing/combine.i
+++ b/tests/slicing/combine.i
@@ -1,6 +1,6 @@
/* run.config
+ PLUGIN: @PTEST_PLUGIN@ constant_propagation sparecode
MODULE: libSelect @PTEST_NAME@
-
OPT: @EVA_OPTIONS@ -deps
*/
diff --git a/tests/slicing/test_config b/tests/slicing/test_config
index 1c214a23023446fa86e655de311a60df62051ceb..9c7afdad731fc9fe8f51b8d9c0d1b68a6001ebf2 100644
--- a/tests/slicing/test_config
+++ b/tests/slicing/test_config
@@ -1,3 +1,4 @@
MODULE: libSelect libAnim
MODULE:
+PLUGIN: eva,scope,variadic slicing
OPT: @EVA_OPTIONS@ -machdep x86_32
diff --git a/tests/sparecode/bts334.i b/tests/sparecode/bts334.i
index f6af16f8c93874894790dd75e3ce64ab219f6464..f05a44ace82ecd919b5168fe6f219d4116ad420c 100644
--- a/tests/sparecode/bts334.i
+++ b/tests/sparecode/bts334.i
@@ -1,7 +1,8 @@
/*run.config
- STDOPT: +"-sparecode-debug 0 -main main_init -sparecode-analysis -sparecode-no-annot "
- STDOPT: +"-sparecode-debug 0 -main main_init -slice-pragma loop_body -then-on 'Slicing export' -print"
- STDOPT: +"-sparecode-debug 0 -main main_init -slice-pragma loop_body -calldeps -then-on 'Slicing export' -print"
+ STDOPT: +"-sparecode-debug 0 -main main_init -sparecode-analysis -sparecode-no-annot "
+PLUGIN: @PTEST_PLUGIN@ slicing
+ STDOPT: +"-sparecode-debug 0 -main main_init -slice-pragma loop_body -then-on 'Slicing export' -print"
+ STDOPT: +"-sparecode-debug 0 -main main_init -slice-pragma loop_body -calldeps -then-on 'Slicing export' -print"
*/
int kf ;
int k[2] ;
@@ -10,7 +11,6 @@ static int si[2] = {0, 0};
static int so[2] = {0, 0};
int f(int vi , int i )
{ int vo ;
-
{vo = so[i] / kf + k[i] * (vi - si[i]);
so[i] = vo;
si[i] = vi;
diff --git a/tests/sparecode/calls.i b/tests/sparecode/calls.i
index 91773f1b22e0e11e51ff9a4402e9dd6df50d3b3a..dd0c6996091af7f446143ccee7108a9cdf19b84a 100644
--- a/tests/sparecode/calls.i
+++ b/tests/sparecode/calls.i
@@ -1,9 +1,9 @@
/* run.config
STDOPT: +"-sparecode-analysis"
+PLUGIN: @PTEST_PLUGIN@ slicing
STDOPT: +"-slicing-level 2 -slice-return main -then-on 'Slicing export' -print"
*/
int G;
-
int f (int x, int y) {
G = y;
return x;
diff --git a/tests/sparecode/dead_code.i b/tests/sparecode/dead_code.i
index 327e62941abd01360bcb74cc728a34ed68931618..5f4165959ff68c54f907c1b6707611503792f28b 100644
--- a/tests/sparecode/dead_code.i
+++ b/tests/sparecode/dead_code.i
@@ -1,5 +1,6 @@
/* run.config
STDOPT: +"-sparecode"
+PLUGIN: @PTEST_PLUGIN@ slicing
STDOPT: +"-slicing-level 2 -slice-return main -then-on 'Slicing export' -print"
*/
diff --git a/tests/sparecode/glob_decls.i b/tests/sparecode/glob_decls.i
index abdf205de22a03d9dce5d76f5e67c2cffa3695f3..eb211f029f70d1e7a2720fe26d44691f7472aeaf 100644
--- a/tests/sparecode/glob_decls.i
+++ b/tests/sparecode/glob_decls.i
@@ -1,6 +1,7 @@
/* run.config
- STDOPT: +"-lib-entry -sparecode-analysis "
- STDOPT: +"-lib-entry -slice-pragma main -slice-return main -then-on 'Slicing export' -print"
+ STDOPT: +"-lib-entry -sparecode-analysis "
+PLUGIN: @PTEST_PLUGIN@ slicing
+ STDOPT: +"-lib-entry -slice-pragma main -slice-return main -then-on 'Slicing export' -print"
STDOPT: +"-sparecode-rm-unused-globals"
*/
@@ -18,7 +19,6 @@ Ps GPs;
typedef struct { int a; int b; } Ts2;
Ts2 S2;
-
typedef char Ts2bis;
Ts2bis C = 'a';
diff --git a/tests/sparecode/intra.i b/tests/sparecode/intra.i
index 65316cbe60af3abe7f2e18cfe00cf1bae48b6903..21f41c1d712ad71bb0ec0e4718acf2c335e91df0 100644
--- a/tests/sparecode/intra.i
+++ b/tests/sparecode/intra.i
@@ -1,11 +1,13 @@
/* run.config
STDOPT: +"-sparecode-analysis"
+PLUGIN: @PTEST_PLUGIN@ slicing
STDOPT: +"-sparecode-debug 0 -slicing-level 2 -slice-return main -then-last -print"
+PLUGIN: @SPARECODE_PLUGINS@
STDOPT: +"-sparecode-debug 0 -main main2 -sparecode-analysis"
+PLUGIN: @PTEST_PLUGIN@ slicing
STDOPT: +"-sparecode-debug 0 -main main2 -slice-return main2 -then-last -print"
STDOPT: +"-sparecode-debug 0 -main main2 -slice-return main2 -slice-assert f10 -then-last -print"
*/
-
/* Waiting for results such as:
* spare code analysis removes statements having variables with
* prefix "spare_"
@@ -13,9 +15,7 @@
* slicing analysis removes statement having variables with
* prefix "spare_" and "any_"
*/
-
int G;
-
int tmp (int a) {
int x = a;
//@ assert x == a ;
diff --git a/tests/sparecode/params.i b/tests/sparecode/params.i
index 26bb415eefc1cd598a97b4b0fe1957132d1d0cab..4fd2d1b6efdebd9eb7f0ea088e74a442bb2049ab 100644
--- a/tests/sparecode/params.i
+++ b/tests/sparecode/params.i
@@ -1,8 +1,8 @@
/* run.config
STDOPT: +"-sparecode-analysis"
+PLUGIN: @PTEST_PLUGIN@ slicing
STDOPT: +"-slicing-level 2 -slice-return main -then-last -print"
*/
-
/* This is an example from #529. 'y' in [main1] should be visible to get a
* compilable result. But unfortunatly, this leads to also select [b=1] in
* [main]. This should be enhanced... */
diff --git a/tests/sparecode/test_config b/tests/sparecode/test_config
index a9330dd48d062e0b27b9bb948a88af6f4250c17a..40e3a32e1141194ae21aebe0470c76bca948bc06 100644
--- a/tests/sparecode/test_config
+++ b/tests/sparecode/test_config
@@ -1 +1,3 @@
+MACRO: SPARECODE_PLUGINS @EVA_PLUGINS@ sparecode
+PLUGIN: @SPARECODE_PLUGINS@
OPT: -journal-disable @EVA_OPTIONS@ -sparecode-debug 1
diff --git a/tests/spec/array_typedef.c b/tests/spec/array_typedef.c
index 86387dcf4273550cd3a88f637d544008c16bacdb..88daa60d902d2501043d8f697ce6152c0c9f44e0 100644
--- a/tests/spec/array_typedef.c
+++ b/tests/spec/array_typedef.c
@@ -1,9 +1,9 @@
/*run.config
- OPT: -print -eva @EVA_CONFIG@ -journal-disable
+PLUGIN: eva, scope
+ OPT: -print -eva @EVA_CONFIG@
*/
#define IP_FIELD 4
typedef int ip_address[IP_FIELD];
-
typedef struct {
ip_address src;
int dst[IP_FIELD];
diff --git a/tests/spec/assigns_result.i b/tests/spec/assigns_result.i
index f850166909efe129536bc4b54cae90447f6dbaaa..55ebd04043412a8e6d2f9e9480b4c0bb94de85b5 100644
--- a/tests/spec/assigns_result.i
+++ b/tests/spec/assigns_result.i
@@ -1,8 +1,8 @@
/* run.config
+PLUGIN: eva,scope
STDOPT: +"-deps @EVA_OPTIONS@"
*/
int X,Y;
-
/*@ assigns \result;
assigns \exit_status;
*/
diff --git a/tests/spec/assigns_void.c b/tests/spec/assigns_void.c
index 6e70195b864bfe5bb5f5d6f5c48ae74d798d9fbf..36cfe99b1ec2643f87f63401a3361e8cfce14152 100644
--- a/tests/spec/assigns_void.c
+++ b/tests/spec/assigns_void.c
@@ -1,10 +1,10 @@
/* run.config
- OPT: -print -journal-disable -kernel-warn-key=annot-error=active
- OPT: -eva @EVA_CONFIG@ -main g -print -no-annot -journal-disable
+ OPT: -print -kernel-warn-key=annot-error=active
+PLUGIN: eva,scope
+ OPT: -eva @EVA_CONFIG@ -main g -print -no-annot
*/
//@ assigns *x;
void f(void *x);
-
void g() {
int y;
int* x = &y;
diff --git a/tests/spec/behavior_assert.c b/tests/spec/behavior_assert.c
index 2f5d7f9760516f5bb73dea22b220b91f2e07edc3..7d0ce3885199a400d456597f6083bdf51a3470c2 100644
--- a/tests/spec/behavior_assert.c
+++ b/tests/spec/behavior_assert.c
@@ -1,8 +1,8 @@
/* run.config
-OPT: -eva @EVA_CONFIG@ -deps -out -input -journal-disable -lib-entry
-OPT: -eva @EVA_CONFIG@ -deps -out -input -journal-disable
+PLUGIN: eva,from,inout,scope
+ OPT: -eva @EVA_CONFIG@ -deps -out -input -journal-disable -lib-entry
+ OPT: -eva @EVA_CONFIG@ -deps -out -input -journal-disable
*/
-
int e;
/*@
diff --git a/tests/spec/default_assigns_bts0966.i b/tests/spec/default_assigns_bts0966.i
index 6b4cd671eda66ecb86c8a548620127b06604a1e6..4e2abccd49e698ad4aa3fc57c1e3c48b5556d250 100644
--- a/tests/spec/default_assigns_bts0966.i
+++ b/tests/spec/default_assigns_bts0966.i
@@ -1,7 +1,7 @@
/* run.config
+PLUGIN: eva,scope
OPT: -eva -print
*/
-
int auto_states[4] ; // = { 1 , 0 , 0, 0 };
enum states {
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index 06f74139cfb7854ec517df292b9ca720dbd9ceed..ec9786ea47fe132077767e2b02ceda89f6849843 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -1,10 +1,10 @@
/* run.config
-OPT: -eva -eva-use-spec f
-OPT: -print
+PLUGIN: eva,scope
+ OPT: -eva -eva-use-spec f
+PLUGIN:
+ OPT: -print
*/
-
/*@ check lemma easy_proof: \false; */ // should not be put in any environment
-
/*@ check requires f_valid_x: \valid(x);
assigns *x;
check ensures f_init_x: *x == 0;
diff --git a/tests/spec/kw.c b/tests/spec/kw.c
index e57a4869f38f02d6bb9c79f6e7c7b1b7139b50fc..c780af02c9dc6fbc09f6badafd206db025676aa0 100644
--- a/tests/spec/kw.c
+++ b/tests/spec/kw.c
@@ -1,3 +1,9 @@
+/* run.config
+COMMENT: eva plugin is required for the slevel annotation
+PLUGIN: eva
+ STDOPT:
+*/
+
typedef int assert;
assert behavior = 0;
diff --git a/tests/spec/logic_def.c b/tests/spec/logic_def.c
index a9050410d76999cd48d4168575d26b22c5760e8d..c01bfb9e61297a6a281ab144bdd7c3524a753d9a 100644
--- a/tests/spec/logic_def.c
+++ b/tests/spec/logic_def.c
@@ -1,7 +1,7 @@
/* run.config
+PLUGIN: eva,scope
STDOPT: +"-eva -eva-verbose 2"
*/
-
//@ logic integer foo(int x) = x + 2 ;
int main() {
diff --git a/tests/spec/oracle/assigns_void.0.res.oracle b/tests/spec/oracle/assigns_void.0.res.oracle
index ad68c8cfaa692fac538086d5a4969b433d91fff7..4e730b46a501a71788c2a543b438e9ad4922a0dc 100644
--- a/tests/spec/oracle/assigns_void.0.res.oracle
+++ b/tests/spec/oracle/assigns_void.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/spec/assigns_void.c (with preprocessing)
-[kernel:annot-error] tests/spec/assigns_void.c:5: Warning:
+[kernel:annot-error] tests/spec/assigns_void.c:6: Warning:
Cannot use a pointer to void here. Ignoring specification of function f
/* Generated by Frama-C */
void f(void *x);
diff --git a/tests/spec/oracle/statement_behavior.res.oracle b/tests/spec/oracle/statement_behavior.res.oracle
index 355b543903f30f9c0f17481e84bf35b15329bd6a..75f55931501876f76e9cd706ac8856116d8a50ec 100644
--- a/tests/spec/oracle/statement_behavior.res.oracle
+++ b/tests/spec/oracle/statement_behavior.res.oracle
@@ -10,7 +10,7 @@
no \from part for clause 'assigns five_times;'
[eva:alarm] tests/spec/statement_behavior.c:17: Warning:
assertion got status unknown.
-[eva:alarm] tests/spec/statement_behavior.c:4: Warning:
+[eva:alarm] tests/spec/statement_behavior.c:5: Warning:
function pfsqopfc: postcondition got status unknown.
[eva:alarm] tests/spec/statement_behavior.c:18: Warning:
accessing uninitialized left-value. assert \initialized(&five_times);
diff --git a/tests/spec/preprocess.c b/tests/spec/preprocess.c
index 64b0e62aeec278a03dfd822ddc33e5f539566b1f..5047548c8ecacacc9a172e81fc4cd7f069841aa2 100644
--- a/tests/spec/preprocess.c
+++ b/tests/spec/preprocess.c
@@ -1,7 +1,7 @@
/* run.config
- OPT: -eva @EVA_CONFIG@ -journal-disable -print
+PLUGIN: eva,scope
+ OPT: -eva @EVA_CONFIG@ -print
*/
-
// see bts 1357
#define assert(x) (x)?1:0
diff --git a/tests/spec/shifts.c b/tests/spec/shifts.c
index a7d934e68da3bb28a16e8b0922eb34cc823694dc..5979c3d67ff3dc7feb1a1da0a3728bef50dc1ab6 100644
--- a/tests/spec/shifts.c
+++ b/tests/spec/shifts.c
@@ -1,7 +1,7 @@
/* run.config
- OPT: -eva @EVA_CONFIG@ -deps -journal-disable
+PLUGIN: eva,scope,from
+ OPT: -eva @EVA_CONFIG@ -deps
*/
-
int e;
/*@
diff --git a/tests/spec/statement_behavior.c b/tests/spec/statement_behavior.c
index e91bc04723652701f7477a479ac8abf29fbacac5..c8834f72c8ea2102631e6060ac6dc0c3acc9cc3c 100644
--- a/tests/spec/statement_behavior.c
+++ b/tests/spec/statement_behavior.c
@@ -1,11 +1,11 @@
/* run.config
- OPT: -eva @EVA_CONFIG@ -inout -journal-disable
+PLUGIN: eva,inout,scope
+ OPT: -eva @EVA_CONFIG@ -inout
*/
/*@ ensures \result == (int)(5 * x);
*/
int pfsqopfc(int x) {
int five_times;
-
/*@
assigns five_times;
ensures five_times == (int)(5 * x);
diff --git a/tests/syntax/Refresh_visitor.i b/tests/syntax/Refresh_visitor.i
index 6bf2f55e42ef1cd1009a5f8de7b7962f3349a710..c1d19f0a1d62fa1dd8b3d2f9befaaf2872fd4b25 100644
--- a/tests/syntax/Refresh_visitor.i
+++ b/tests/syntax/Refresh_visitor.i
@@ -1,8 +1,8 @@
/* run.config
+ PLUGIN: eva,scope
MODULE: @PTEST_NAME@
OPT: @EVA_OPTIONS@
*/
-
struct S { int i; };
/*@ lemma foo: \forall struct S x; x.i >= 0 || x.i < 0; */
diff --git a/tests/syntax/char_is_unsigned.i b/tests/syntax/char_is_unsigned.i
index 771ea26e6800c6fac56c23f00561be16aeda4fce..02a2088fef3e3a4aa038f1bd41a176bd45e36cf1 100644
--- a/tests/syntax/char_is_unsigned.i
+++ b/tests/syntax/char_is_unsigned.i
@@ -1,6 +1,7 @@
/* run.config
+PLUGIN: rtegen
MODULE: machdep_char_unsigned
- OPT:-print -machdep unsigned_char -then -constfold -rte
+ OPT: -print -machdep unsigned_char -then -constfold -rte
*/
char t[10];
diff --git a/tests/syntax/copy_logic.i b/tests/syntax/copy_logic.i
index 271bdce7af4fbd5e66c5393e3a7078be00677bbc..fee16b6120468fa4170798dc4290114348c9ee3d 100644
--- a/tests/syntax/copy_logic.i
+++ b/tests/syntax/copy_logic.i
@@ -1,7 +1,7 @@
/* run.config
+PLUGIN: eva,scope
STDOPT: +"-copy" +"-eva"
*/
-
/*@ predicate p(int x); */
/*@ predicate q(int x) = x == 42; */
/*@ logic int f (int y); */
diff --git a/tests/syntax/copy_visitor.i b/tests/syntax/copy_visitor.i
index 2f475d79ae7a5ebeaf572e79e97e4b5f533cc833..d2d4bdb124e786dd2ee04327d9803b86b6c3dbe7 100644
--- a/tests/syntax/copy_visitor.i
+++ b/tests/syntax/copy_visitor.i
@@ -1,4 +1,5 @@
/* run.config
+PLUGIN: eva,scope
STDOPT: +"-copy -eva @EVA_CONFIG@"
*/
struct S {
@@ -6,7 +7,6 @@ struct S {
int b;
};
struct S s = {.a = 1, .b=2};
-
/*@
requires \valid(s);
assigns s->a;
diff --git a/tests/syntax/copy_visitor_bts_1073.c b/tests/syntax/copy_visitor_bts_1073.c
index ec7e1ab180571bc3edbdc5ddafa90c2a602d0b21..e028f3cbe4d7e4d22d360e84786dad8c073e43e7 100644
--- a/tests/syntax/copy_visitor_bts_1073.c
+++ b/tests/syntax/copy_visitor_bts_1073.c
@@ -1,10 +1,10 @@
/* run.config
+PLUGIN: variadic
MODULE: @PTEST_NAME@
OPT:
MODULE: @PTEST_NAME@_bis
OPT: -test -then-on filtered -print
*/
-
#include "stdio.h"
int f(int x);
diff --git a/tests/syntax/cpp-command.c b/tests/syntax/cpp-command.c
index 3b9d41a71f080ea682cbc3482fa8412e53af2064..48585271169f5f929f117075c3011689e3011168 100644
--- a/tests/syntax/cpp-command.c
+++ b/tests/syntax/cpp-command.c
@@ -1,10 +1,10 @@
/* run.config*
FILTER: sed "s:/[^ ]*[/]cpp-command\.[^ ]*\.i:TMPDIR/FILE.i:g; s:$PWD/::g; s: -m32::"
- OPT: -machdep x86_32 -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']"
- OPT: -machdep x86_32 -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'"
- OPT: -machdep x86_32 -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "printf \"%s\n\" \"using \\% has no effect : \$(basename \"\%input\")\""
- OPT: -machdep x86_32 -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %var is not an interpreted placeholder"
- OPT: -machdep x86_32 -no-autoload-plugins -print-cpp-commands
+ OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']"
+ OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'"
+ OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "printf \"%s\n\" \"using \\% has no effect : \$(basename \"\%input\")\""
+ OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo %var is not an interpreted placeholder"
+ OPT: -machdep x86_32 -print-cpp-commands
OPT: -cpp-extra-args-per-file=@PTEST_FILE@:"-DPF=\\\"cp%02d_3f\\\"" -no-autoload-plugins @PTEST_FILE@ -print
*/
diff --git a/tests/syntax/extern_init.i b/tests/syntax/extern_init.i
index e6773ed70089a517ab8a9499fbeb5b1b49304902..37a97faef54b721dcfc5c135e34f9c294e4c7235 100644
--- a/tests/syntax/extern_init.i
+++ b/tests/syntax/extern_init.i
@@ -1,7 +1,9 @@
/* run.config
+PLUGIN: eva,scope
OPT: @PTEST_DIR@/@PTEST_NAME@_1.i @PTEST_DIR@/@PTEST_NAME@_2.i -eva @EVA_CONFIG@
OPT: @PTEST_DIR@/@PTEST_NAME@_2.i @PTEST_DIR@/@PTEST_NAME@_1.i -eva @EVA_CONFIG@
*/
+
extern int a[] ;
/*@ assigns a[3] \from \nothing; */
diff --git a/tests/syntax/fct_ptr.i b/tests/syntax/fct_ptr.i
index 6b64b57479349ea4bb49e98aba19bcfce06789d3..63a57c55fdf6f3f53de8efb85cf41aa2a6aad003 100644
--- a/tests/syntax/fct_ptr.i
+++ b/tests/syntax/fct_ptr.i
@@ -1,20 +1,20 @@
-int f(int);
+/* run.config
+ PLUGIN: variadic
+ STDOPT:
+*/
+int f(int);
void *p = f;
-
int (*pf) (int x) = f;
-
int g() {
return ((int (*)(int))(*pf))(4);
}
-
int main () {
int (*q)(int) = (void *)0xfff45;
q(2);
q = p;
q(3);
}
-
typedef int (*Function_ptr)();
char *f_va(int a, ...) { return a; }
Function_ptr fp_table[1] = {(Function_ptr) f_va}; // warning, but no error
diff --git a/tests/syntax/function-types-compatible.i b/tests/syntax/function-types-compatible.i
index 770198b5691b45604630bd53effc937be6319407..a02b6ba9d748b2b9d10446148b7c43fd3f65c2bd 100644
--- a/tests/syntax/function-types-compatible.i
+++ b/tests/syntax/function-types-compatible.i
@@ -1,5 +1,12 @@
+/* run.config
+PLUGIN: variadic
+STDOPT:
+*/
+
void (*p)(int, ...);
+
void f();
+
void main() {
p = f;
p(1, 2); // warning, but no parsing error; will fail during execution
diff --git a/tests/syntax/gcc_builtins.c b/tests/syntax/gcc_builtins.c
index 00a9054c8b191a212b70e1b5000c4b710c4984ae..db5d0e38bdd1c27bea62b457f061eacbdb2c3211 100644
--- a/tests/syntax/gcc_builtins.c
+++ b/tests/syntax/gcc_builtins.c
@@ -1,7 +1,7 @@
/* run.config
+ PLUGIN: variadic
STDOPT: +"-machdep gcc_x86_32"
*/
-
#include "stdint.h"
#define likely(x) __builtin_expect((x),1)
diff --git a/tests/syntax/inline_calls.i b/tests/syntax/inline_calls.i
index a71073677d14b7d1b989f2d667f54b3d2bb917ac..4cf6b9c05992ba6000408bbe11dde27f4ad4bda0 100644
--- a/tests/syntax/inline_calls.i
+++ b/tests/syntax/inline_calls.i
@@ -1,9 +1,9 @@
/* run.config
+PLUGIN: eva,scope
STDOPT: +"-inline-calls @all -kernel-msg-key printer:attrs"
STDOPT: +"-inline-calls @inline"
STDOPT: +"-inline-calls @inline -remove-inlined @inline"
*/
-
int f() {
return 2;
}
diff --git a/tests/syntax/local-init-const.i b/tests/syntax/local-init-const.i
index 1d79724df761cbe3b412972bc0fb43c3fd156ea1..09793138d4693239a17072a39327874320e9e4ff 100644
--- a/tests/syntax/local-init-const.i
+++ b/tests/syntax/local-init-const.i
@@ -1,6 +1,8 @@
/*run.config
- OPT: -no-autoload-plugins -load-module eva,scope -eva -eva-verbose 0
+PLUGIN: eva,scope
+ OPT: -eva -eva-verbose 0
*/
+
unsigned id(unsigned x) { return x; }
void main() {
diff --git a/tests/syntax/loop-case-switch-for-unroll.c b/tests/syntax/loop-case-switch-for-unroll.c
index 7785be51b6a9e2495750bee02becb6c8fd846b61..3052cb9f5529fa6a77d6763f81aaee4673598cbd 100644
--- a/tests/syntax/loop-case-switch-for-unroll.c
+++ b/tests/syntax/loop-case-switch-for-unroll.c
@@ -1,4 +1,5 @@
/* run.config
+PLUGIN: eva,scope
STDOPT: +"-eva-slevel 100 -eva"
STDOPT: +"-ulevel 1 -eva-slevel 100 -eva"
STDOPT: +"-ulevel 2 -eva-slevel 100 -eva"
@@ -6,7 +7,6 @@
the result of Frama-C piped to:
"| grep Frama_C_show_each | sed 's/^.*Frama_C_show_each_//'"
*/
-
#ifdef __FRAMAC__
#define print(line, s, a) Frama_C_show_each_ ## s ## _(a)
#else
diff --git a/tests/syntax/merge_variadic.i b/tests/syntax/merge_variadic.i
index dab33541e614a5c024f194ca824c8de30c0ffea6..b296224e959149e92dd12a8136ea5ed89d60076d 100644
--- a/tests/syntax/merge_variadic.i
+++ b/tests/syntax/merge_variadic.i
@@ -1,9 +1,9 @@
/* run.config
-OPT: @PTEST_DIR@/@PTEST_NAME@_aux.i -print
+PLUGIN: variadic
+ OPT: @PTEST_DIR@/@PTEST_NAME@_aux.i -print
*/
int open (const char* file, int flags, int mode) {
return -1;
}
-
/*@ assigns \result \from x; */
int foo (int x, int y);
diff --git a/tests/syntax/oracle/bts1553_2.res.oracle b/tests/syntax/oracle/bts1553_2.res.oracle
index 93dacee514969b19d8bc20ff47fcaffdd2a4c526..9293259fe565811c4e9f7f6dedc355b38faa4288 100644
--- a/tests/syntax/oracle/bts1553_2.res.oracle
+++ b/tests/syntax/oracle/bts1553_2.res.oracle
@@ -5,8 +5,6 @@
struct a {
int b ;
};
- /* compiler builtin:
- void Frama_C_show_aorai_state(...); */
/* compiler builtin:
__builtin_va_list __builtin_next_arg(void); */
/* compiler builtin:
@@ -42,8 +40,6 @@
struct a {
int b ;
};
- /* compiler builtin:
- void Frama_C_show_aorai_state(...); */
/* compiler builtin:
__builtin_va_list __builtin_next_arg(void); */
/* compiler builtin:
diff --git a/tests/syntax/oracle/check_builtin_bts1440.res.oracle b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
index f81e5813ccc1c324160bc8600bf6e042c3e3fbbd..510a8f2b3ab41a3c39cd5c26cc41c8703528b9e1 100644
--- a/tests/syntax/oracle/check_builtin_bts1440.res.oracle
+++ b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
@@ -2,8 +2,6 @@
[kernel:file:print-one]
result of parsing tests/syntax/check_builtin_bts1440.i:
/* Generated by Frama-C */
- void Frama_C_show_aorai_state(...);
-
void __builtin__Exit(int);
int __builtin___fprintf_chk(void *, int, char const * , ...);
diff --git a/tests/syntax/oracle/function-types-compatible.res.oracle b/tests/syntax/oracle/function-types-compatible.res.oracle
index 121d63a24e7721aba55611f25c673bf25953f32f..b25ea3698a6a3dd2d6995d583b96a878368f2cda 100644
--- a/tests/syntax/oracle/function-types-compatible.res.oracle
+++ b/tests/syntax/oracle/function-types-compatible.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/function-types-compatible.i (no preprocessing)
-[kernel:typing:incompatible-types-call] tests/syntax/function-types-compatible.i:4: Warning:
+[kernel:typing:incompatible-types-call] tests/syntax/function-types-compatible.i:11: Warning:
implicit conversion between incompatible function types:
void (*)()
and
diff --git a/tests/syntax/oracle/merge_variadic.res.oracle b/tests/syntax/oracle/merge_variadic.res.oracle
index 88885da35e2f84e1f548dd833903435f798a8958..a0c39aecf62846a1e8877d3a78f32647a8704355 100644
--- a/tests/syntax/oracle/merge_variadic.res.oracle
+++ b/tests/syntax/oracle/merge_variadic.res.oracle
@@ -3,7 +3,7 @@
[kernel:linker:drop-conflicting-unused] Warning:
Incompatible declaration for open:
different vararg specifiers
- First declaration was at tests/syntax/merge_variadic.i:4
+ First declaration was at tests/syntax/merge_variadic.i:5
Current declaration is at tests/syntax/merge_variadic_aux.i:5
Current declaration is unused, silently removing it
[kernel:linker:drop-conflicting-unused] Warning:
diff --git a/tests/syntax/oracle/static_formals_1.res.oracle b/tests/syntax/oracle/static_formals_1.res.oracle
index f3dc98b3d3003fb066ecc0db86d86140b90ce85c..6261380034edbdbaf53954bee958450e2f36d238 100644
--- a/tests/syntax/oracle/static_formals_1.res.oracle
+++ b/tests/syntax/oracle/static_formals_1.res.oracle
@@ -1,24 +1,24 @@
[kernel] Parsing tests/syntax/static_formals_1.c (with preprocessing)
[kernel] Parsing tests/syntax/static_formals_2.c (with preprocessing)
/* Generated by Frama-C */
-/*@ requires /* vid:26, lvid:26 */x < 10; */
-static int /* vid:60 */f(int /* vid:26, lvid:26 */x);
+/*@ requires /* vid:23, lvid:23 */x < 10; */
+static int /* vid:56 */f(int /* vid:23, lvid:23 */x);
-int /* vid:31 */g(void)
+int /* vid:28 */g(void)
{
- int /* vid:32 */tmp;
- /* vid:32 */tmp = /* vid:60 */f(4);
- return /* vid:32 */tmp;
+ int /* vid:29 */tmp;
+ /* vid:29 */tmp = /* vid:56 */f(4);
+ return /* vid:29 */tmp;
}
-/*@ requires /* vid:55, lvid:55 */x < 10; */
-static int /* vid:61 */f_0(int /* vid:55, lvid:55 */x);
+/*@ requires /* vid:51, lvid:51 */x < 10; */
+static int /* vid:57 */f_0(int /* vid:51, lvid:51 */x);
-int /* vid:58 */h(void)
+int /* vid:54 */h(void)
{
- int /* vid:59 */tmp;
- /* vid:59 */tmp = /* vid:61 */f_0(6);
- return /* vid:59 */tmp;
+ int /* vid:55 */tmp;
+ /* vid:55 */tmp = /* vid:57 */f_0(6);
+ return /* vid:55 */tmp;
}
diff --git a/tests/syntax/oracle/unroll_visit.res.oracle b/tests/syntax/oracle/unroll_visit.res.oracle
index 271518ba4c2d9a67a2fd616ca5818cbe5d4818b3..1679a9dc5d55a5b96376f47c9800d9501192aa9e 100644
--- a/tests/syntax/oracle/unroll_visit.res.oracle
+++ b/tests/syntax/oracle/unroll_visit.res.oracle
@@ -4,8 +4,8 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/syntax/unroll_visit.i:9: assertion got status valid.
-[eva] tests/syntax/unroll_visit.i:7: starting to merge loop iterations
+[eva] tests/syntax/unroll_visit.i:12: assertion got status valid.
+[eva] tests/syntax/unroll_visit.i:10: starting to merge loop iterations
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/syntax/oracle/variadic.res.oracle b/tests/syntax/oracle/variadic.res.oracle
index 9e0223986f0000922185c919e1881cb0f45c1bca..1052103bac84ae187ec185f26ae494a81c58d95d 100644
--- a/tests/syntax/oracle/variadic.res.oracle
+++ b/tests/syntax/oracle/variadic.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/syntax/variadic.i (no preprocessing)
-[kernel:typing:implicit-function-declaration] tests/syntax/variadic.i:20: Warning:
+[kernel:typing:implicit-function-declaration] tests/syntax/variadic.i:26: Warning:
Calling undeclared function f. Old style K&R code?
-[kernel:typing:no-proto] tests/syntax/variadic.i:21: Warning:
+[kernel:typing:no-proto] tests/syntax/variadic.i:27: Warning:
Calling function h that is declared without prototype.
Its formals will be inferred from actual arguments
/* Generated by Frama-C */
diff --git a/tests/syntax/static_formals_1.c b/tests/syntax/static_formals_1.c
index 6cd8687eba15553886326158692c69839fd4e061..97cfbca9a65701a0dfebf4cab8f8550af431ebbf 100644
--- a/tests/syntax/static_formals_1.c
+++ b/tests/syntax/static_formals_1.c
@@ -1,7 +1,6 @@
/* run.config
STDOPT: +"@PTEST_DIR@/static_formals_2.c" +"-cpp-extra-args=\"-I @PTEST_DIR@\"" +"-kernel-msg-key printer:vid"
*/
-
#include "static_formals.h"
int g() { return f(4); }
diff --git a/tests/syntax/string_concat.c b/tests/syntax/string_concat.c
index 924e8b423c7f30720939ddfb15b23b5c78ddc01b..b78a7d85590f3c5981b36737e9d20ec207dc0aad 100644
--- a/tests/syntax/string_concat.c
+++ b/tests/syntax/string_concat.c
@@ -1,4 +1,5 @@
/* run.config*
+PLUGIN: eva,scope variadic
TIMEOUT: 600
OPT: -eva
*/
diff --git a/tests/syntax/test_config b/tests/syntax/test_config
index df749c62084f1dff34265d08aa76546e4a89949e..3d75cb1ea823f0885cd7c5d9e4be187df1b0b67d 100644
--- a/tests/syntax/test_config
+++ b/tests/syntax/test_config
@@ -1,4 +1,5 @@
COMMENT: this directory is meant to test exclusively the front-end
COMMENT: (parser, type-checker, linker, syntactic transformations)
-OPT: -print -journal-disable -check -machdep x86_32
+PLUGIN:
+OPT: -print -machdep x86_32
FILEREG:.*\.\(c\|i\|ci\)$
diff --git a/tests/syntax/unroll_labels.i b/tests/syntax/unroll_labels.i
index 66da8b7cf4882b0214a9cc46294e20ff7f81668b..4fcef3f5d46dfd9784cf49c16fa8fbe38b7c99f4 100644
--- a/tests/syntax/unroll_labels.i
+++ b/tests/syntax/unroll_labels.i
@@ -1,10 +1,10 @@
/* run.config
+PLUGIN: eva,scope
STDOPT: +"-eva @EVA_CONFIG@"
STDOPT: +"-eva @EVA_CONFIG@ -main main2 -eva-slevel 3"
*/
enum { SIX = 6 } ;
volatile foo;
-
void main () {
int j = 0;
/*@ loop pragma UNROLL "completely", 4; */
diff --git a/tests/syntax/unroll_property_status_bts1442.i b/tests/syntax/unroll_property_status_bts1442.i
index 70ac3a9bbafb983c076f2aa1f3b6960753d24444..0a8970b5b8990d77268c0b7a7e2b8d8f54512e28 100644
--- a/tests/syntax/unroll_property_status_bts1442.i
+++ b/tests/syntax/unroll_property_status_bts1442.i
@@ -1,8 +1,8 @@
/* run.config
-OPT: -report
-OPT: -ulevel -1 -report
+PLUGIN: report
+ OPT: -report
+ OPT: -ulevel -1 -report
*/
-
int u(void);
char *strcpy(char*dst, char*src) {
diff --git a/tests/syntax/unroll_visit.i b/tests/syntax/unroll_visit.i
index 495b3bd0c50ce064137350a98b95406b6d5ed3ff..f4d949c53ef9a94e93a366b61bbb2a14caf8356c 100644
--- a/tests/syntax/unroll_visit.i
+++ b/tests/syntax/unroll_visit.i
@@ -1,7 +1,10 @@
/* run.config
+PLUGIN: eva,scope,from,inout
STDOPT: +"-eva @EVA_CONFIG@ -deps -out -input -deps"
*/
+
typedef char i8; // ideally, pretty-printing should keep 'i8' for some casts
+
void main() {
/*@ loop pragma UNROLL 2; */
for(i8 i=0; i<100; i++) {
diff --git a/tests/syntax/variadic.i b/tests/syntax/variadic.i
index b07b22acab044134cb870e6860a21a96783784ab..fc23e732c0c17b9d7407c4a07236490a6a0dc62d 100644
--- a/tests/syntax/variadic.i
+++ b/tests/syntax/variadic.i
@@ -1,8 +1,14 @@
+/* run.config
+ PLUGIN: variadic
+ STDOPT:
+*/
int normal(int n);
int vf(int x, ...);
+
typedef char tt;
struct T {int a;} st;
+
tt abstract;
unsigned char uchar;
signed char chr;
@@ -14,7 +20,7 @@ double d;
void h();
void g() {
- vf(1,1u,uchar,3.0f, ushort, ll, abstract, st, ld,d);
+ vf(1,1u,uchar,3.0f, ushort, ll, abstract, st, ld,d);
// vf() is variadic: the default argument promotions apply after the initial
// arguments. C99 6.5.2.2:7
f(1,uchar); // f undeclared, default argument promotions apply C99 6.5.2.2:6
diff --git a/tests/syntax/wstring_concat.c b/tests/syntax/wstring_concat.c
index 76f68ddd1b187f24f22591786cda9f13ce1a8209..9bd6571dd63b901380598f6dc29c9b769f8f6f24 100644
--- a/tests/syntax/wstring_concat.c
+++ b/tests/syntax/wstring_concat.c
@@ -1,8 +1,8 @@
/* run.config*
+PLUGIN: eva,scope,variadic
TIMEOUT: 600
OPT: -eva
*/
-
#include <wchar.h>
#include <stdio.h>
diff --git a/tests/test_config b/tests/test_config
index 11d75bf850c7c2f65ff98bf5fd486ec47200f499..f188ff4072509a1f23ce78441acaac71a8d02cf9 100644
--- a/tests/test_config
+++ b/tests/test_config
@@ -1,3 +1,6 @@
+MACRO: EVA_PLUGINS from,inout,eva,scope,variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
-OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
+
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -out -input -deps
diff --git a/tests/test_config_apron b/tests/test_config_apron
index ff3a028903375e622d271ae85a070bdad02df8cb..411673ceafcafde7b9e20b8a40abe841a1cbd1a5 100644
--- a/tests/test_config_apron
+++ b/tests/test_config_apron
@@ -1,7 +1,9 @@
+MACRO: EVA_PLUGINS from,inout,eva,scope,variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains apron-octagon -eva-warn-key experimental=inactive
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
# Compare the result with the oracle of the default config.
FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
-OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -out -input -deps
diff --git a/tests/test_config_bitwise b/tests/test_config_bitwise
index 103334223c75fc4d7ef5faadd2187fd3913defbf..19dd5d40c9f00151a44d21a20b5cb797d1c1fe6c 100644
--- a/tests/test_config_bitwise
+++ b/tests/test_config_bitwise
@@ -1,3 +1,4 @@
+MACRO: EVA_PLUGINS from,inout,eva,scope,variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains bitwise
MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
diff --git a/tests/test_config_equality b/tests/test_config_equality
index ffa23c9d32dac550f13db32f54185a48c1b3772e..fff8c6fb43f010c4d22835dbf0a4e5c43f2a249f 100644
--- a/tests/test_config_equality
+++ b/tests/test_config_equality
@@ -1,7 +1,9 @@
+MACRO: EVA_PLUGINS from,inout,eva,scope,variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains equality
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
# Compare the result with the oracle of the default config.
FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
-OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -out -input -deps
diff --git a/tests/test_config_gauges b/tests/test_config_gauges
index 2c04eba2c74acdaa705e8dc6437b577266183d32..37ea7dfeb18c677bbb3d58d199a4d7030cd5dcac 100644
--- a/tests/test_config_gauges
+++ b/tests/test_config_gauges
@@ -1,7 +1,9 @@
+MACRO: EVA_PLUGINS from,inout,eva,scope,variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains gauges
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
# Compare the result with the oracle of the default config.
FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
-OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -out -input -deps
diff --git a/tests/test_config_octagon b/tests/test_config_octagon
index c3f170e9652940aae572fa469a014cb5da8baf23..a63c091418a391a00eee6a9f0bb681358a49d7c5 100644
--- a/tests/test_config_octagon
+++ b/tests/test_config_octagon
@@ -1,7 +1,9 @@
+MACRO: EVA_PLUGINS from,inout,eva,scope,variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-domains octagon
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
# Compare the result with the oracle of the default config.
FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
-OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -out -input -deps
diff --git a/tests/test_config_symblocs b/tests/test_config_symblocs
index d25a43c5eb7a0aeff3b6cddcdda469a1433ba638..3b082f3869cd61f8bb7baf1944ea34ca3eb2e66f 100644
--- a/tests/test_config_symblocs
+++ b/tests/test_config_symblocs
@@ -1,7 +1,9 @@
+MACRO: EVA_PLUGINS from,inout,eva,scope,variadic
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains symbolic-locations
-MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
# Compare the result with the oracle of the default config.
FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
-OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
+PLUGIN: @EVA_PLUGINS@
+OPT: -eva @EVA_CONFIG@ -out -input -deps