Skip to content
Snippets Groups Projects
Commit 257a6b46 authored by Patrick Baudin's avatar Patrick Baudin Committed by Virgile Prevosto
Browse files

[Ptests] update doc

parent 94a79991
No related branches found
No related tags found
No related merge requests found
...@@ -954,13 +954,17 @@ the configuration header of a test (or a test suite). ...@@ -954,13 +954,17 @@ the configuration header of a test (or a test suite).
\textbf{Kind} & \textbf{Name} & \textbf{Specification} & \textbf{default}\\ \textbf{Kind} & \textbf{Name} & \textbf{Specification} & \textbf{default}\\
\hline \hline
\hline \multirow{4}{23mm}{\centering{Command}} \hline \multirow{4}{23mm}{\centering{Command}}
& \texttt{PLUGIN}\nscodeidxdef{Test!Directive}{PLUGIN}
& Plugins to be loaded with each subsequent
& \texttt{from,inout,eva,scope,variadic} for tests under \texttt{./tests} directory
\\
& \texttt{CMD}\nscodeidxdef{Test!Directive}{CMD} & \texttt{CMD}\nscodeidxdef{Test!Directive}{CMD}
& Program to run & Program to run
& \texttt{./bin/toplevel.opt} & \texttt{./bin/toplevel.opt}
\\ \\
& \texttt{OPT}\nscodeidxdef{Test!Directive}{OPT} & \texttt{OPT}\nscodeidxdef{Test!Directive}{OPT}
& Options given to the program & 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} & \texttt{STDOPT}\nscodeidxdef{Test!Directive}{STDOPT}
& Add and remove options from the default set & Add and remove options from the default set
......
...@@ -318,19 +318,33 @@ let example_msg = ...@@ -318,19 +318,33 @@ let example_msg =
MACRO: <name> <def> @[<v 0># Set a definition to the macro @@<name>@@.@]@ \ MACRO: <name> <def> @[<v 0># Set a definition to the macro @@<name>@@.@]@ \
@]@ \ @]@ \
@[<v 1>\ @[<v 1>\
Some predefined macros can be used in test commands:@ \ Default directive values:@ \
@@PTEST_DIR@@ # Dirname of the test file.@ \ FILEREG: %s@ \
@@PTEST_FILE@@ # Substituted by the test filename.@ \ CMD: %s@ \
@@PTEST_NAME@@ # Basename of the test file.@ \ EXIT: 0@ \
@@PTEST_NUMBER@@ # Test command number.@ \ @]@ \
@@PTEST_CONFIG@@ # Test configuration suffix.@ \ @[<v 1>\
@@PTEST_RESULT@@ # Shorthand alias to '@@PTEST_DIR@@/result@@PTEST_CONFIG@@' (the result directory dedicated to the tested configuration).@ \ Some predefined macros can be used in test commands:@ \
@@PTEST_ORACLE@@ # Basename of the current oracle file (macro only usable in FILTER directives).@ \ @@PTEST_DIR@@ # Dirname of the test file.@ \
@@PTEST_MODULE@@ # Current list of module defined by the MODULE directive.@ \ @@PTEST_FILE@@ # Substituted by the test filename.@ \
@@PTEST_LOAD_MODULE@@ # The '-load-module' option related to the MODULE directive.@ \ @@PTEST_NAME@@ # Basename of the test file.@ \
@@PTEST_PLUGIN@@ # Current list of plugins defined by the PLUGIN directive.@ \ @@PTEST_NUMBER@@ # Test command number.@ \
@@PTEST_LOAD_PLUGIN@@ # The '-load-module' option related to the PLUGIN directive.@ \ @@PTEST_CONFIG@@ # Test configuration suffix.@ \
@@PTEST_LOAD_OPTIONS@@ # Shorthand alias to '@@PTEST_LOAD_PLUGIN@@ @@PTEST_LOAD_MODULE@@' .@ \ @@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>\ @[<v 1>\
Examples:@ \ Examples:@ \
ptests@ \ ptests@ \
...@@ -345,7 +359,11 @@ let example_msg = ...@@ -345,7 +359,11 @@ let example_msg =
ptests -v -j 1 \ ptests -v -j 1 \
# to check the time taken by each test\ # 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]";; let umsg = "Usage: ptests [options] [names of test suites]";;
......
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