diff --git a/src/plugins/e-acsl/doc/userman/examples/check.i b/src/plugins/e-acsl/doc/userman/examples/check.i
new file mode 100644
index 0000000000000000000000000000000000000000..087de43466bf8d1ff86b26014b55550c433a5520
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/check.i
@@ -0,0 +1,6 @@
+int main(void) {
+ int x = 0;
+ /*@ assert x == 0; */
+ /*@ assert x << 2 == 0; */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/doc/userman/examples/uninitialized.i b/src/plugins/e-acsl/doc/userman/examples/uninitialized.i
new file mode 100644
index 0000000000000000000000000000000000000000..ba12ce1eecc229c99d2df95d2cb8a269688b46c6
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/uninitialized.i
@@ -0,0 +1,5 @@
+int main(void) {
+ int x;
+ /*@ assert x == 0; */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index f839e590b08033a7b38569c6203e246ab35f6384..147fc7981a155d1cef980040a141153b15b20d48 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -11,15 +11,39 @@ hard to lift. Thus they could be there for a while. Lifting them could be part
of commercial supports\footnote{Contact us or read
\url{http://frama-c.com/support.html} for additional details.}.
-\section{Undefined Value}
-\index{Undefined value}
+\section{Uninitialized Value}
+\index{Uninitialized value}
-\begin{itemize}
-\item use of undefined values are not tracked in annotations
-\item missing guards for \lstinline+\offset+, \lstinline+\block_length+ and
- \lstinline+texbase_addr+ (\lstinline+offset(p)+ must ensures that $p$ is
- valid)
-\end{itemize}
+As explained in Section~\ref{sec:runtime-error}, the \eacsl plug-in should never
+translate an annotation into a \C code which can lead to a runtime error. That
+is the case, except for unitialized values which are values read before having
+been written like in the following example.
+
+\listingname{uninitialized.i}
+\cinput{examples/uninitialized.i}
+
+If you generate the instrumented code, compile it, and finally execute it, you
+may get no runtime error depending on your \C compiler, but the behavior is
+actually uninitialized and should be trap by the \eacsl plug-in. That is not the
+case yet.
+\begin{shell}
+\$ frama-c -e-acsl uninitialized.i -then-on e-acsl -print \
+ -ocode monitored_uninitialized.i
+\$ gcc -Wuninitialized -o pointer `frama-c -print-share-path`/e-acsl/e_acsl.c` \
+ monitored_uninitialized.i
+monitored_uninitialized.i: In function 'main':
+monitored_uninitialized.i:44:16: warning: 'x' is used uninitialized in this function\
+[-Wuninitialized]
+\$ ./monitored_uninitialized
+\end{shell}
+
+Actually that is more a design choice that a limitation: if the \eacsl plug-in
+would generate additional instrumentation to prevent such values to be executed,
+the generated code would be much more verbose and much slower.
+
+If you really want to track such unitializations in your annotation, you have to
+manually add calls to the \eacsl predicate
+\lstinline|\initialized|~\cite{eacsl}.
\section{Incomplete Programs}
@@ -36,7 +60,7 @@ plug-in is running (see examples of Sections~\ref{sec:no-main} and
\index{Program!Without main}
\label{sec:limits:no-main}
-The generation is incorrect for every program without main containing a
+The generated program is incorrect for every program without main containing a
memory-related annotations, except if the option
\optionuse{-}{e-acsl-full-mmodel} is provided.
@@ -86,6 +110,18 @@ freed: \valid(x).
\label{sec:limits:no-code}
\index{Function!Without code}
+The generated program is incorrect for every program which contains a
+memory-related annotation $a$ and a function $f$ without code if and only if:
+\begin{itemize}
+\item either $f$ has an (even indirect) effect on a left-value occuring in $a$;
+\item or $a$ is one of the post-condition of $f$.
+\end{itemize}
+
+There is no workaround yet.
+
+Also, the option \optionuse{-}{e-acsl-check} does not verify the annotations of
+function without code. There is also no workaround yet.
+
\section{Recursive Function}
\index{Function!Recursive}
diff --git a/src/plugins/e-acsl/doc/userman/main.pdf b/src/plugins/e-acsl/doc/userman/main.pdf
index 2e7c0e5973cad57c03ed424a9244c69e52e5ef65..681398086ae842db2727d513dce9a2c53009a163 100644
Binary files a/src/plugins/e-acsl/doc/userman/main.pdf and b/src/plugins/e-acsl/doc/userman/main.pdf differ
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index d25c27fcbe94371be601af90c297fc5bcb6c39f9..d6c3dac9fe4d3c0f25e8bf5652bb5c2ba542ea79 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -590,11 +590,31 @@ combination with value and wp
\section{Customization}
\label{sec:custom}
-\begin{itemize}
-\item -e-acsl-project
-\item -e-acsl-check
-\item -eacsl-share
-\end{itemize}
+There are few ways to customize the \eacsl plug-in.
+
+First, the name of the generated project ---which is \texttt{e-acsl} by
+default--- may be changed by setting the option \optiondef{-}{e-acsl-project}.
+
+Second, the directory which the \eacsl library files are searched in ---which is
+\texttt{`frama-c -print-share-path`/e-acsl} by default--- may be changed by
+setting the option \optiondef{-}{e-acsl-share}.
+
+Third, the option \optiondef{-}{e-acsl-check} does not generate any new project
+but it only verifies that each annotation is translatable. Then it produces a
+summary as shown in the following example (left shift in annotation is not
+yet supported by the \eacsl plug-in).
+
+\listingname{check.i}
+\cinput{examples/check.i}
+
+\begin{shell}
+\$ frama-c -e-acsl-check check.i
+<skip preprocessing commands>
+check.i:4:[e-acsl] warning: E-ACSL construct `left/right shift' is not yet supported.
+ Ignoring annotation.
+[e-acsl] 0 annotation was ignored, being untypable.
+[e-acsl] 1 annotation was ignored, being unsupported.
+\end{shell}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 5b32e4fc6b80a32dd471f8bc2ff502617de3aef1..20ea1b4504bd304377269af5c37ea9c4d1e44e13 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -137,7 +137,7 @@ class e_acsl_visitor prj generate = object (self)
Cil.DoChildrenPost
(fun f ->
(* extend the main with forward initialization and put it at end *)
- if not (Options.Check.get ()) then begin
+ if generate then begin
let must_init =
try
Varinfo.Hashtbl.iter
@@ -283,13 +283,13 @@ you must call function `%s' and `__clean' by yourself.@]"
vi.vghost <- false;
(* remember that we have to remove the main later (see method
[vfile]) *)
- if vi.vorig_name = Kernel.MainFunction.get ()
- && not (Options.Check.get ())
- then main_fct <- Some fundec
+ if vi.vorig_name = Kernel.MainFunction.get () then
+ main_fct <- Some fundec
| GVarDecl(_, vi, _) ->
(* do not convert extern ghost variables, because they can't be linked,
see bts #1392 *)
- if vi.vstorage <> Extern then vi.vghost <- false
+ if vi.vstorage <> Extern then
+ vi.vghost <- false
| _ ->
()
in
@@ -297,7 +297,8 @@ you must call function `%s' and `__clean' by yourself.@]"
| GVar(vi, _, _) | GVarDecl(_, vi, _) ->
Varinfo.Hashtbl.replace global_vars vi None
| _ -> ());
- Cil.DoChildrenPost(fun g -> List.iter do_it g; g)
+ if generate then Cil.DoChildrenPost(fun g -> List.iter do_it g; g)
+ else Cil.DoChildren
method vinit vi _off _i =
if generate then
@@ -328,6 +329,7 @@ you must call function `%s' and `__clean' by yourself.@]"
Cil.DoChildren
method private add_generated_variables_in_function f =
+ assert generate;
let vars = Env.get_generated_variables !function_env in
self#reset_env ();
f.slocals <- f.slocals @ List.map fst vars;
@@ -339,16 +341,19 @@ you must call function `%s' and `__clean' by yourself.@]"
vars
method vfunc f =
- let kf = Extlib.the self#current_kf in
- Options.feedback ~dkey ~level:2 "entering in function %a."
- Kernel_function.pretty kf;
- List.iter (fun vi -> vi.vghost <- false) f.slocals;
- Cil.DoChildrenPost
- (fun f ->
- self#add_generated_variables_in_function f;
- Options.feedback ~dkey ~level:2 "function %a done."
- Kernel_function.pretty kf;
- f)
+ if generate then
+ let kf = Extlib.the self#current_kf in
+ Options.feedback ~dkey ~level:2 "entering in function %a."
+ Kernel_function.pretty kf;
+ List.iter (fun vi -> vi.vghost <- false) f.slocals;
+ Cil.DoChildrenPost
+ (fun f ->
+ self#add_generated_variables_in_function f;
+ Options.feedback ~dkey ~level:2 "function %a done."
+ Kernel_function.pretty kf;
+ f)
+ else
+ Cil.DoChildren
method private is_return old_kf stmt =
let old_ret =
@@ -373,10 +378,11 @@ you must call function `%s' and `__clean' by yourself.@]"
(* [JS 2013/05/21] already a warning in pre-analysis *)
(* Options.warning ~once:true "%s@ \
@[The generated program may be incomplete.@]"
- s;*)
+ s;*)
false
- method private literal_string env e =
+ method private literal_string env e =
+ assert generate;
let env_ref = ref env in
let o = object
inherit Cil.genericCilVisitor (Cil.copy_visit (Project.current ()))
@@ -415,7 +421,7 @@ you must call function `%s' and `__clean' by yourself.@]"
let env =
if self#is_first_stmt kf stmt then
(* JS: should be done in the new project? *)
- let env = allocate_function env kf in
+ let env = if generate then allocate_function env kf else env in
(* translate the precondition of the function *)
if Pre_visit.is_generated_function (Extlib.the self#current_kf) then
Project.on prj (Translate.translate_pre_spec kf Kglobal env) !funspec
@@ -449,7 +455,7 @@ you must call function `%s' and `__clean' by yourself.@]"
Use [function_env] to get it back. *)
let env = !function_env in
let env =
- if stmt.ghost then begin
+ if stmt.ghost && generate then begin
stmt.ghost <- false;
(* translate potential RTEs of ghost code *)
let rtes = get_rte_by_stmt kf stmt in
@@ -464,6 +470,7 @@ you must call function `%s' and `__clean' by yourself.@]"
env
in
let mk_block b =
+ assert generate;
let mk b = match b.bstmts with
| [] ->
(match stmt.skind with
@@ -509,54 +516,63 @@ you must call function `%s' and `__clean' by yourself.@]"
in
(* de-allocating memory previously allocating by the kf *)
(* JS: should be done in the new project? *)
- let env = deallocate_function env kf in
- let b, env = Env.pop_and_get env stmt ~global_clear:true Env.After in
- if is_main && Pre_analysis.use_model () then begin
- let stmts = b.bstmts in
- let l = List.rev stmts in
- match l with
- | [] -> assert false (* return is here *)
- | ret :: l ->
- let delete_stmts =
- Globals.Vars.fold_in_file_order
- (fun vi _ acc ->
- if Pre_analysis.must_model_vi vi then
- let vi = Cil.get_varinfo self#behavior vi in
- Misc.mk_delete_stmt vi :: acc
- else
- acc)
- [ Misc.mk_call ~loc:(Stmt.loc stmt) "__clean" []; ret ]
- in
- b.bstmts <- List.rev l @ delete_stmts
- end;
- let new_stmt = mk_block b in
- (* move the labels of the return to the new block in order to
- evaluate the postcondition when jumping to them. *)
- move_labels env stmt new_stmt;
- new_stmt, env
+ if generate then
+ let env = deallocate_function env kf in
+ let b, env =
+ Env.pop_and_get env stmt ~global_clear:true Env.After
+ in
+ if is_main && Pre_analysis.use_model () && generate then begin
+ let stmts = b.bstmts in
+ let l = List.rev stmts in
+ match l with
+ | [] -> assert false (* return is here *)
+ | ret :: l ->
+ let delete_stmts =
+ Globals.Vars.fold_in_file_order
+ (fun vi _ acc ->
+ if Pre_analysis.must_model_vi vi then
+ let vi = Cil.get_varinfo self#behavior vi in
+ Misc.mk_delete_stmt vi :: acc
+ else
+ acc)
+ [ Misc.mk_call ~loc:(Stmt.loc stmt) "__clean" []; ret ]
+ in
+ b.bstmts <- List.rev l @ delete_stmts
+ end;
+ let new_stmt = mk_block b in
+ (* move the labels of the return to the new block in order to
+ evaluate the postcondition when jumping to them. *)
+ move_labels env stmt new_stmt;
+ new_stmt, env
+ else
+ stmt, env
else
- let stmt = rename_alloc_function stmt in
- (* must generate [pre_block] which includes [stmt] before generating
- [post_block] *)
- let pre_block, env =
- Env.pop_and_get env stmt ~global_clear:false Env.After
- in
- let env = mk_post_env (Env.push env) in
- let post_block, env =
- Env.pop_and_get
- env (mk_block pre_block) ~global_clear:false Env.Before
- in
- (* TODO: must clear the local block anytime (?) *)
- mk_block post_block, env
+ if generate then
+ let stmt = rename_alloc_function stmt in
+ (* must generate [pre_block] which includes [stmt] before generating
+ [post_block] *)
+ let pre_block, env =
+ Env.pop_and_get env stmt ~global_clear:false Env.After
+ in
+ let env = mk_post_env (Env.push env) in
+ let post_block, env =
+ Env.pop_and_get
+ env (mk_block pre_block) ~global_clear:false Env.Before
+ in
+ (* TODO: must clear the local block anytime (?) *)
+ mk_block post_block, env
+ else
+ stmt, env
in
function_env := env;
Options.debug ~level:4
"@[new stmt (from sid %d):@ %a@]" stmt.sid Printer.pp_stmt new_stmt;
- new_stmt
+ if generate then new_stmt else stmt
in
Cil.ChangeDoChildrenPost(stmt, mk_block)
method private add_initializer loc checked_lv assigned_lv =
+ assert generate;
let kf = Extlib.the self#current_kf in
let stmt = Extlib.the self#current_stmt in
let may_safely_ignore = function
@@ -579,14 +595,17 @@ you must call function `%s' and `__clean' by yourself.@]"
method vinst = function
| Set(old_lv, _, _) ->
- Cil.DoChildrenPost
- (function
- | [ Set(new_lv, _, loc) ] as l ->
- self#add_initializer loc old_lv new_lv;
- l
- | _ -> assert false)
+ if generate then
+ Cil.DoChildrenPost
+ (function
+ | [ Set(new_lv, _, loc) ] as l ->
+ self#add_initializer loc old_lv new_lv;
+ l
+ | _ -> assert false)
+ else
+ Cil.DoChildren
| Call(Some old_ret, _, _, _) ->
- if Misc.is_generated_kf (Extlib.the self#current_kf) then
+ if not generate || Misc.is_generated_kf (Extlib.the self#current_kf) then
Cil.DoChildren
else
Cil.DoChildrenPost
@@ -644,7 +663,7 @@ you must call function `%s' and `__clean' by yourself.@]"
blk.blocals;
new_blk
in
- Cil.DoChildrenPost handle_memory
+ if generate then Cil.DoChildrenPost handle_memory else Cil.DoChildren
method vexpr exp =
if generate then