Commit 299e6d62 authored by Julien Signoles's avatar Julien Signoles
Browse files

[E-ACSL] improve handling of -e-acsl-prepare resulting in one warning less + end of manual

parent 61f36448
......@@ -24,7 +24,8 @@
- E-ACSL [2012/12/20] Support of ghost variables and statements.
-* E-ACSL [2012/12/13] Fix bug with complex term left-values.
- E-ACSL [2012/11/27] Support of \valid_read.
- E-ACSL [2012/11/27] Prevent runtime errors in annotations.
- E-ACSL [2012/11/27] Prevent runtime errors in annotations, except
unitialized variables.
- E-ACSL [2012/11/19] Support of floats in annotations. Approximate
reals by floats.
- E-ACSL [2012/10/25] Support of \valid.
......
int main(void) {
int x = 0xffff;
int y = 0xfff;
int z = x + y;
return 0;
}
......@@ -2,10 +2,12 @@
\framac~\cite{userman,sefm12} 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. This plug-in automatically translates
an annotated C code into another one which fails at runtime if an annotation is
violated. If no annotation is violated, the behavior of the new program is
exactly the same than the one of the original program.
documents the \eacsl plug-in of \framac, version \eacslversion. Which \eacsl
version you are using is indicated by running \texttt{frama-c
-e-acsl-version}\optionidx{-}{e-acsl-version}. This plug-in automatically
translates an annotated C code into another one which fails at runtime if an
annotation is violated. If no annotation is violated, the behavior of the new
program is exactly the same than the one of the original program.
Such a translation brings several benefits. First it allows the user to monitor
a \C code, in particular to perform what is usually called ``runtime assertion
......
......@@ -7,6 +7,7 @@
\newcommand{\framac}{\textsc{Frama-C}\xspace}
\newcommand{\acsl}{\textsc{ACSL}\xspace}
\newcommand{\eacsl}{\textsc{E-ACSL}\xspace}
\newcommand{\rte}{\textsc{RTE}\xspace}
\newcommand{\C}{\textsc{C}\xspace}
\newcommand{\jml}{\textsc{JML}\xspace}
\newcommand{\valueplugin}{\textsc{Value}\xspace}
......
File suppressed by a .gitattributes entry or the file's encoding is unsupported.
\chapter{What the Plug-in Provides}
This chapter is the core of this manual and describes how to use the
plug-in. First, Section~\ref{sec:run} shows how to run the plug-in on a trivial
example and how to execute the generated code with a standard \C compiler to
detect invalid annotations at runtime. Then, Section~\ref{sec:exec-env} provides
additional details on the execution of the generated code. Next,
plug-in. You can still call the option \optiondef{-}{e-acsl-help} to get the
list of available options with few lines of documentation. First,
Section~\ref{sec:simple} shows how to run the plug-in on a trivial example and
how to execute the generated code with a standard \C compiler to detect invalid
annotations at runtime. Then, Section~\ref{sec:exec-env} provides additional
details on the execution of the generated code. Next,
Section~\ref{sec:incomplete} focuses on how to deal with incomplete programs,
\emph{i.e.} in which some functions have no body or in which there are no main
function. After, Section~\ref{sec:combine} explains how to combine the plug-in
......@@ -17,7 +19,7 @@ policy of the plug-in.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Simple Example}
\label{sec:run}
\label{sec:simple}
This Section is a mini-tutorial which explains from scratch how to use the
\eacsl plug-in to detect at runtime that an \eacsl annotation is violated.
......@@ -25,6 +27,7 @@ This Section is a mini-tutorial which explains from scratch how to use the
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Running \eacsl}
\label{sec:run}
Consider the following simple program in which the first assertion is valid
while the second one is not.
......@@ -572,16 +575,64 @@ the beginning of this manual may overflow in case of big exponentiations.
\section{Combining E-ACSL with Others Plug-ins}
\label{sec:combine}
\begin{itemize}
\item -e-acsl-valid
\item -e-acsl-prepare
\end{itemize}
annotations are kept in order to analyze the generated code
possible to run rte first
As the \eacsl plug-in generates a new \framac project, it is easy to run any
plug-in on the generated program, either in the same \framac session (thanks to
the option \optionuse{-}{then} or through the GUI), or in another one. The only
issue might be that, depending on the plug-in, the analysis may be unperfect if
the generated program uses \gmp or the dedicated memory library: both
intensively use dynamic structures which are usually difficult to handle by
analysis tools.
Another way to combine \eacsl with others plug-ins is to run \eacsl afterwards.
For instance, the \rte plug-in~\cite{rte} may be used to generate annotations
corresponding to runtime errors. Then the \eacsl plug-in may generate an
instrumented program to verify that there is no such runtime errors during the
execution of the program.
Consider the following program.
\listingname{combine.i}
\cinput{examples/combine.i}
To check at runtime that this programs 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 \
-ocode monitored_combine.i
\$ gcc -o combine `frama-c -print-share-path`/e-acsl monitored_combine.i
\$ ./combine.
\end{shell}
combination with value and wp
Nevertheless if you run the \eacsl plug-in after another one, it first generates
a new temporary project in which it links the analysed program against its own
library in order to generate the \framac internal representation of the \C
program (\emph{aka} AST), as explained in Section~\ref{sec:run}. Consequently,
even if the \eacsl plug-in keeps the maximum amount of information, results of
already executed analyzer (like the validity status of the annotations) are not
known in this new project. If you want to keep them, you have to set the option
\optiondef{-}{e-acsl-prepare} when the first analysis is asked for.
In this context, the \eacsl plug-in does not generate code for annotations
proven valid by another plug-in, except if you explicitely set the option
\optiondef{-}{e-acsl-valid}. For instance, \valueplugin~\cite{value} is able to
prove that there is no potential overflow in the previous program, so the \eacsl
plugin 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
\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
\$ frama-c -rte combine.i -then -val -then -e-acsl \
-then-on e-acsl -print -ocode monitored_combine.i
\end{shell}
In the first case, that is because it is explicitely required by the option
\texttt{-e-acsl-valid} while, in the second case, that is because the option
\texttt{-e-acsl-prepare} is not provided on the command line which results in
the fact that the result of the value analysis are unknown when the \eacsl
plug-in is running.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......
......@@ -43,13 +43,7 @@ let check =
(Datatype.func Datatype.unit Datatype.bool)
check
module Extended_ast =
State_builder.Option_ref
(Project.Datatype)
(struct
let name = "E-ACSL AST is extended"
let dependencies = []
end)
let extended_ast_project: Project.t option ref = ref None
let unmemoized_extend_ast () =
let extend () =
......@@ -101,12 +95,21 @@ E-ACSL is going to work on a copy.";
Project.current ()
end
let extend_ast () = Extended_ast.memo unmemoized_extend_ast
let extend_ast () = match !extended_ast_project with
| None ->
let prj = unmemoized_extend_ast () in
extended_ast_project := Some prj;
prj
| Some prj ->
prj
let apply_on_e_acsl_ast f x =
let tmp_prj = extend_ast () in
let res = Project.on tmp_prj f x in
if tmp_prj != Project.current () then Project.remove ~project:tmp_prj ();
if not (Project.equal tmp_prj (Project.current ())) then begin
extended_ast_project := None;
Project.remove ~project:tmp_prj ()
end;
res
module Resulting_projects =
......@@ -166,6 +169,10 @@ let predicate_to_exp =
let add_e_acsl_library _files =
if Options.must_visit () || Options.Prepare.get () then ignore (extend_ast ())
(* extending the AST as soon as possible reduce the amount of time the AST is
duplicated:
- that is faster
- locations are better (indicate an existing file, and not a temp file) *)
let () = Cmdline.run_after_configuring_stage add_e_acsl_library
let main () =
......
Markdown is supported
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