diff --git a/src/plugins/e-acsl/doc/userman/examples/gmp.i b/src/plugins/e-acsl/doc/userman/examples/gmp.i
index e2af01141153c258a98e163612724fc6bec76662..f7c6511a8a8bbf98f00de7f16cf56c6b80813974 100644
--- a/src/plugins/e-acsl/doc/userman/examples/gmp.i
+++ b/src/plugins/e-acsl/doc/userman/examples/gmp.i
@@ -1,10 +1,11 @@
 unsigned long long my_pow(unsigned int x, unsigned int n) {
-  int tmp;
-  if (n <= 1) return 1;
-  tmp = my_pow(x, n / 2);
-  tmp *= tmp;
-  if (n % 2 == 0) return tmp;
-  return x * tmp;
+  int res = 1;
+  while (n) {
+    if (n & 1) res *= x;
+    n >>= 1;
+    x *= x;
+  }
+  return res;
 }
 
 int main(void) {
diff --git a/src/plugins/e-acsl/doc/userman/examples/main.c b/src/plugins/e-acsl/doc/userman/examples/main.c
new file mode 100644
index 0000000000000000000000000000000000000000..217e19c45199aa377c8434991332b95b34308886
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/main.c
@@ -0,0 +1,7 @@
+#include "stdio.h"
+
+int main(void) {
+  unsigned long long x = my_pow(2, 16);
+  printf("x = %llu\n",x);
+  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
new file mode 100644
index 0000000000000000000000000000000000000000..3ed8a899df06591a39894d0641ac271da84b8cd8
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/no_main.i
@@ -0,0 +1,16 @@
+/*@ behavior even:
+  @   assumes n % 2 == 0;
+  @   ensures \result >= 1;
+  @ behavior odd:
+  @   assumes n % 2 != 0;
+  @   ensures x >= 0 ==> \result >= 1; 
+  @   ensures x < 0 ==> \result <= -1; */
+unsigned long long my_pow(unsigned int x, unsigned int n) {
+  int 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 c217294ec2cac9aca538c050a6d148570b96123b..898228436c0fc0a0fe240f08b6f3935ae7bc9982 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -21,6 +21,10 @@ of commercial supports\footnote{Contact us or read
   valid)
 \end{itemize}
 
+\section{Program without Main}
+\index{Program!Without main}
+\label{sec:limits:no-main}
+
 \section{Function without Code}
 \index{Function!Without code}
 
diff --git a/src/plugins/e-acsl/doc/userman/main.pdf b/src/plugins/e-acsl/doc/userman/main.pdf
index 1201eb94902065bc03ed7cc54154a51a93b8a221..d46bcc712b002c613eb83e6846e06995d66dfe8e 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 321f8d39722dc42ca101782b432192ea47e7e73f..99cb721ec645d9d9bd593da8e3fa37414db09e44 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -463,13 +463,49 @@ instrumented code.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \subsection{Program without Main}
+\index{Program!Without main}
 
+The \eacsl plug-in may work even if there is no \texttt{main} function.
+Consider for instance the following annotated program without such a
+\texttt{main}.  
 
+\listingname{no\_main.i} 
+\cinput{examples/no_main.i}
+
+The instrumented code is generated as usual, even if you get an additional
+warning.
+\begin{shell}
+\$ frama-c -e-acsl no_main.i -then-on e-acsl -print -ocode monitored_no_main.i
+<skip preprocessing command line>
+[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.
+[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
+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
+\$ ./no_main
+x = 65536
+\end{shell}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \subsection{Function without Code}
 \label{sec:no-code}
+\index{Function!Without code}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%