Skip to content
Snippets Groups Projects
Commit 9ab690f9 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

[man] Update manuals and changelog as per changes to e-acsl-gcc.sh

options
parent 287a440b
No related branches found
No related tags found
No related merge requests found
......@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
-* E-ACSL [2016/08/02] Removed --production|-P, --no-stdlib|-N and
--debug-log|-D options of e-acsl-gcc.sh.
-* E-ACSL [2016/07/21] Enable reporting of stack traces during assertion
failures in instrumented programs.
-* E-ACSL [2016/07/13] Add an e-acsl-gcc.sh option (--print--models)
......
......@@ -142,25 +142,6 @@ By default the Patricia trie memory model is used.
.B --print-models
Print the names of the supported memory models
.TP
.B -P, --production
generate an optimized executable with all debug features disabled.
Unoptimized executables (default) may lead to a significant
performance slowdown.
.TP
.B -N, --no-stdlib
if specified the \fBE-ACSL\fP runtime library uses custom
implementations of standard library functions (such as \fBmemset\fP).
By default \fBGCC\fP builtins are used (e.g., \fB__builtin_memset\fP).
.TP
.B -D, --debug-log=\fI<FILE>
the name of the file for logging of the debugging output of
modified executables. If '-' is specified then the
output is redirected to \fISTDERR\fP. By default
the debug output is redirected to
\fI/tmp/e-acsl.log\fP. This option is only meaningful
in the absence of the \fB-P\fP flag that disables debug logging for
performance reasons.
.TP
.B -I, --frama-c=\fI<FILE>
the name of the \fBFrama-C\fP executable. By default the
first \fIframa-c\fP executable found in the system path is used.
......
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