Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
eb67ef5f
Commit
eb67ef5f
authored
5 years ago
by
Virgile Prevosto
Committed by
Valentin Perrelle
5 years ago
Browse files
Options
Downloads
Patches
Plain Diff
[doc] Fix index entry for MODULE and clean up test directive entries
parent
39cd8ff7
No related branches found
No related tags found
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
doc/developer/advance.tex
+20
-20
20 additions, 20 deletions
doc/developer/advance.tex
doc/developer/macros.sty
+2
-1
2 additions, 1 deletion
doc/developer/macros.sty
with
22 additions
and
21 deletions
doc/developer/advance.tex
+
20
−
20
View file @
eb67ef5f
...
@@ -745,7 +745,7 @@ occurs currently in the following cases:
...
@@ -745,7 +745,7 @@ occurs currently in the following cases:
\begin{example}
\begin{example}
Test
\texttt
{
tests/sparecode/calls.c
}
declares the following directives.
Test
\texttt
{
tests/sparecode/calls.c
}
declares the following directives.
\
s
scodeidx
{
Test
}{
Directive
}{
OPT
}
\
n
scodeidx
{
Test
!
Directive
}{
OPT
}
\begin{listing-nonumber}
\begin{listing-nonumber}
/* run.config
/* run.config
OPT: -sparecode-analysis
OPT: -sparecode-analysis
...
@@ -895,59 +895,59 @@ the configuration header of a test (or a test suite).
...
@@ -895,59 +895,59 @@ 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
{
CMD
}
\
s
scodeidxdef
{
Test
}{
Directive
}{
CMD
}
&
\texttt
{
CMD
}
\
n
scodeidxdef
{
Test
!
Directive
}{
CMD
}
&
Program to run
&
Program to run
&
\texttt
{
./bin/toplevel.opt
}
&
\texttt
{
./bin/toplevel.opt
}
\\
\\
&
\texttt
{
OPT
}
\
s
scodeidxdef
{
Test
}{
Directive
}{
OPT
}
&
\texttt
{
OPT
}
\
n
scodeidxdef
{
Test
!
Directive
}{
OPT
}
&
Options given to the program
&
Options given to the program
&
\texttt
{
-val -out -input -deps
}
&
\texttt
{
-val -out -input -deps
}
\\
\\
&
\texttt
{
STDOPT
}
\
s
scodeidxdef
{
Test
}{
Directive
}{
STDOPT
}
&
\texttt
{
STDOPT
}
\
n
scodeidxdef
{
Test
!
Directive
}{
STDOPT
}
&
Add and remove options from the default set
&
Add and remove options from the default set
&
\textit
{
None
}
&
\textit
{
None
}
\\
\\
&
\texttt
{
LOG
}
\
s
scodeidxdef
{
Test
}{
Directive
}{
LOG
}
&
\texttt
{
LOG
}
\
n
scodeidxdef
{
Test
!
Directive
}{
LOG
}
&
Add an additional file to compare against an oracle
&
Add an additional file to compare against an oracle
&
\textit
{
None
}
&
\textit
{
None
}
\\
\\
&
\texttt
{
EXECNOW
}
\
s
scodeidxdef
{
Test
}{
Directive
}{
EXECNOW
}
&
\texttt
{
EXECNOW
}
\
n
scodeidxdef
{
Test
!
Directive
}{
EXECNOW
}
&
Run a command before the following commands. When specified in a configuration
&
Run a command before the following commands. When specified in a configuration
file, run it only once.
file, run it only once.
&
\textit
{
None
}
&
\textit
{
None
}
\\
\\
&
\texttt
{
EXEC
}
\
s
scodeidxdef
{
Test
}{
Directive
}{
EXEC
}
&
\texttt
{
EXEC
}
\
n
scodeidxdef
{
Test
!
Directive
}{
EXEC
}
&
Similar to
\texttt
{
EXECNOW
}
, but run it once per testing file.
&
Similar to
\texttt
{
EXECNOW
}
, but run it once per testing file.
&
\textit
{
None
}
&
\textit
{
None
}
\\
\\
&
\texttt
{
MACRO
}
\
s
scodeidxdef
{
Test
}{
Directive
}{
MACRO
}
&
\texttt
{
MACRO
}
\
n
scodeidxdef
{
Test
!
Directive
}{
MACRO
}
&
Define a new macro
&
Define a new macro
&
\textit
{
None
}
&
\textit
{
None
}
\\
\\
&
\texttt
{
FILTER
}
\
s
scodeidxdef
{
Test
}{
Directive
}{
FILTER
}
&
\texttt
{
FILTER
}
\
n
scodeidxdef
{
Test
!
Directive
}{
FILTER
}
&
Command used to filter results
&
Command used to filter results
&
\textit
{
None
}
&
\textit
{
None
}
\\
\\
&
\texttt
{
MODULE
}
\
s
scodeidxdef
{
Test
}{
Directive
}{
FILTER
}
&
\texttt
{
MODULE
}
\
n
scodeidxdef
{
Test
!
Directive
}{
MODULE
}
&
Register a dynamic module to be built and to be loaded with each subsequent
&
Register a dynamic module to be built and to be loaded with each subsequent
test
test
&
\textit
{
None
}
&
\textit
{
None
}
\\
\\
\hline
\multirow
{
2
}{
23mm
}{
\centering
{
Test suite
}}
\hline
\multirow
{
2
}{
23mm
}{
\centering
{
Test suite
}}
&
\texttt
{
DONTRUN
}
\
s
scodeidxdef
{
Test
}{
Directive
}{
DONTRUN
}
&
\texttt
{
DONTRUN
}
\
n
scodeidxdef
{
Test
!
Directive
}{
DONTRUN
}
&
Do not execute this test
&
Do not execute this test
&
\textit
{
None
}
&
\textit
{
None
}
\\
\\
&
\texttt
{
FILEREG
}
\
s
scodeidxdef
{
Test
}{
Directive
}{
FILEREG
}
&
\texttt
{
FILEREG
}
\
n
scodeidxdef
{
Test
!
Directive
}{
FILEREG
}
&
selects the files to test
&
selects the files to test
&
\texttt
{
.*
\bss
.
\bss
(c|i
\bss
)
}
&
\texttt
{
.*
\bss
.
\bss
(c|i
\bss
)
}
\\
\\
\hline
\multirow
{
2
}{
23mm
}{
\centering
{
Miscellaneous
}}
\hline
\multirow
{
2
}{
23mm
}{
\centering
{
Miscellaneous
}}
&
\texttt
{
COMMENT
}
\
s
scodeidxdef
{
Test
}{
Directive
}{
COMMENT
}
&
\texttt
{
COMMENT
}
\
n
scodeidxdef
{
Test
!
Directive
}{
COMMENT
}
&
Comment in the configuration
&
Comment in the configuration
&
\textit
{
None
}
&
\textit
{
None
}
\\
\\
&
\texttt
{
GCC
}
\
s
scodeidxdef
{
Test
}{
Directive
}{
GCC
}
&
\texttt
{
GCC
}
\
n
scodeidxdef
{
Test
!
Directive
}{
GCC
}
&
Unused (compatibility only)
&
Unused (compatibility only)
&
\textit
{
None
}
&
\textit
{
None
}
\\
\\
...
@@ -998,7 +998,7 @@ the sequence above is read in order and defines a configuration level
...
@@ -998,7 +998,7 @@ the sequence above is read in order and defines a configuration level
directive is found). No new test case is generated
directive is found). No new test case is generated
if there is no further
\texttt
{
OPT
}
directive. At a given
if there is no further
\texttt
{
OPT
}
directive. At a given
configuration level, the default value for directive
configuration level, the default value for directive
\texttt
{
CMD
}
\
s
scodeidx
def
{
Test
}{
Directive
}{
CMD
}
is the last
\texttt
{
CMD
}
\
n
scodeidx
{
Test
!
Directive
}{
CMD
}
is the last
\texttt
{
CMD
}
directive of the preceding configuration level.
\texttt
{
CMD
}
directive of the preceding configuration level.
\item
\texttt
{
LOG
}
adds a file to be compared against an oracle in the
\item
\texttt
{
LOG
}
adds a file to be compared against an oracle in the
next
\texttt
{
OPT
}
directive. Several files can be monitored from a single
next
\texttt
{
OPT
}
directive. Several files can be monitored from a single
...
@@ -1012,7 +1012,7 @@ the sequence above is read in order and defines a configuration level
...
@@ -1012,7 +1012,7 @@ the sequence above is read in order and defines a configuration level
configuration level, they correspond to different test cases. The
configuration level, they correspond to different test cases. The
\texttt
{
OPT
}
directive(s) of a given configuration level replace(s)
\texttt
{
OPT
}
directive(s) of a given configuration level replace(s)
the ones of the preceding level.
the ones of the preceding level.
\item
The
\texttt
{
STDOPT
}
\
s
scodeidx
def
{
Test
}{
Directive
}{
STDOPT
}
\item
The
\texttt
{
STDOPT
}
\
n
scodeidx
{
Test
!
Directive
}{
STDOPT
}
directive takes as default set of options
directive takes as default set of options
the last
\texttt
{
OPT
}
directive(s) of the preceding configuration
the last
\texttt
{
OPT
}
directive(s) of the preceding configuration
level. If the preceding configuration level contains several
level. If the preceding configuration level contains several
...
@@ -1030,8 +1030,8 @@ options). As with \texttt{OPT}, each \texttt{STDOPT} corresponds to a different
...
@@ -1030,8 +1030,8 @@ options). As with \texttt{OPT}, each \texttt{STDOPT} corresponds to a different
(set of) test case(s).
\texttt
{
LOG
}
directives preceding an
\texttt
{
STDOPT
}
(set of) test case(s).
\texttt
{
LOG
}
directives preceding an
\texttt
{
STDOPT
}
are taken into account.
are taken into account.
\item
The syntax for directives
\item
The syntax for directives
\texttt
{
EXECNOW
}
\
s
scodeidx
def
{
Test
}{
Directive
}{
EXECNOW
}
\texttt
{
EXECNOW
}
\
n
scodeidx
{
Test
!
Directive
}{
EXECNOW
}
and
\texttt
{
EXEC
}
\
s
scodeidxdef
{
Test
}{
Directive
}{
EXEC
}
is the following.
and
\texttt
{
EXEC
}
\
n
scodeidxdef
{
Test
!
Directive
}{
EXEC
}
is the following.
\begin{code}
\begin{code}
EXECNOW: [ [ LOG file | BIN file ] ... ] cmd
EXECNOW: [ [ LOG file | BIN file ] ... ] cmd
\end{code}
\end{code}
...
@@ -1057,7 +1057,7 @@ or
...
@@ -1057,7 +1057,7 @@ or
the command is put in a test configuration file:
the command is put in a test configuration file:
\texttt
{
EXECNOW
}
executes the command only once for the test suite, while
\texttt
{
EXECNOW
}
executes the command only once for the test suite, while
\texttt
{
EXEC
}
executes it once per test file of the test suite.
\texttt
{
EXEC
}
executes it once per test file of the test suite.
\item
The
\texttt
{
MACRO
}
\
s
scodeidx
def
{
Test
}{
Directive
}{
MACRO
}
directive
\item
The
\texttt
{
MACRO
}
\
n
scodeidx
{
Test
!
Directive
}{
MACRO
}
directive
has the following syntax:
has the following syntax:
\begin{code}
\begin{code}
MACRO: macro-name content
MACRO: macro-name content
...
@@ -1069,7 +1069,7 @@ or
...
@@ -1069,7 +1069,7 @@ or
\texttt
{
STDOPT
}
or
\texttt
{
EXECNOW
}
directive at this configuration level
\texttt
{
STDOPT
}
or
\texttt
{
EXECNOW
}
directive at this configuration level
or in any level below it will be replaced by
\texttt
{
content
}
. Existing
or in any level below it will be replaced by
\texttt
{
content
}
. Existing
pre-defined macros are listed in section~
\ref
{
sec:ptests-macros
}
.
pre-defined macros are listed in section~
\ref
{
sec:ptests-macros
}
.
\item
The
\texttt
{
FILEREG
}
\
s
scodeidx
def
{
Test
}{
Directive
}{
FILEREG
}
\item
The
\texttt
{
FILEREG
}
\
n
scodeidx
{
Test
!
Directive
}{
FILEREG
}
directive contains a regular expression indicating which files in
directive contains a regular expression indicating which files in
the directory containing the current test suite are actually part of
the directory containing the current test suite are actually part of
the suite. This directive is only
the suite. This directive is only
...
...
This diff is collapsed.
Click to expand it.
doc/developer/macros.sty
+
2
−
1
View file @
eb67ef5f
...
@@ -30,7 +30,8 @@
...
@@ -30,7 +30,8 @@
\index
{
#1@
\texttt
{
#1
}
!#2@
\texttt
{
\fontsize
{
8
}{
10
}
\selectfont
#2
}
|bfit
}}
\index
{
#1@
\texttt
{
#1
}
!#2@
\texttt
{
\fontsize
{
8
}{
10
}
\selectfont
#2
}
|bfit
}}
\newcommand
{
\sscodeidxdef
}
[3]
{
%
\newcommand
{
\sscodeidxdef
}
[3]
{
%
\index
{
#1@
\texttt
{
#1
}
!#2@
\texttt
{
#2
}
!#3@
\texttt
{
#3
}
|bfit
}}
\index
{
#1@
\texttt
{
#1
}
!#2@
\texttt
{
#2
}
!#3@
\texttt
{
#3
}
|bfit
}}
\newcommand
{
\nscodeidx
}
[2]
{
\index
{
#1!#2@
\texttt
{
#2
}}}
\newcommand
{
\nscodeidxdef
}
[2]
{
\index
{
#1!#2@
\texttt
{
#2
}
|bfit
}}
\makeatletter
\makeatletter
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment