Skip to content
Snippets Groups Projects
Commit adeba428 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[devman] fix formatting

parent f884b76a
No related branches found
No related tags found
No related merge requests found
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
%%MODERN \documentclass[a4paper,11pt,twoside,openright]{report} %%MODERN \documentclass[a4paper,11pt,twoside,openright]{report}
\documentclass[web,svgnames]{frama-c-book} \documentclass[web,svgnames]{frama-c-book}
\usepackage{xspace,alltt,calc,multirow,tabularx,bigdelim} \usepackage{xspace,alltt,calc,multirow,tabularx,bigdelim,spverbatim}
\usepackage{amsmath} \usepackage{amsmath}
\IfFileExists{diagbox.sty} % Compatibility with newer diagbox and older slashbox \IfFileExists{diagbox.sty} % Compatibility with newer diagbox and older slashbox
{\usepackage{diagbox} {\usepackage{diagbox}
......
...@@ -842,7 +842,7 @@ to your needs. See \texttt{ocamlmerlin -help} for the list of flags. ...@@ -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. Ptests pre-defines a certain number of macros for each test about to be run.
Figure~\ref{fig:ptests-macros} gives their definition. Figure~\ref{fig:ptests-macros} gives their definition.
\begin{figure}[htbp] \begin{figure}[htbp]
\begin{tabular}{|p{3cm}|p{10cm}|} \begin{tabular}{|p{4.5cm}|p{10cm}|}
\hline \hline
Name & Expansion \\ Name & Expansion \\
\hline \hline
...@@ -865,29 +865,29 @@ fact two independent numbering schemes: one for \verb|EXECNOW| commands and ...@@ -865,29 +865,29 @@ fact two independent numbering schemes: one for \verb|EXECNOW| commands and
one for regular tests (if more than one \verb|OPT|).\\ one for regular tests (if more than one \verb|OPT|).\\
\hline \hline
\verb|PTEST_RESULT| & shorthand alias to \verb|@PTEST_DIR@/result@PTEST_CONFIG@| \verb|PTEST_RESULT| & shorthand alias to \verb|@PTEST_DIR@/result@PTEST_CONFIG@|
(the result directory dedicated to the tested configuration) (the result directory dedicated to the tested configuration)\\
\hline \hline
\verb|@PTEST_ORACLE| & basename of the current oracle file (macro only usable in FILTER directives) \verb|PTEST_ORACLE| & basename of the current oracle file (macro only usable in FILTER directives)\\
\hline \hline
\verb|PTEST_MODULE| & current list of module defined by the \verb|MODULE| directive \verb|PTEST_MODULE| & current list of module defined by the \verb|MODULE| directive\\
\hline \hline
\verb|PTEST_PLUGIN| & current list of plugins defined by the \verb|PLUGIN| directive \verb|PTEST_PLUGIN| & current list of plugins defined by the \verb|PLUGIN| directive\\
\hline \hline
\verb|PTEST_DEFAULT_OPTIONS| & the default option list: \verb|-journal-disable| \verb|-check| \verb|-no-autoload-plugins| \verb|PTEST_DEFAULT_OPTIONS| & the default option list: \verb|-journal-disable| \verb|-check| \verb|-no-autoload-plugins|\\
\hline \hline
\verb|PTEST_LOAD_MODULE| & the \verb|-load-module| option related to the \verb|MODULE| directive \verb|PTEST_LOAD_MODULE| & the \verb|-load-module| option related to the \verb|MODULE| directive\\
\hline \hline
\verb|PTEST_LOAD_PLUGIN| & the \verb|-load-module| option related to the \verb|PLUGIN| directive \verb|PTEST_LOAD_PLUGIN| & the \verb|-load-module| option related to the \verb|PLUGIN| directive\\
\hline \hline
\verb|PTEST_LOAD_OPTIONS| & shorthand alias to \verb|@PTEST_LOAD_PLUGIN@ @PTEST_LOAD_MODULE@| \verb|PTEST_LOAD_OPTIONS| & shorthand alias to \spverb|@PTEST_LOAD_PLUGIN@ @PTEST_LOAD_MODULE@|\\
\hline \hline
\verb|PTEST_OPTIONS| & the current list of options related to \verb|OPT| and \verb|STDOPT| directives (for \verb|CMD| directives) \verb|PTEST_OPTIONS| & the current list of options related to \verb|OPT| and \verb|STDOPT| directives (for \verb|CMD| directives)\\
\hline \hline
\verb|frama-c| & shortcut defined as follow: \verb|@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@| \verb|frama-c| & shortcut defined as follows: \spverb|@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@|\\
\hline \hline
\verb|frama-c-cmd| & shortcut defined as follow: \verb|@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@| \verb|frama-c-cmd| & shortcut defined as follows: \spverb|@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@|\\
\hline \hline
\verb|frama-c-exe| & set to the value of the \verb|TOPLEVEL_PATH| variable from \verb|./tests/ptests_config| file \verb|frama-c-exe| & set to the value of the \verb|TOPLEVEL_PATH| variable from \verb|./tests/ptests_config| file\\
\hline \hline
\end{tabular} \end{tabular}
\caption{Predefined macros for ptests}\label{fig:ptests-macros} \caption{Predefined macros for ptests}\label{fig:ptests-macros}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment