diff --git a/src/plugins/e-acsl/doc/userman/examples/modified_main.c b/src/plugins/e-acsl/doc/userman/examples/modified_main.c
new file mode 100644
index 0000000000000000000000000000000000000000..c990f33187a8d89bc4b32e2d880c4f89be28e182
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/modified_main.c
@@ -0,0 +1,10 @@
+extern void e_acsl_global_init(void);
+extern void __clean(void);
+extern void f(void);
+
+int main(void) {
+ e_acsl_global_init();
+ f();
+ __clean();
+ return 0;
+}
diff --git a/src/plugins/e-acsl/doc/userman/examples/my_assert.c b/src/plugins/e-acsl/doc/userman/examples/my_assert.c
new file mode 100644
index 0000000000000000000000000000000000000000..4c124e0b1866d7674d034e5017d3fdb8f9caa6c8
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/my_assert.c
@@ -0,0 +1,12 @@
+#include "stdio.h"
+
+void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line)
+{
+ printf("%s at line %d in function %s is %s.\n\
+The verified predicate was: `%s'.\n",
+ kind, line, fct, predicate ? "valid" : "invalid", pred_txt);
+}
diff --git a/src/plugins/e-acsl/doc/userman/examples/valid_no_main.c b/src/plugins/e-acsl/doc/userman/examples/valid_no_main.c
new file mode 100644
index 0000000000000000000000000000000000000000..da6dd0f055bc877a83f5479fd00d6e0a7e874674
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/valid_no_main.c
@@ -0,0 +1,13 @@
+#include "stdlib.h"
+
+extern void *malloc(size_t);
+extern void free(void*);
+
+int f(void) {
+ int *x;
+ x = (int*)malloc(sizeof(int));
+ /*@ assert \valid(x); */
+ free(x);
+ /*@ assert freed: \valid(x); */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index bdc38a33c342ce287865a4a6369c82cfcd00519b..f839e590b08033a7b38569c6203e246ab35f6384 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -22,9 +22,69 @@ of commercial supports\footnote{Contact us or read
\end{itemize}
\section{Incomplete Programs}
+
+Section~\ref{sec:incomplete} explains how the \eacsl plug-in is able to handle
+incomplete programs, which are either programs without main, or programs
+containing functions without bodies.
+
+However, if such programs contain memory-related annotations, the generated code
+may be incorrect. That is made explicit by a warning displayed when the \eacsl
+plug-in is running (see examples of Sections~\ref{sec:no-main} and
+\ref{sec:no-code}).
+
+\subsection{Program without Main}
\index{Program!Without main}
+\label{sec:limits:no-main}
+
+The generation is incorrect for every program without main containing a
+memory-related annotations, except if the option
+\optionuse{-}{e-acsl-full-mmodel} is provided.
+
+Consider the following example.
+
+\listingname{valid\_no\_main.c}
+\cinput{examples/valid_no_main.c}
+
+You can generate the instrumented program as follows.
+\begin{shell}
+\$ frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl valid_no_main.c \
+ -then-on e-acsl -print -ocode monitored_valid_no_main.i
+<skip preprocessing commands>
+[e-acsl] beginning translation.
+<skip warnings about annotations from the Frama-C libc
+ which cannot be translated>
+[kernel] warning: no entry point specified:
+ you must call function `e_acsl_global_init' and `__clean' by yourself.
+[e-acsl] translation done in project "e-acsl".
+\end{shell}
+
+The last warning states an important point: if this program is linked against
+another file containing a \texttt{main} function, then this main function must
+be modified to insert a call to the function
+\texttt{e\_acsl\_global\_init}\codeidx{e\_acsl\_global\_init} at
+the very beginning and a call to the function
+\texttt{\_\_clean}\codeidx{\_\_clean} at the very end like in the following
+example.
+
+\listingname{modified\_main.c}
+\cinput{examples/modified_main.c}
+
+Then just compile and run it as explained in Section~\ref{sec:memory}.
+
+\begin{shell}
+\$ DIR=`frama-c -print-share-path`/e-acsl
+\$ MDIR=\$DIR/memory_model
+\$ gcc -o valid_no_main \$DIR/e_acsl.c \$MDIR/e_acsl_bittree.c \
+ \$MDIR/e_acsl_mmodel.c monitored_valid_no_main.i modified_main.c
+\$ ./valid_no_main
+Assertion failed at line 11 in function f.
+The failing predicate is:
+freed: \valid(x).
+\end{shell}
+
+\subsection{Function without Code}
+\label{sec:limits:no-code}
\index{Function!Without code}
-\label{sec:limits:incomplete}
\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 140f0229b2b2ffb4d6f764b2892462e76c9a7de1..2e7c0e5973cad57c03ed424a9244c69e52e5ef65 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 8c04fe99a92b14e8a5bad010675ea4750b2f8673..d25c27fcbe94371be601af90c297fc5bcb6c39f9 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -343,6 +343,11 @@ We can now execute it as usual.
Since the assertion is valid, there is no output in this case.
+The option \optiondef{-}{e-acsl-gmp-only} (unset by default) may be set to
+always generate \gmp integers, even when it is not required. If it is set, the
+generated program must be linked against \gmp as soon as there is an integer or
+any integral \C type in an annotation.
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Memory-related Annotations}
@@ -378,7 +383,8 @@ must be generated from \texttt{monitored\_valid.i} as follows:
\begin{shell}
\$ DIR=`frama-c -print-share-path`/e-acsl
\$ MDIR=\$DIR/memory_model
-\$ gcc -o valid \$DIR/e_acsl.c \$MDIR/e_acsl_bittree.c \$MDIR/e_acsl_mmodel.c monitored_valid.i
+\$ gcc -o valid \$DIR/e_acsl.c \$MDIR/e_acsl_bittree.c \$MDIR/e_acsl_mmodel.c \
+ monitored_valid.i
\end{shell}
Now we can execute the generate binary which fails at runtime since the second
@@ -417,6 +423,11 @@ The failing predicate is:
mem_access: \valid_read(x).
\end{shell}
+The option \optiondef{-}{e-acsl-full-mmodel} (unset by default) may be set to
+always instrumente the code for handline potential memory-related annotations,
+even when it is not required. If it is set, the generated program must be always
+linked against the memory library.
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Execution Behavior Environment}
@@ -463,6 +474,7 @@ instrumented code.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Program without Main}
+\label{sec:no-main}
\index{Program!Without main}
The \eacsl plug-in may work even if there is no \texttt{main} function.
@@ -487,7 +499,7 @@ warning.
This warning indicates that the instrumentation would be incorrect if the
program contains memory-related annotations (see
-Section~\ref{sec:limits:incomplete}). That is not the case here, so you can
+Section~\ref{sec:limits:no-main}). That is not the case here, so you can
safely ignore it. Now, it is possible to compile the generated code with a \C
compiler in a standard way, and even to link it against additional files like
the following one. In this particular case, we also need to link against \gmp as
@@ -530,7 +542,7 @@ generating default assigns from the prototype
Like in the previous Section, this warning indicates that the instrumentation
would be incorrect if the program contains memory-related annotations (see
-Section~\ref{sec:limits:incomplete}). That is still not the case here, so you
+Section~\ref{sec:limits:no-code}). That is still not the case here, so you
can safely ignore it. Now, it is possible to compile the generated code with a
\C compiler in a standard way, and even to link it against additional files that
provided an implementation for the missing functions like the following one. In
diff --git a/src/plugins/e-acsl/options.ml b/src/plugins/e-acsl/options.ml
index 116b536b441780b80d15891aba42a3e9a1876866..e7e4af5cb0069e97f5d4887ef4917f3011977e22 100644
--- a/src/plugins/e-acsl/options.ml
+++ b/src/plugins/e-acsl/options.ml
@@ -73,14 +73,14 @@ module Gmp_only =
False
(struct
let option_name = "-e-acsl-gmp-only"
- let help = ""
+ let help = "always use GMP integers instead of C integral types"
end)
module Full_mmodel =
False
(struct
let option_name = "-e-acsl-full-mmodel"
- let help = ""
+ let help = "maximal memory-related instrumentation"
end)
let () = Plugin.set_group help
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index e3ec7b0847c3a8f6a49f46f3308419143677dd94..529771ac51896e4d27bd7361ff36219f9f8cf430 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -663,8 +663,10 @@ and must_model_exp ?kf ?stmt e = match e.enode with
| AlignOfE _ -> assert false
let must_model_vi ?kf ?stmt vi =
- Options.Full_mmodel.get ()
- || Error.generic_handle (must_model_vi ?kf ?stmt) false vi
+ not (Cil.isFunctionType vi.vtype || (vi.vghost && vi.vstorage = Extern))
+ &&
+ (Options.Full_mmodel.get ()
+ || Error.generic_handle (must_model_vi ?kf ?stmt) false vi)
let must_model_lval ?kf ?stmt lv =
Options.Full_mmodel.get ()
@@ -674,7 +676,7 @@ let old_must_model_vi bhv ?kf ?stmt vi =
Options.Full_mmodel.get ()
|| must_model_vi ?kf ?stmt (Cil.get_original_varinfo bhv vi)
-let use_model () = not (Env.is_empty ())
+let use_model () = not (Env.is_empty ()) || Options.Full_mmodel.get ()
(*
Local Variables:
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index ec969c8d87a7af09f6f522a393c881c2f57f76d3..5b32e4fc6b80a32dd471f8bc2ff502617de3aef1 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -226,7 +226,7 @@ class e_acsl_visitor prj generate = object (self)
let new_globals =
List.fold_right
(fun g acc -> match g with
- | GFun({ svar = vi }, _)
+ | GFun({ svar = vi }, _)
when Varinfo.equal vi main.svar ->
acc
| _ -> g :: acc)
@@ -235,8 +235,8 @@ class e_acsl_visitor prj generate = object (self)
in
f.globals <- new_globals
| None ->
- Kernel.warning "no entry point specified:@ \
-you must call function `%s' by yourself"
+ Kernel.warning "@[no entry point specified:@ \
+you must call function `%s' and `__clean' by yourself.@]"
fname;
f.globals <- f.globals @ [ cil_fct ]
in