Skip to content
Snippets Groups Projects
Commit 61650ee9 authored by Julien Signoles's avatar Julien Signoles
Browse files

[userman] ready for v0.5

parent 3be07742
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 155 additions and 84 deletions
src/plugins/e-acsl/VERSION
+ 1
− 1
View file @ 61650ee9
0.4.1+dev
0.5
src/plugins/e-acsl/doc/Changelog
+ 4
− 0
View file @ 61650ee9
......@@ -15,6 +15,10 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
########################
Plugin E-ACSL 0.5 Sodium
########################
- E-ACSL [2015/06/01] Support of \freeable. Thus illegal calls to
free (e.g. double free) are detected.
-* E-ACSL [2015/05/28] Fix types of \block_length and \offset.
......
src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf
+9.61 KiB (+1%)
View file @ 61650ee9
File suppressed by a .gitattributes entry or the file's encoding is unsupported.
src/plugins/e-acsl/doc/userman/Makefile
+ 1
− 1
View file @ 61650ee9
......@@ -16,7 +16,7 @@ default: main.pdf
main.pdf: $(DEPS_MODERN)
EACSL_VERSION= $(shell cat $(VERSION_FILE))
FC_VERSION= Neon
FC_VERSION= Sodium
EACSL_DIR=../..
DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
......
src/plugins/e-acsl/doc/userman/biblio.bib
+ 33
− 10
View file @ 61650ee9
......@@ -38,26 +38,26 @@
author = {Baudin, Patrick and Pascal Cuoq and Filli\^{a}tre, Jean-Christophe
and March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and
Prevosto, Virgile},
month = apr,
title = {ACSL: ANSI/ISO C Specification Language. Version 1.8 ---
month = mar,
title = {ACSL: ANSI/ISO C Specification Language. Version 1.9 ---
Frama-C Neon implementation.},
year = {2014}
year = {2015}
}
@manual{eacsl,
author = {Julien Signoles},
title = {E-ACSL: Executable ANSI/ISO C Specification Language. Version 1.8},
year = 2014,
month = apr,
title = {E-ACSL: Executable ANSI/ISO C Specification Language. Version 1.9},
year = 2015,
month = jun,
note = {\mbox{\url{http://frama-c.com/download/e-acsl/e-acsl.pdf}}}
}
@manual{eacsl-implem,
author = {Julien Signoles},
title = {E-ACSL Version 1.7.
Implementation in Frama-C Plug-in E-ACSL version 0.4},
year = 2014,
month = apr,
title = {E-ACSL Version 1.9.
Implementation in Frama-C Plug-in E-ACSL version 0.5},
year = 2015,
month = jun,
note = {\mbox{\url{http://frama-c.com/download/e-acsl/e-acsl-implementation.pdf}}}
}
......@@ -124,6 +124,19 @@
month = oct,
}
@article{fac15,
year={2015},
month={jan},
journal={Formal Aspects of Computing},
title={{Frama-C: A Software Analysis Perspective}},
publisher={Springer London},
keywords={Formal verification; Static analysis; Dynamic analysis; C},
author={Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and
Signoles, Julien and Yakobowski, Boris},
pages={1-37},
note={Extended version of \cite{sefm12}},
}
@article{runtime-assertion-checking,
author = {Lori A. Clarke and
David S. Rosenblum},
......@@ -155,3 +168,13 @@
year = 2009,
publisher = {{IEEE} Computer Society},
}
@inproceedings{jfla15,
title = {{Rester statique pour devenir plus rapide, plus pr{\'e}cis et plus mince}},
author = {Arvid Jakobsson and Nikolai Kosmatov and Julien Signoles},
booktitle = {Journes Francophones des Langages Applicatifs (JFLA'15)},
editor = {David Baelde and Jade Alglave},
year = {2015},
month = jan,
note = {In French},
}
src/plugins/e-acsl/doc/userman/changes.tex
+ 6
− 1
View file @ 61650ee9
......@@ -6,13 +6,18 @@ release. First we list changes of the last release.
\section*{E-ACSL \eacslversion}
\begin{itemize}
\item \textbf{Libc}: new section.
\item \textbf{Architecture Dependent Annotations}: add a remark about \gcc's
machdep.
\item Use \texttt{-then-last} whenever possible.
\item Update output wrt \framac Sodium changes.
\item \textbf{Bibliography:} fix incorrect links.
\end{itemize}
\section*{E-ACSL 0.4}
\begin{itemize}
\item No change
\item No change.
\end{itemize}
\section*{E-ACSL 0.3}
......
src/plugins/e-acsl/doc/userman/eacslversion.tex
+ 2
− 2
View file @ 61650ee9
\newcommand{\eacslversion}{0.4.1\xspace}
\newcommand{\fcversion}{Neon\xspace}
\newcommand{\eacslversion}{0.5\xspace}
\newcommand{\fcversion}{Sodium\xspace}
src/plugins/e-acsl/doc/userman/examples/pointer.c
+ 1
− 1
View file @ 61650ee9
#include "stdlib.h"
#include <stdlib.h>
extern void *malloc(size_t);
extern void free(void*);
......
src/plugins/e-acsl/doc/userman/introduction.tex
+ 2
− 2
View file @ 61650ee9
\chapter{Introduction}
\framac~\cite{userman,sefm12} is a modular analysis framework for the C language
which supports the ACSL specification language~\cite{acsl}. This manual
\framac~\cite{userman,sefm12,fac15} is a modular analysis framework for the C
language which supports the ACSL specification language~\cite{acsl}. This manual
documents the \eacsl plug-in of \framac, version \eacslversion. The \eacsl
version you are using is indicated by the command \texttt{frama-c
-e-acsl-version}\optionidx{-}{e-acsl-version}. This plug-in automatically
......
src/plugins/e-acsl/doc/userman/macros.tex
+ 8
− 0
View file @ 61650ee9
......@@ -275,3 +275,11 @@
\newcommand{\optionuse}[2]{\texttt{#1#2}\optionidx{#1}{#2}}
\newcommand{\textttuse}[1]{\texttt{#1}\codeidx{#1}}
\definecolor{gris}{gray}{0.85}
\makeatletter
\newenvironment{important}%
{\hspace{5pt plus \linewidth minus \marginparsep}%
\begin{lrbox}{\@tempboxa}%
\begin{minipage}{\linewidth - 2\fboxsep}}
{\end{minipage}\end{lrbox}\colorbox{gris}{\usebox{\@tempboxa}}}
src/plugins/e-acsl/doc/userman/main.tex
+ 6
− 5
View file @ 61650ee9
......@@ -42,14 +42,15 @@ CEA LIST, Software Safety Laboratory, Saclay, F-91191 \\
This is the user manual of the \framac plug-in
\eacsl\footnote{\url{http://frama-c.com/eacsl}}. The contents of this document
correspond to its version \eacslversion (\today) compatible with the version
\fcversion of \framac~\cite{userman,sefm12}. However the development of the
\eacsl plug-in is still ongoing: features described here may still evolve in the
future.
\fcversion of \framac~\cite{userman,sefm12,fac15}. However the development of
the \eacsl plug-in is still ongoing: features described here may still evolve in
the future.
\section*{Acknowledgements}
We gratefully thank all the people who contributed to this document: Florent
Kirchner, Nikola Kosmatov and Guillaume Petiot.
We gratefully thank all the people who contributed to this document: Jens
Gerlach, Pierre-Lo\"ic Garoche, Florent Kirchner, Nikola Kosmatov and Guillaume
Petiot.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......
src/plugins/e-acsl/doc/userman/provides.tex
+ 91
− 61
View file @ 61650ee9
......@@ -39,38 +39,40 @@ Running \eacsl on this file just consists in adding the option
\optiondef{-}{e-acsl} to the \framac command line:
\begin{shell}
\$ frama-c -e-acsl first.i
[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl.h
[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp_types.h
[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp.h
[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_mmodel_api.h
[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_bittree.h
[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_mmodel.h
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
[kernel] Parsing first.i (no preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
\end{shell}
Even if \texttt{first.i} is already preprocessed, \eacsl first asks the \framac
kernel to preprocess and to link against \texttt{first.i} several files which
form the \eacsl library. Their usage will be explain later, mainly in
form the \eacsl library. Their usage will be explained later, mainly in
Section~\ref{sec:exec-env}.
Then \eacsl takes the annotated \C code as input and
translates it into a new \framac project named \texttt{e-acsl}\footnote{The
notion of \emph{project} is explained in Section 8.1 of the \framac user
manual~\cite{userman}.}. By default, the option \optionuse{-}{e-acsl} does
nothing more. It is however possible to have a look at the generated code in the
\framac GUI. This is also possible through the command line thanks to the kernel
options \optionuse{-}{then-on} and \optionuse{-}{print} which respectively
switch to another project and pretty prints the \C code~\cite{userman}:
Then \eacsl takes the annotated \C code as input and translates it into a new
\framac project named \texttt{e-acsl}\footnote{The notion of \emph{project} is
explained in Section 8.1 of the \framac user manual~\cite{userman}.}. By
default, the option \optionuse{-}{e-acsl} does nothing more. It is however
possible to have a look at the generated code in the \framac GUI. This is also
possible through the command line thanks to the kernel options
\optionuse{-}{then-last} and \optionuse{-}{print} which respectively switch to
the last generated project and pretty prints the \C code~\cite{userman}:
\begin{shell}
\$ frama-c -e-acsl first.i -then-on e-acsl -print
[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl.h
[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp_types.h
[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp.h
[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_mmodel_api.h
[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_bittree.h
[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_mmodel.h
\$ frama-c -e-acsl first.i -then-last -print
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
/* Generated by Frama-C */
......@@ -82,9 +84,6 @@ struct __anonstruct___mpz_struct_1 {
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
typedef unsigned int size_t;
/*@
model __mpz_struct { integer n };
*/
/*@ requires predicate != 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
......@@ -93,18 +92,24 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *pred_txt,
int line);
int __fc_random_counter __attribute__((__unused__));
/*@
model __mpz_struct { integer n };
*/
int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__); */
/*@
axiomatic
dynamic_allocation {
axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
}
*/
/*@ ghost extern int __e_acsl_init; */
/*@ ghost extern int __e_acsl_internal_heap; */
extern size_t __memory_size;
/*@
......@@ -152,20 +157,22 @@ precise error reports as shown in Section~\ref{sec:exec}.
\label{sec:exec}
By using the option \optionuse{-}{ocode} of \framac~\cite{userman}, we can
redirect the generated code into a \C file as follows.
redirect the generated code into a \C file as follow.
\begin{shell}
\$ frama-c -e-acsl first.i -then-on e-acsl -print -ocode monitored_first.i
\$ frama-c -e-acsl first.i -then-last -print -ocode monitored_first.i
\end{shell}
Then it may be executed by a standard \C compiler like \gcc in the following
way.
\lstset{escapechar=£}
\lstset{escapechar=£}
\begin{shell}
\$ gcc -o monitored_first `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_first.i
In file included from <file_path>/e_acsl.c:23:0:
<file_path>/e_acsl.h:41:3: warning: `FC_BUILTIN' attribute directive ignored [-Wattributes]
monitored_first.i:8:1: warning: `__FC_BUILTIN__' attribute directive ignored [-Wattributes]
monitored_first.i:19:60: warning: `__FC_BUILTIN__' attribute directive ignored [-Wattributes]
monitored_first.i:16:60: warning: `__FC_BUILTIN__' attribute directive ignored [-Wattributes]
monitored_first.i:21:1: warning: `__FRAMA_C_MODEL__' attribute directive ignored [-Wattributes]
\end{shell}
You may notice that the generated file \texttt{monitored\_first.i} is linked
against the file \texttt{`frama-c -print-share-path`/e-acsl/e\_acsl.c}. This
......@@ -223,8 +230,8 @@ undefined as soon as $e$ has to be evaluated in order to evaluate $t$
undefined term is never evaluated''}~\cite{eacsl}.
Accordingly, the \eacsl plug-in prevents an undefined term from being
evaluated. Should it be because an annotation contains such a term, it will
report a proper error at runtime instead.
evaluated. If an annotation contains such a term, \eacsl will report a proper
error at runtime instead of evaluating it.
Consider for instance the following annotated program.
......@@ -239,7 +246,7 @@ However we can generate an instrumented code and compile it through the
following command lines:
\begin{shell}
\$ frama-c -e-acsl rte.i -then-on e-acsl -print -ocode monitored_rte.i
\$ frama-c -e-acsl rte.i -then-last -print -ocode monitored_rte.i
\$ gcc -o rte `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_rte.i
\end{shell}
......@@ -255,7 +262,7 @@ division_by_zero: y != 0.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Architecture Dependent Annotations}
\subsection{Architecture Dependent Annotations}\label{sec:architecture}
In many cases, the execution of a \C program depends on the underlying machine
architecture it is executed on. The program must be compiled on the very same
......@@ -279,7 +286,7 @@ following command lines (the option \optionuse{-}{pp-annot} must be used to
preprocess the annotations~\cite{userman}):
\begin{shell}
\$ frama-c -pp-annot -e-acsl archi.c -then-on e-acsl -print -ocode monitored_archi.i
\$ frama-c -pp-annot -e-acsl archi.c -then-last -print -ocode monitored_archi.i
\$ gcc -o archi `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_archi.i
\end{shell}
......@@ -298,9 +305,32 @@ when running the \eacsl plug-in.
\begin{shell}
\$ frama-c -machdep x86_64 -pp-annot -e-acsl archi.c \
-then-on e-acsl -print -ocode monitored_archi.i
-then-last -print -ocode monitored_archi.i
\end{shell}
\begin{important}\index{Gcc}
If you plan to compile the generated code with \gcc, it is even better to set
\texttt{-machdep} to \texttt{gcc\_x86\_64} (or \texttt{gcc\_x86\_32}), even if
it does not matter on this simple example.
\end{important}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Libc}\index{Libc}
By default, \framac uses its own standard library (\emph{aka} libc) instead of
the one of your system. If you do not want to use it, you have to add the option
\texttt{-no-framac-stdlib}\optionidx{-}{framac-stdlib} to the \framac command
line following options on the command line:
It might be particularly useful in one of the following contexts:
\begin{itemize}
\item several libc functions are still not defined in the \framac libc; or
\item your system libc and the \framac libc mismatch about several function
types (for instance, your system libc is not 100\% posix compliant); or
\item several \framac lib functions get a contract and you are not interested in
verifying them (for instance, only runtime errors matter).
\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -312,9 +342,9 @@ when running the \eacsl plug-in.
corresponds to mathematical integers. Such a type does not fit in any integral
\C type. To circumvent this issue, \eacsl uses the \gmp
library\footnote{\url{http://gmplib.org}}. Thus, even if \eacsl does its best to
use standard integral types instead of \gmp~\cite{sac13}, it may generate such
integers from time to time. In such cases, the generated code must be linked
against \gmp to be executed.
use standard integral types instead of \gmp~\cite{sac13,jfla15}, it may generate
such integers from time to time. In such cases, the generated code must be
linked against \gmp to be executed.
Consider for instance the following program.
......@@ -328,11 +358,11 @@ We can generate an instrumented code as usual through the following command
line:
\begin{shell}
\$ frama-c -e-acsl gmp.i -then-on e-acsl -print -ocode monitored_gmp.i
\$ frama-c -e-acsl gmp.i -then-last -print -ocode monitored_gmp.i
\end{shell}
To compile it however, you need to have \gmp installed and to add the option
\optionuse{-}{lgmp} to \gcc as follows:
\optionuse{-}{lgmp} to \gcc as follow:
\begin{shell}
\$ gcc -o pow_gmp `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_gmp.i -lgmp
......@@ -370,17 +400,17 @@ Consider for instance the following program.
\listingname{valid.c}
\cinput{examples/valid.c}
Assuming that we want to execute the generated code on an X86 64-bit machine,
the generation of the instrumented code requires the use of the option
\optionuse{-}{machdep} since the code uses \texttt{sizeof}. However, nothing
is required here.
Assuming that we want to execute the generated code on an X86 64-bit machine and
to compile it with \gcc, the generation of the instrumented code requires the
use of the option \optionuse{-}{machdep} since the code uses
\texttt{sizeof}. However, nothing is required here.
\begin{shell}
\$ frama-c -machdep x86_64 -e-acsl valid.c -then-on e-acsl -print -ocode monitored_valid.i
\$ frama-c -machdep gcc_x86_64 -e-acsl valid.c -then-last -print -ocode monitored_valid.i
\end{shell}
Since the original code uses \lstinline|\valid|, the executable binary
must be generated from \texttt{monitored\_valid.i} as follows:
must be generated from \texttt{monitored\_valid.i} as follow:
\begin{shell}
\$ DIR=`frama-c -print-share-path`/e-acsl
......@@ -403,9 +433,9 @@ freed: \valid(x).
\end{shell}
Like for integers, the \eacsl plug-in does its best to use the dedicated memory
library only when required~\cite{rv13}. So, if your program does not contain
memory-related annotations, the generated one does not require to be linked
against the dedicated memory library, like the examples of the previous
library only when required~\cite{rv13,jfla15}. So, if your program does not
contain memory-related annotations, the generated one does not require to be
linked against the dedicated memory library, like the examples of the previous
sections.
However, if your program contains some annotations with pointer dereferencing
......@@ -419,7 +449,7 @@ example.
\cinput{examples/pointer.c}
\begin{shell}
\$ frama-c -machdep x86_64 -e-acsl pointer.c -then-on e-acsl -print -ocode
\$ frama-c -machdep gcc_x86_64 -e-acsl pointer.c -then-last -print -ocode
monitored_pointer.i
\$ DIR=`frama-c -print-share-path`/e-acsl
\$ MDIR=\$DIR/memory_model
......@@ -459,7 +489,7 @@ instead of \texttt{e\_acsl.c}, as shown below (we reuse the initial example
\texttt{first.i} of this manual).
\begin{shell}
\$ frama-c -e-acsl first.i -then-on e-acsl -print -ocode monitored_first.i
\$ frama-c -e-acsl first.i -then-last -print -ocode monitored_first.i
\$ gcc -o customized_first my_assert.c monitored_first.i
\$ ./customized_first
Assertion at line 3 in function main is valid.
......@@ -497,7 +527,7 @@ Consider for instance the following annotated program without such a
The instrumented code is generated as usual, even though you get an additional
warning.
\begin{shell}
\$ frama-c -e-acsl no_main.i -then-on e-acsl -print -ocode monitored_no_main.i
\$ frama-c -e-acsl no_main.i -then-last -print -ocode monitored_no_main.i
<skip preprocessing command line>
[e-acsl] beginning translation.
[e-acsl] warning: cannot find entry point `main'.
......@@ -603,7 +633,7 @@ Consider the following program.
To check at runtime that this program does not perform any runtime error (which
are potential overflows in this case), just do:
\begin{shell}
\$ frama-c -rte combine.i -then -e-acsl -then-on e-acsl -print \
\$ frama-c -rte combine.i -then -e-acsl -then-last -print \
-ocode monitored_combine.i
\$ gcc -o combine `frama-c -print-share-path`/e-acsl monitored_combine.i
\$ ./combine.
......@@ -626,14 +656,14 @@ plug-in does not generate additional code for checking them if you run the
following command.
\begin{shell}
\$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
-then-on e-acsl -print -ocode monitored_combine.i
-then-last -print -ocode monitored_combine.i
\end{shell}
The additional code will be generated with one of the two following commands.
\begin{shell}
\$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
-e-acsl-valid -then-on e-acsl -print -ocode monitored_combine.i
-e-acsl-valid -then-last -print -ocode monitored_combine.i
\$ frama-c -rte combine.i -then -val -then -e-acsl \
-then-on e-acsl -print -ocode monitored_combine.i
-then-last -print -ocode monitored_combine.i
\end{shell}
In the first case, that is because it is explicitly required by the option
\texttt{-e-acsl-valid} while, in the second case, that is because the option
......@@ -712,7 +742,7 @@ also displays the information of all the lower levels.
\hline
\texttt{-e-acsl-verbose 3}& predicates- and statements-related information\\
\hline
\texttt{-e-acsl-verbose 4 and above}& terms- and expressions-related information
\texttt{-e-acsl-verbose 4}& terms- and expressions-related information
\\
\hline
\end{tabular}
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment