[E-ACSL] version 0.2 ready to be released

src/plugins/e-acsl/Makefile.in

@@ -96,7 +96,7 @@ PLUGIN_GENERATED:= $(PLUGIN_DIR)/local_config.ml
 
 EACSL_VERSION=$(shell $(SED) -e 's/\\(.*\\)/\\1/' VERSION)
 
-$(PLUGIN_DIR)/local_config.ml: $(PLUGIN_DIR)/Makefile.in
+$(PLUGIN_DIR)/local_config.ml: $(PLUGIN_DIR)/Makefile.in VERSION
 	$(PRINT_MAKING) $@
 	$(RM) $@
 	$(ECHO) "(* This file was automatically generated from $<. Don't edit it. *)" >> $@
@@ -146,12 +146,14 @@ uninstall::
 
 EXPORT	=e-acsl-$(EACSL_VERSION)
 
+DOC_FILES= doc/manuals/e-acsl-manual.pdf  \
+	doc/manuals/e-acsl.pdf doc/manuals/e-acsl-implementation.pdf
+
 DISTRIB_FILES= $(filter-out $(wildcard *local_config.ml), $(wildcard *.ml)) \
 	$(wildcard *.mli) \
 	configure.ac Makefile.in \
 	doc/Changelog \
-	doc/manuals/e-acsl-manual.pdf  \
-	doc/manuals/e-acsl.pdf doc/manuals/e-acsl-implementation.pdf \
+	$(DOC_FILES) \
 	share/e-acsl/*.[ch] share/e-acsl/memory_model/*.[ch] \
 	tests/test_config.in \
 	tests/e-acsl-reject/test_config tests/e-acsl-reject/*.i \
@@ -186,6 +188,13 @@ WWW	= /localhome/julien/frama-c/doc/www
 e-acsl-install-distrib: e-acsl-distrib
 	$(PRINT) Copying to website
 	$(CP) $(EXPORT).tar.gz $(WWW)/distrib/download/e-acsl
+	$(CP) $(DOC_FILES) $(WWW)/distrib/download/e-acsl
+	$(CP) doc/manuals/e-acsl-manual.pdf \
+	      $(WWW)/distrib/download/e-acsl/e-acsl-manual-$(EACSL_VERSION).pdf
+	$(CP) doc/manuals/e-acsl.pdf \
+	      $(WWW)/distrib/download/e-acsl/e-acsl-1.7.pdf
+	$(CP) doc/manuals/e-acsl-implementation.pdf \
+	      $(WWW)/distrib/download/e-acsl/e-acsl-implementation-$(EACSL_VERSION).pdf
 
 ##########
 # Header #

src/plugins/e-acsl/VERSION

-0.1+dev
+0.2

src/plugins/e-acsl/doc/Changelog

@@ -20,12 +20,12 @@
 -* E-ACSL       [2013/01/09] Fix bug when translating a postcondition of a
 	        function where the init state is the same than the final
 	        state (bts #!1300).
--  E-ACSL       [2013/01/09] Support of specified function without code.
+-  E-ACSL       [2013/01/09] Support of undefined function with a contract.
 -  E-ACSL       [2012/12/20] Support of ghost variables and statements.
 -* E-ACSL       [2012/12/13] Fix bug with complex term left-values.
 -  E-ACSL       [2012/11/27] Support of \valid_read.
 -  E-ACSL       [2012/11/27] Prevent runtime errors in annotations, except
-	        unitialized variables.
+	        uninitialized variables.
 -  E-ACSL       [2012/11/19] Support of floats in annotations. Approximate
 	        reals by floats.
 -  E-ACSL       [2012/10/25] Support of \valid.

src/plugins/e-acsl/doc/refman/Makefile

@@ -18,8 +18,8 @@ e-acsl: e-acsl-implementation.pdf e-acsl.pdf main.pdf
 
 all: e-acsl
 
-LANGUAGE_VERSION=1.6+dev
-EACSL_VERSION= 0.1+dev
+LANGUAGE_VERSION=1.7
+EACSL_VERSION= 0.2
 
 EACSL_DIR=$(HOME)/plugins/e-acsl
 DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib

src/plugins/e-acsl/doc/refman/binders.tex

@@ -7,7 +7,7 @@
   type-expr ::= logic-type-expr | C-type-expr
   \
   logic-type-expr ::= built-in-logic-type ;
-  | id ; type id
+  | id ; type identifier
   \
   built-in-logic-type ::= "boolean" | "integer" | { "real" }
   \

src/plugins/e-acsl/doc/refman/changes_modern.tex

@@ -3,7 +3,7 @@
 \subsection{Version \version}
 
 \begin{itemize}
-\item Update according to \acsl 1.6.
+\item Update according to \acsl 1.7.
 \item \changeinsection{separation}{no more absent}
 \end{itemize}
 

src/plugins/e-acsl/doc/refman/eacslversion.tex

-\newcommand{\eacslversion}{0.1+dev}
+\newcommand{\eacslversion}{0.2}

src/plugins/e-acsl/doc/refman/main.tex

@@ -25,8 +25,8 @@
 \usepackage{alltt}
 \makeindex
 
-\newcommand{\acslversion}{1.6\xspace}
-\newcommand{\version}{\acslversion+dev\xspace}
+\newcommand{\acslversion}{1.7\xspace}
+\newcommand{\version}{\acslversion\xspace}
 
 \renewcommand{\textfraction}{0.01}
 \renewcommand{\topfraction}{0.99}

src/plugins/e-acsl/doc/refman/model.tex

 \begin{syntax}
   declaration ::= C-declaration ;
   | {"/*@" "model" parameter ";" "*/"} ; model variable
-  | "/*@" "model" C-type "{" parameter ";"? "}" ";" "*/" ; model field
-  | { "/*@" "model" C-declaration "*/" } ; model variable
+  | { "/*@" "model" C-type "{" parameter ";"? "}" ";" "*/" } ; model field
 \end{syntax}

src/plugins/e-acsl/doc/refman/predicate.tex

@@ -26,6 +26,7 @@
        | [ { "\forall" binders ";" pred } ]; univ. quantification
        | [ { "\exists" binders ";" pred } ]; exist. quantification
        | id ":" pred ; syntactic naming
+       | string ":" pred ; syntactic naming
        \
   [ integer-guards ] ::= [ interv  ("&&" interv)* ]
        \

src/plugins/e-acsl/doc/refman/speclang_modern.tex

@@ -45,6 +45,12 @@ only difference between \eacsl and \acsl predicates are quantifications.
 \label{fig:gram:binders}
 \end{figure}
 
+\begin{notimplementedenv}
+  Reals are not correctly supported by the \eacsl plug-in right now. Only
+  floating point numbers are supported: real constants and operations are seen as
+  \C floating point constants and operations.
+\end{notimplementedenv}
+
 \subsection*{Quantification}
 \eacsl quantification must be computable. They are limited to two limited forms.
 

src/plugins/e-acsl/doc/refman/term.tex

 \begin{syntax}
-  bin-op ::= "+" | "-" | "*" | [ "/" ] | [ "%" ];
+  literal ::= { "\true" } | { "\false" } ; boolean constants
+       | integer ; integer constants
+       | real ; real constants
+       | string ; string constants
+       | character ; character constants
+       \ 
+  bin-op ::= "+" | "-" | "*" | [ "/" ] | [ "%" ] | { "<<" } | { ">>" };
        | "==" | "!=" | "<=" | ">=" | ">" | "<" ;
-       | [ "&&" ] | [ "||" ] |   ; boolean operations
-       | { "&" } | { "|" } | { "-->" }
-       | { "<-->" } | "^" ; bitwise operations
+       | [ "&&" ] | [ "||" ] | [ "^^" ] ; boolean operations
+       | { "&" } | { "|" } | { "-->" } | { "<-->" } | "^" ; bitwise operations
        \
   unary-op ::= "+" | "-" ; unary plus and minus
        | "!" ; boolean negation
@@ -11,9 +16,7 @@
        | [ "*" ]; pointer dereferencing
        | "&" ; address-of operator
        \
-  term ::= { "\true" } | { "\false" };
-       | integer ; integer constants
-       | { real } ; real constants
+  term ::= literal ; literal constants
        | id ; variables
        | unary-op term ;
        | term bin-op term ;
@@ -30,4 +33,5 @@
        | "sizeof" "(" term ")" ;
        | "sizeof" "(" C-type-expr ")" ;
        | id ":" term ; syntactic naming
+       | string ":" term ; syntactic naming
 \end{syntax}

src/plugins/e-acsl/doc/userman/Makefile

@@ -13,7 +13,7 @@ default: main.pdf
 
 main.pdf: $(DEPS_MODERN)
 
-EACSL_VERSION= 0.1+dev
+EACSL_VERSION= 0.2
 FC_VERSION= Fluorine-20130501
 
 EACSL_DIR=$(HOME)/plugins/e-acsl
@@ -21,7 +21,7 @@ DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
 install: 
 	cp -f main.pdf $(EACSL_DIR)/doc/manuals/e-acsl-manual.pdf
 	cp -f main.pdf \
-	  $(DISTRIB_DIR)/download/e-acsl/e-acsl-$(EACSL_VERSION).pdf
+	  $(DISTRIB_DIR)/download/e-acsl/e-acsl-manual-$(EACSL_VERSION).pdf
 
 include $(EACSL_DIR)/doc/support/MakeLaTeXModern
 

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

-\newcommand{\eacslversion}{0.1+dev\xspace}
+\newcommand{\eacslversion}{0.2\xspace}
 \newcommand{\fcversion}{Fluorine-20130501\xspace}