[E-ACSL] manual

src/plugins/e-acsl/doc/userman/biblio.bib

@@ -130,3 +130,15 @@
   note = {Submitted for publication},
 }
   
+@inproceedings{pathcrawler,
+  author =	 {Bernard Botella and Mickal Delahaye and Stphane
+                  Hong-Tuan-Ha and Nikolai Kosmatov and Patricia Mouy
+                  and Muriel Roger and Nicky Williams},
+  title =	 {Automating Structural Testing of {C} Programs:
+                  Experience with {PathCrawler}},
+  booktitle =	 {the 4th Int. Workshop on Automation
+               of Software Test {(AST 2009)}},
+  pages =	 {70--78},
+  year =	 2009,
+  publisher =	 {{IEEE} Computer Society},
+}

src/plugins/e-acsl/doc/userman/examples/archi.c

-#define ARCH_BITS 64 /* consider a 64 bits architecture */
+#define ARCH_BITS 64 /* assume a 64 bits architecture */
 
 #if ARCH_BITS == 32
 #define SIZEOF_LONG 4

src/plugins/e-acsl/doc/userman/introduction.tex

@@ -3,22 +3,23 @@
 \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 a \C code which fails at runtime if an annotation is
+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
-checking~\cite{runtime-assertion-checking}\footnote{In our context, ``runtime
+a \C code, in particular to perform what is usually called ``runtime assertion
+checking''~\cite{runtime-assertion-checking}\footnote{In our context, ``runtime
   annotation checking'' would be a better more-general expression.}. That is the
 primary goal of \eacsl. Second it allows to combine \framac and its existing
-analyzers, with other analyzer tools for \C, even those who do not understand
-the \acsl specification language. Third, the possibility to detect invalid
-annotations during a concrete execution may be very helpful while writing a
-correct specification of a given program, \emph{e.g.} for later program proving.
-Finally, an executable specification makes it possible to check runtime
-assertions that cannot be verified statically and to establish a link between
-monitoring tools and static analysis tools like
+analyzers, with other analyzer tools for \C like
+\pathcrawler~\cite{pathcrawler}, even those who do not understand the \acsl
+specification language. Third, the possibility to detect invalid annotations
+during a concrete execution may be very helpful while writing a correct
+specification of a given program, \emph{e.g.} for later program proving.
+Finally, an executable specification makes it possible to check at runtime
+assertions that cannot be verified statically and thus to establish a link
+between monitoring tools and static analysis tools like
 \valueplugin~\cite{value}\index{Value} or \wpplugin~\cite{wp}\index{Wp}.
 
 Annotations must be written in the \eacsl specification

src/plugins/e-acsl/doc/userman/macros.tex

@@ -11,7 +11,8 @@
 \newcommand{\jml}{\textsc{JML}\xspace}
 \newcommand{\valueplugin}{\textsc{Value}\xspace}
 \newcommand{\wpplugin}{\textsc{Wp}\xspace}
-\newcommand{\gcc}{\textsc{gcc}\xspace}
+\newcommand{\pathcrawler}{\textsc{PathCrawler}\xspace}
+\newcommand{\gcc}{\textsc{Gcc}\xspace}
 \newcommand{\gmp}{\textsc{GMP}\xspace}
 
 \newcommand{\nodiff}{\emph{No difference with \acsl.}}