diff --git a/src/plugins/e-acsl/doc/userman/examples/gmp.i b/src/plugins/e-acsl/doc/userman/examples/gmp.i
index f7c6511a8a8bbf98f00de7f16cf56c6b80813974..cb203067964042d4da3656b1ce3362f6051242de 100644
--- a/src/plugins/e-acsl/doc/userman/examples/gmp.i
+++ b/src/plugins/e-acsl/doc/userman/examples/gmp.i
@@ -1,7 +1,7 @@
unsigned long long my_pow(unsigned int x, unsigned int n) {
int res = 1;
while (n) {
- if (n & 1) res *= x;
+ if (n & 1) res *= x;
n >>= 1;
x *= x;
}
diff --git a/src/plugins/e-acsl/doc/userman/examples/no_code.c b/src/plugins/e-acsl/doc/userman/examples/no_code.c
new file mode 100644
index 0000000000000000000000000000000000000000..9b76ff82404876b71143faf373a2a9f980ec24f7
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/no_code.c
@@ -0,0 +1,14 @@
+#include "stdio.h"
+
+/*@ behavior even:
+ @ assumes n % 2 == 0;
+ @ ensures \result >= 1;
+ @ behavior odd:
+ @ assumes n % 2 != 0;
+ @ ensures \result >= 1; */
+extern unsigned long long my_pow(unsigned int x, unsigned int n);
+
+int main(void) {
+ unsigned long long x = my_pow(2, 64);
+ return 0;
+}
diff --git a/src/plugins/e-acsl/doc/userman/examples/no_main.i b/src/plugins/e-acsl/doc/userman/examples/no_main.i
index 3ed8a899df06591a39894d0641ac271da84b8cd8..6c21ce10d60b62147e5994827ea953731cf733fe 100644
--- a/src/plugins/e-acsl/doc/userman/examples/no_main.i
+++ b/src/plugins/e-acsl/doc/userman/examples/no_main.i
@@ -3,10 +3,9 @@
@ ensures \result >= 1;
@ behavior odd:
@ assumes n % 2 != 0;
- @ ensures x >= 0 ==> \result >= 1;
- @ ensures x < 0 ==> \result <= -1; */
+ @ \result >= 1; */
unsigned long long my_pow(unsigned int x, unsigned int n) {
- int res = 1;
+ unsigned long long res = 1;
while (n) {
if (n & 1) res *= x;
n >>= 1;
diff --git a/src/plugins/e-acsl/doc/userman/examples/pow.i b/src/plugins/e-acsl/doc/userman/examples/pow.i
new file mode 100644
index 0000000000000000000000000000000000000000..3deda0f62135de3c82cc43dace3849e86e8bd8d7
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/pow.i
@@ -0,0 +1,9 @@
+unsigned long long my_pow(unsigned int x, unsigned int n) {
+ unsigned long long res = 1;
+ while (n) {
+ if (n & 1) res *= x;
+ n >>= 1;
+ x *= x;
+ }
+ return res;
+}
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index 898228436c0fc0a0fe240f08b6f3935ae7bc9982..bdc38a33c342ce287865a4a6369c82cfcd00519b 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -21,12 +21,10 @@ of commercial supports\footnote{Contact us or read
valid)
\end{itemize}
-\section{Program without Main}
+\section{Incomplete Programs}
\index{Program!Without main}
-\label{sec:limits:no-main}
-
-\section{Function without 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 d46bcc712b002c613eb83e6846e06995d66dfe8e..140f0229b2b2ffb4d6f764b2892462e76c9a7de1 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 99cb721ec645d9d9bd593da8e3fa37414db09e44..8c04fe99a92b14e8a5bad010675ea4750b2f8673 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -481,22 +481,24 @@ warning.
[e-acsl] warning: cannot find entry point `main'.
Please use option `-main' for specifying a valid entry point.
The generated program may miss memory instrumentation.
+ if there are memory-related annotations.
[e-acsl] translation done in project "e-acsl".
\end{shell}
This warning indicates that the instrumentation would be incorrect if the
program contains memory-related annotations (see
-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
+Section~\ref{sec:limits:incomplete}). 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
explained in Section~\ref{sec:integers}.
\listingname{main.c}
\cinput{examples/main.c}
\begin{shell}
-\$ gcc -o no_main `frama-c -print-share-path`/e-acsl/e_acsl.c main.c -lgmp
+\$ gcc -o no_main `frama-c -print-share-path`/e-acsl/e_acsl.c \
+ monitored_no_main.i main.c -lgmp
\$ ./no_main
x = 65536
\end{shell}
@@ -507,6 +509,50 @@ x = 65536
\label{sec:no-code}
\index{Function!Without code}
+The \eacsl plug-in may also work if some functions have no implementation.
+Consider for instance the following annotated program for which the
+implementation of the function \texttt{my\_pow} is not provided.
+
+\listingname{no\_code.c}
+\cinput{examples/no_code.c}
+
+The instrumented code is generated as usual, even if you get an additional
+warning.
+\begin{shell}
+[e-acsl] beginning translation.
+[e-acsl] warning: annotated function `my_pow' without code:
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[kernel] warning: No code nor implicit assigns clause for function my_pow,
+generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
+\end{shell}
+
+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
+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
+this particular case, we also need to link against \gmp as explained in
+Section~\ref{sec:integers}.
+
+\listingname{pow.i}
+\cinput{examples/pow.i}
+
+\begin{shell}
+\$ gcc -o no_code `frama-c -print-share-path`/e-acsl/e_acsl.c \
+ pow.i monitored_no_code.i -lgmp
+\$ ./no_code
+Postcondition failed at line 8 in function my_pow.
+The failing predicate is:
+\old(n%2 != 0) ==> \result >= 1.
+\end{shell}
+
+The execution of the corresponding binary fails at runtime: actually, our
+implementation of the function \texttt{my\_pow} that we use several times since
+the beginning of this manual may overflow in case of big exponentiations.
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 4289d1aeb326589de3552238458eddc1f85ea4e9..e3ec7b0847c3a8f6a49f46f3308419143677dd94 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -610,7 +610,8 @@ instrumentation.";
Env.consolidate set
with Globals.No_such_entry_point s ->
Options.warning ~once:true "%s@ \
-@[The generated program may miss memory instrumentation.@]"
+@[The generated program may miss memory instrumentation@ \
+if there are memory-related annotations.@]"
s);
Options.feedback ~level:2 "pre-analysis done.";
Env.consolidated_mem vi
diff --git a/src/plugins/e-acsl/pre_visit.ml b/src/plugins/e-acsl/pre_visit.ml
index f62adb6f482638ce9ec44698125ac3762919d5b7..5fe9ff11f18b2150629fb847939527a808150b6a 100644
--- a/src/plugins/e-acsl/pre_visit.ml
+++ b/src/plugins/e-acsl/pre_visit.ml
@@ -297,6 +297,15 @@ class dup_functions_visitor prj = object (self)
Cil.DoChildrenPost
(fun l -> match l with
| [ GVarDecl(_, vi, _) | GFun({ svar = vi }, _) as g ] ->
+ (match g with
+ | GVarDecl _ ->
+ if vi.vname <> "malloc" && vi.vname <> "free" then
+ Options.warning "@[annotated function `%a' without code:@ \
+the generated program may miss memory instrumentation@ \
+if there are memory-related annotations.@]"
+ Printer.pp_varinfo vi
+ | GFun _ -> ()
+ | _ -> assert false);
let tmp = vi.vname in
if tmp = Kernel.MainFunction.get () then begin
(* the new function becomes the new main: simply swap the name of both
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
index a43ff5bf86fa36871465d5329a6e404a61ac7fc6..dbc2d219818170d1eccfb6ef11a78a3add5e6f4c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
@@ -7,7 +7,8 @@
[e-acsl] beginning translation.
[e-acsl] warning: cannot find entry point `main'.
Please use option `-main' for specifying a valid entry point.
- The generated program may miss memory instrumentation.
+ The generated program may miss memory instrumentation
+ if there are memory-related annotations.
[e-acsl] translation done in project "e-acsl".
/* Generated by Frama-C */
struct __anonstruct___mpz_struct_1 {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
index a43ff5bf86fa36871465d5329a6e404a61ac7fc6..dbc2d219818170d1eccfb6ef11a78a3add5e6f4c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
@@ -7,7 +7,8 @@
[e-acsl] beginning translation.
[e-acsl] warning: cannot find entry point `main'.
Please use option `-main' for specifying a valid entry point.
- The generated program may miss memory instrumentation.
+ The generated program may miss memory instrumentation
+ if there are memory-related annotations.
[e-acsl] translation done in project "e-acsl".
/* Generated by Frama-C */
struct __anonstruct___mpz_struct_1 {
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 04ef1afc4ecdf3328b5925fa399ffb87b46b8006..ec969c8d87a7af09f6f522a393c881c2f57f76d3 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -369,10 +369,11 @@ you must call function `%s' by yourself"
try
let main, _ = Globals.entry_point () in
Kernel_function.equal old_kf main
- with Globals.No_such_entry_point s ->
- Options.warning ~once:true "%s@ \
-@[The generated program may be incomplete.@]"
- s;
+ with Globals.No_such_entry_point _s ->
+ (* [JS 2013/05/21] already a warning in pre-analysis *)
+ (* Options.warning ~once:true "%s@ \
+ @[The generated program may be incomplete.@]"
+ s;*)
false
method private literal_string env e =