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
Snippets
Deploy
Releases
Package Registry
Container Registry
Model registry
Operate
Terraform modules
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
Charles Southerland
frama-c
Commits
94643712
Commit
94643712
authored
4 years ago
by
Andre Maroneze
Browse files
Options
Downloads
Patches
Plain Diff
[Doc/Devman] Update ptests section in developer manual
parent
ea221a25
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
doc/developer/advance.tex
+4
-14
4 additions, 14 deletions
doc/developer/advance.tex
doc/developer/architecture.tex
+0
-7
0 additions, 7 deletions
doc/developer/architecture.tex
ptests/ptests.ml
+1
-1
1 addition, 1 deletion
ptests/ptests.ml
with
5 additions
and
22 deletions
doc/developer/advance.tex
+
4
−
14
View file @
94643712
...
...
@@ -709,19 +709,6 @@ There is exactly one directive by line. The different directives (\emph{i.e.}
possibilities for
\texttt
{
CONFIG
\_
OPTION
}
) are detailed in
Section~
\ref
{
ptests:directives
}
.
\begin{important}
Note that some specific configurations require dynamic linking, which
is not available on all platforms for native code.
{
\tt
ptests
}
takes
care of reverting to bytecode when it detects that the
{
\tt
OPT
}
,
{
\tt
EXECNOW
}
, or
\texttt
{
EXEC
}
options of a test require dynamic linking. This
occurs currently in the following cases:
\begin{itemize}
\item
{
\tt
OPT
}
contains the option
{
\tt
-load-script
}
\item
{
\tt
OPT
}
contains the option
{
\tt
-load-module
}
\item
{
\tt
EXECNOW
}
and
\texttt
{
EXEC
}
use
{
\tt
make
}
to create a
{
\tt
.cmxs
}
\end{itemize}
\end{important}
\begin{important}
\textbf
{
Concurrency issues:
}
tests using compiled modules (
{
\tt
-load-script
}
or
{
\tt
-load-module
}
) may
...
...
@@ -740,6 +727,7 @@ occurs currently in the following cases:
In addition, if the same script
{
\tt
tests/suite/script.ml
}
is shared by several test files, the
{
\tt
EXECNOW
}
directive should be put
into
{
\tt
tests/suite/test
\_
config
}
.
Check the
{
\tt
MODULE
}
directive for a common solution to this issue.
\end{important}
...
...
@@ -832,9 +820,11 @@ Figure~\ref{fig:ptests-options} details the options of \ptests.
&
\texttt
{
-byte
}
&
Use bytecode toplevel
&
no
\\
&
\texttt
{
-opt
}
&
Use native toplevel
&
yes
\\
&
\texttt
{
-gui
}
&
Use GUI instead of console-based toplevel
&
no
\\
\hline
\multirow
{
4
}{
16mm
}{
\centering
{
Behavior
}}
\hline
\multirow
{
5
}{
16mm
}{
\centering
{
Behavior
}}
&
\texttt
{
-run
}
&
Delete current results; run tests and examine results
&
yes
\\
&
\texttt
{
-dry-run
}
&
Print commands, but do not execute them
&
no
\\
&
\texttt
{
-examine
}
&
Only examine current results; do not run tests
&
no
\\
&
\texttt
{
-show
}
&
Run tests and show results, but do not examine
them; implies
\texttt
{
-byte
}
&
...
...
This diff is collapsed.
Click to expand it.
doc/developer/architecture.tex
+
0
−
7
View file @
94643712
...
...
@@ -203,13 +203,6 @@ only possible one to define mutually dependent plug-ins while the third one
(through module
\texttt
{
Db
}
) is now fully deprecated even if most of the older
\framac
plug-ins are still defined this way.
Plug-ins are usually dynamically linked when
\framac
is booting, even if some
older
\framac
plug-ins are still statically linked. However it is still possible
to statically link a dynamic plug-in if wanted or required. In particular,
\ocaml
does not support dynamic linking on some hardware
architecture~
\cite
{
caml
}
: in this case, you have to statically link all
plug-ins.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section
{
Libraries
}
\label
{
archi:libraries
}
...
...
This diff is collapsed.
Click to expand it.
ptests/ptests.ml
+
1
−
1
View file @
94643712
...
...
@@ -338,7 +338,7 @@ let rec argspec =
"-xunit"
,
Arg
.
Set
xunit
,
" Create a xUnit file named xunit.xml collecting results"
;
"-error-code"
,
Arg
.
Set
do_error_code
,
" Exit with error code 1 if tests failed (useful for scripts"
;
" Exit with error code 1 if tests failed (useful for scripts
)
"
;
]
and
help_msg
()
=
Arg
.
usage
(
Arg
.
align
argspec
)
umsg
;;
...
...
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