[e-acsl] Hollydays works (now ready for alpha release):

* fixes bug:
  - fixed bug in quantifications when the bound variable got C type
  - fixed bug with DEV_FLAGS in Makefile.in
* implements new E-ACSL features:
  - invariant as assertion
  - existential quantification \exists over integers
  - equivalence <==>
  - \at as a predicate
  - conditional _ ? _ : _ (for terms and predicates)
  - binary boolean operations over terms
  - mixed assumes and ensures in function contracts
* other new features:
  - better error messages when runtime checks fail 
    (replace e_acsl_fail by e_acsl_assert)
  - remove option -e-acsl-assert
  - add E-ACSL manuals in doc/manuals
  - add files doc/Changelog, INSTALL, README and VERSION
  - new option -e-acsl-version
  - check Frama-C version at configure
  - make src-distrib
  - header 2012

src/plugins/e-acsl/E_ACSL.mli

 (**************************************************************************)
 (*                                                                        *)
-(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
 (*                                                                        *)
-(*  Copyright (C) 2011                                                    *)
+(*  Copyright (C) 2012                                                    *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)

src/plugins/e-acsl/INSTALL

+			   -------------------------
+			   INSTALLATION INSTRUCTIONS
+			   -------------------------
+
+===============================================================================
+				    SUMMARY
+===============================================================================
+
+0)  Summary
+1)  Quick Start
+2)  Requirements
+3)  Configuration
+4)  Compilation
+5)  Installation
+6)  Custom Installation
+7)  Testing the Installation
+8)  Uninstallation
+9)  Have Fun with E-ACSL!
+
+===============================================================================
+				  QUICK START
+===============================================================================
+
+1) Install Frama-C if not already installed.
+
+2a) On Linux-like distribution:
+  ./configure && make && sudo make install
+
+2b) On Windows+Cygwin or Windows+MinGW+msys:
+  ./configure --prefix C:/windows/path/with/direct/slash && make && make install
+
+4) Optionally, test your installation by running:
+   frama-c.byte -e-acsl tests/e-acsl-runtime/true.i -then-on e-acsl -print
+   frama-c -e-acsl tests/e-acsl-runtime/true.i -then-on e-acsl -print
+
+See below for more detailed and specific instructions.
+
+===============================================================================
+				  REQUIREMENTS
+===============================================================================
+
+- GNU make version >= 3.81
+- Objective Caml >= 3.10.2;
+- Frama-C = Nitrogen-20111001 
+  (no warranty that this plug-in works with more recent version of Frama-C)
+
+- The native version of the plug-in is only available if native dynamic linking
+  feature of OCaml is available on your system (see Frama-C User Manual, 
+  Section 3.1). 
+- Optionally, the GMP library >= ???
+  It is required to run the tests and to run the generated programs, 
+  but not to run the plug-in through Frama-C.
+
+===============================================================================
+				 CONFIGURATION
+===============================================================================
+
+The E-ACSL plug-in is configured by "./configure [options]"
+
+configure is generated by autoconf, so that the standard options for setting
+installation directories are available, in particular '--prefix=/path'.
+
+Under Cygwin or MinGW:
+----------------------
+Use "./configure --prefix C:/windows/path/with/direct/slash".
+
+===============================================================================
+				  COMPILATION
+===============================================================================
+
+Type "make".
+
+Makefile targets of interest are:
+- doc	   generates the API documentation
+
+===============================================================================
+				  INSTALLATION
+===============================================================================
+
+Type "make install"
+(depending on the installation directory, may require superuser privileges).
+
+It is possible to install in a given directory by setting
+the DESTDIR variable: "make install DESTDIR=/tmp" installs Frama-C in
+sub-directories of /tmp.
+
+The following files are installed.
+
+Object files: (usually in `frama-c -print-plugin-path`)
+-------------
+- E_ACSL.cmi
+- E_ACSL.cmo
+- E_ACSL.cmxs (only if native dynamic linking of OCaml is available)
+
+Shared files: (usually in `frama-c -print-share-path`/e-acsl)
+-------------
+- e_acsl.h
+- e_acsl_gmp.h
+- e_acsl_gmp_types.h
+
+Manuals: (usually in `frama-c -print-share-path`/manuals)
+--------
+- e-acsl.pdf
+- e-acsl-implementation.pdf
+
+===============================================================================
+			      CUSTOM INSTALLATION
+===============================================================================
+
+You can manually move any installed files. However, in such a case, you have to
+set specific environment variables in order that Frama-C found the appropriate
+objects when required.
+
+The environment variables are:
+------------------------------
+FRAMAC_SHARE: absolute path to the Frama-C share subdirectory
+FRAMAC_LIB: absolute path of the Frama-C lib subdirectory
+FRAMAC_PLUGIN: absolute path of the Frama-C plug-in directory.
+
+===============================================================================
+			    TESTING THE INSTALLATION
+===============================================================================
+
+This step is optional.
+
+Test your installation by running:
+  frama-c.byte -e-acsl tests/e-acsl-runtime/true.i -then-on e-acsl -print
+  frama-c -e-acsl tests/e-acsl-runtime/true.i -then-on e-acsl -print
+
+The second command only works if native dynamic linking of OCaml is available 
+on your system.
+
+===============================================================================
+				 UNINSTALLATION
+===============================================================================
+
+Type "make uninstall" to remove Frama-C and all the installed plug-ins.
+That works only if you have not manually moved the installed files (see Section
+"Custom Installation").
+
+===============================================================================
+			     HAVE FUN WITH E-ACSL!
+===============================================================================

src/plugins/e-acsl/Makefile.in

 ##########################################################################
 #                                                                        #
-#  This file is part of the E-ACSL plug-in of Frama-C.                   #
+#  This file is part of the Frama-C's E-ACSL plug-in.                    #
 #                                                                        #
-#  Copyright (C) 2011                                                    #
+#  Copyright (C) 2012                                                    #
 #    CEA (Commissariat  l'nergie atomique et aux nergies              #
 #         alternatives)                                                  #
 #                                                                        #
@@ -20,6 +20,10 @@
 #                                                                        #
 ##########################################################################
 
+#######################
+# Frama-C Environment #
+#######################
+
 # Do not use ?= to initialize both below variables
 # (fixed efficiency issue, see GNU Make manual, Section 8.11)
 ifndef FRAMAC_SHARE
@@ -29,6 +33,19 @@ ifndef FRAMAC_LIBDIR
 FRAMAC_LIBDIR :=$(shell frama-c -journal-disable -print-libpath)
 endif
 
+# OCAMLVERSION and HAS_OCAML312 are defined in Frama-C common Makefile
+# but cannot be used at this point
+OCAMLVERSION 	?=@OCAMLVERSION@
+ifeq ($(findstring 3.12,$(OCAMLVERSION)),)
+HAS_OCAML312 = no
+else
+HAS_OCAML312 = yes
+endif
+
+#########################
+# Plug-in configuration #
+#########################
+
 PLUGIN_DIR ?=.
 PLUGIN_ENABLE:=@ENABLE_E_ACSL@
 PLUGIN_DYNAMIC:=@DYNAMIC_E_ACSL@
@@ -46,13 +63,16 @@ PLUGIN_CMO:= local_config \
 	main
 PLUGIN_HAS_MLI:=yes
 
-# Enable -warn-error, but do not distribute the plug-in with this option being
-# activated 
+# Enable -warn-error in development mode, but not in distribution mode
+# Do not edit the line below: it is automatically set by 'make src-distrib'
+IS_DISTRIBUTED:=no
+ifneq ($(IS_DISTRIBUTED),yes)
 ifeq ($(HAS_OCAML312),yes)
 DEV_FLAGS=-warn-error +a
 else
 DEV_FLAGS=-warn-error A
 endif
+endif
 PLUGIN_BFLAGS:=$(DEV_FLAGS)
 PLUGIN_OFLAGS:=$(DEV_FLAGS)
 
@@ -60,13 +80,20 @@ PLUGIN_DISTRIBUTED:=no
 
 PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
 PLUGIN_DISTRIB_BIN:=no
+
+#######################
+# Local configuration #
+#######################
+
 PLUGIN_GENERATED:= $(PLUGIN_DIR)/local_config.ml
 
+VERSION=$(shell $(SED) -e 's/\\(.*\\)/\\1/' VERSION)
+
 $(PLUGIN_DIR)/local_config.ml: $(PLUGIN_DIR)/Makefile.in
 	$(PRINT_MAKING) $@
 	$(RM) $@
 	$(ECHO) "(* This file was automatically generated from $<. Don't edit it. *)" >> $@
-	$(ECHO) "let may_use_assert = @MAY_USE_ASSERT@" >> $@
+	$(ECHO) "let version = \""$(VERSION)"\"" >> $@
 	$(CHMOD_RO) $@
 
 ###########
@@ -95,10 +122,56 @@ install::
 	$(PRINT_CP) E-ACSL share files
 	$(MKDIR) $(FRAMAC_SHARE)/e-acsl
 	$(CP) $(E_ACSL_DIR)/share/e-acsl/* $(FRAMAC_SHARE)/e-acsl
+	$(CP) $(E_ACSL_DIR)/doc/manuals/e-acsl.pdf \
+		$(E_ACSL_DIR)/doc/manuals/e-acsl-implementation.pdf \
+		$(FRAMAC_SHARE)/manuals
 
 uninstall::
 	$(PRINT_RM) E-ACSL share files
 	$(RM) -r $(FRAMAC_SHARE)/e-acsl
+	$(RM) $(FRAMAC_SHARE)/manuals/e-acsl.pdf \
+		$(FRAMAC_SHARE)/manuals/e-acsl-implementation.pdf
+
+################################
+# Building source distribution #
+################################
+
+EXPORT	=e-acsl-$(VERSION)
+
+DISTRIB_FILES= $(filter-out $(wildcard *local_config.ml), $(wildcard *.ml)) \
+	$(wildcard *.mli) \
+	configure.ac Makefile.in \
+	doc/Changelog \
+	doc/manuals/e-acsl.pdf doc/manuals/e-acsl-implementation.pdf \
+	share/e-acsl/*.h \
+	tests/test_config.in \
+	tests/e-acsl-reject/test_config tests/e-acsl-reject/*.i \
+	tests/e-acsl-runtime/test_config tests/e-acsl-runtime/*.i \
+	license/CEA_LGPL license/headache_config.txt license/LGPLv2.1 \
+	INSTALL README VERSION .depend
+
+src-distrib: .depend
+	$(PRINT_TAR) tmp-distrib
+	$(TAR) cf tmp.tar $(DISTRIB_FILES)
+	$(PRINT_MAKING) export directories
+	$(MKDIR) $(EXPORT)
+	$(PRINT_UNTAR) tmp-distrib
+	cd $(EXPORT); \
+	  $(TAR) xf ../tmp.tar; autoconf; \
+	  $(SED) -i -e 's/IS_DISTRIBUTED:=no/IS_DISTRIBUTED:=yes/' Makefile.in
+	$(PRINT_RM) tmp-distrib
+	$(RM) tmp.tar
+	$(PRINT_MAKING) test directories
+	for dir in $(EXPORT)/tests/*; do \
+	  if test -d $$dir; then \
+	    $(MKDIR) $$dir/result; \
+	    $(MKDIR) $$dir/oracle; \
+          fi \
+	done
+	$(PRINT_MAKING) archive
+	$(TAR) czf $(EXPORT).tar.gz $(EXPORT)
+	$(PRINT) Cleaning
+	$(RM) -fr $(EXPORT)
 
 ##########
 # Header #

src/plugins/e-acsl/README

+				------
+				README
+				------
+
+===============================================================================
+				SUMMARY
+===============================================================================
+
+0) Summary
+1) What Is
+2) Simple use
+3) Examples
+4) Advanced uses
+5) Compatibility with previous releases
+6) Have Fun with E-ACSL!
+
+===============================================================================
+				WHAT IS
+===============================================================================
+
+This package contains the Frama-C's E-ACSL plug-in. It takes as input an 
+annotated C program and returns the same program in which annotations have 
+been converted into C code dedicated to runtime assertion checking: this code 
+fails at runtime if and only if the annotation is wrong in the execution 
+context.
+
+Annotations must be written in a subset of ACSL (ANSI/ISO C Specification 
+Language), namely E-ACSL (Executable ANSI/ISO C Specification Language). E-ACSL
+is fully described in file doc/manuals/e-acsl.pdf.
+
+This plug-in is still under implementation: some parts of E-ACSL are not yet 
+implemented. What is supported is described in file 
+doc/manuals/e-acsl-implementation.pdf.
+
+Please read file INSTALL for details about the installation procedure of
+this plug-in and consult http://frama-c.com and http://frama-c.com/e-acsl 
+for information about Frama-C and ACSL.
+
+===============================================================================
+				SIMPLE USE
+===============================================================================
+
+The standard use is the following:
+
+$ frama-c -e-acsl <files> -then-on e-acsl -print -ocode generated_code.c
+
+Option -e-acsl runs the Frama-C's E-ACSL plug-in on the given <files>: it
+returns a new Frama-C project called `e-acsl'. Option -then-on switches to 
+this project while options -print and -ocode pretty prints the corresponding C 
+code into file `generated_code'.
+
+Here the only E-ACSL specific option is -e-acsl. The others (-then-on, -print
+and -ocode) are standard Frama-C options, described in the Frama-C User Manual
+as well as the concept of Frama-C Project. 
+
+The generated file is a C file which usually depends on the GMP library
+(http://???).  The following commands compile and run it:
+
+$ gcc generated_code.c -lgmp -o generated_code
+$ ./generated_code
+
+The execution behaves in the same way than the original <files>, except that 
+it fails if an annotation is violated.
+
+===============================================================================
+				EXAMPLES
+===============================================================================
+
+1) Consider the following C program:
+<true.i>
+int main(void) {
+  /*@ assert \true; */
+  return 0;
+}
+
+Since the assertion is always true, the generated code behaves in the same way 
+that just returning 0:
+$ frama-c -e-acsl true.i -then-on e-acsl -print -ocode gen_true.c
+$ gcc gen_true.c -o gen_true
+$ ./gen_true
+$ echo $?
+0
+
+As this example is trivial, the generated code does not require to be linked
+against GMP. It is usually not the case.
+
+2) Now consider the following C program:
+<false.i>
+int main(void) {
+  int x = 0;
+  /*@ assert x+1 == 0; */
+  return 0;
+}
+
+Since the assertion is always false, the generated code fails at runtime:
+$ frama-c -e-acsl false.i -then-on e-acsl -print -ocode gen_false.c
+$ gcc gen_false.c -lgmp -o gen_false
+$ ./gen_false
+Assertion failed at line 7.
+The failing predicate is:
+(x+1 == 0).
+$ echo $?
+1
+
+As this example uses arithmetic in annotations, the generated code must be
+linked against GMP (GCC's option -lgmp) to be able to produce an executable.
+
+3) More advanced examples are available in directory tests/e-acsl-runtime. Note
+   that these examples never fail at runtime: all the annotations are valid.
+
+===============================================================================
+				ADVANCED USES
+===============================================================================
+
+This E-ACSL plug-in is fully integrated within Frama-C: any standard Frama-C
+options may be used in order to custom the Frama-C execution. Read the Frama-C
+User Manual for additional information.
+
+The list of E-ACSL option is available through the option -e-acsl-help:
+$ frama-c -e-acsl-help
+
+As this example is trivial, the generated code does not require to be linked
+against GMP. It is usually not the case.
+
+2) Now consider the following C program:
+<false.i>
+int main(void) {
+  int x = 0;
+  /*@ assert x+1 == 0; */
+  return 0;
+}
+
+Since the assertion is always false, the generated code fails at runtime:
+$ frama-c -e-acsl false.i -then-on e-acsl -print -ocode gen_false.c
+$ gcc gen_false.c -lgmp -o gen_false
+$ ./gen_false
+Assertion failed at line 7.
+The failing predicate is:
+(x+1 == 0).
+$ echo $?
+1
+
+As this example uses arithmetic's in annotations, the generated code must be
+linked against GMP (GCC's option -lgmp) to be able to produce an executable.
+
+3) More advanced examples are available in directory tests/e-acsl-runtime. Note
+   that these examples never fail at runtime: all the annotations are valid.
+
+===============================================================================
+				ADVANCED USES
+===============================================================================
+
+This E-ACSL plug-in is fully integrated within Frama-C: any standard Frama-C
+options may be used in order to custom the Frama-C execution. Read the Frama-C
+User Manual for additional information.
+
+The list of E-ACSL option is available through the option -e-acsl-help:
+$ frama-c -e-acsl-help
+
+These options are the following.
+-e-acsl             generate a new project where E-ACSL annotations are
+                    translated to executable C code
+-e-acsl-check       only type check E-ACSL annotated program
+-e-acsl-project <prj>  the name of the generated project is <prj> (default to
+                    "e-acsl")
+
+-e-acsl-help        help of plug-in E-ACSL
+-e-acsl-h           alias for option -e-acsl-help
+-e-acsl-version     version of plug-in E-ACSL
+
+-e-acsl-debug <n>   level of debug for plug-in E-ACSL (defaults to 0)
+-e-acsl-verbose <n>  level of verbosity for plug-in E-ACSL (defaults to 1)
+
+The generated code contains fresh variable names prefixed by 'e_acsl'. No
+verification is done to ensure that these new names do not clash with existing
+ones. Thus be sure that your input program does not contain any variable
+prefixed by 'e_acsl'. A direct consequence is that it is not possible to give as
+input to the E-ACSL plug-in a program generated by E-ACSL itself.
+
+===============================================================================
+			COMPATIBILITY WITH PREVIOUS RELEASES
+===============================================================================
+
+Changes are documented in a textual way in file Changelog.
+
+===============================================================================
+				HAVE FUN WITH E-ACSL!
+===============================================================================

src/plugins/e-acsl/TODO

@@ -2,50 +2,25 @@
 # NEXT RELEASE #
 ################
 
-- quantifications sur les entiers
-- mixed assumes and ensures in contracts
-- utiliser Options.use_asserts
+- vérifier le code de la division et du modulo 
+  (div et modulo mathématiques différents des div et modulo de l'ANSI C99)
+- voir les ??? dans le INSTALL et le README
 
 ########
 # CODE #
 ########
 
+- grep TODO *.ml*
 - Env.new_var*: ajouter la varinfo en sortie de la fonction ?
-- function contracts for functions only declared
-  ==> le noyau génère un "assigns \nothing" pour ces fonctions...
-  ce assign n'est de toute façon pas gérer
-- multi ensures or multi requirements, their conjunctions and undefinedness
-  	[JS 2011/12/06] c'est quoi çà ? :-(
 - gestion des initialiseurs des globals: requiert un main
 - mkcall ne devrait pas générer de nouvelles variables pour une même fonction
-- garde pour les casts quand overflows potentiels
-  (même pas de warnings aujourd'hui)
-- constante entière longue: utiliser la représentation sous forme de string et 
-  rechercher la base appropriée.
-- arithmetic overflows
-- [Bernard] avoir une fonction 
-  e_acsl_assert(int guard, char *msg, char *kind) {
-    if (guard) e_acsl_fail(msg, kind);
-  }
-à appeler au lieu de générer la garde. La kind est le type de l'annotation 
-(assert, requires, ensures, RTE? ...)
-- [Bernard] avoir une fonction
-  e_acsl_trace_behavior(char *bhv_name) {}
-à appeler dès qu'un behavior est activé
-- meilleur schéma de compilation des assumes (not possible in multi-bhv?):
-  if (assume_bhv) {
-    e_acsl_trace_behavior(bhv_name);
-    requires_bhv;
-    run_function;
-    ensures_bhv;
-  }
-- utiliser Rte (get_rte_annotations dans Oxygen)
+- [Bernard] avoir une fonction e_acsl_trace_behavior(char *bhv_name) {}
+  à appeler dès qu'un behavior est activé
+- utiliser Rte pour tous les overflows potentiels
+  (get_rte_annotations dans Oxygen)
 - [Yannick] Logic functions
-- type system for generating C int/float when possible 
-  (generalisation of current Visit.principal_type, 
-  nouvelle unité de compilation Typing)
-- vérifier le code de la division et du modulo 
-  (div et modulo mathématiques différents des div et modulo de l'ANSI C99)
+- type system for generating C types whenever possible 
+  (generalisation of current Visit.principal_type)
 - customization des noms de variable générés 
   (par ex pour indiquer le nom de la variable d'origine, ou son rôle)
 
@@ -60,17 +35,8 @@
 # TESTS #
 #########
 
-- fonction sans code
-- tester plusieurs fonctions contenant des annotations
 - améliorer test "integer_constant.i" quand bug fixed #745
 - test sizeof.i devraient être plus précis quand logic_typing plus précis
 - structs
 - unions
 - inclure exemple du E-ACSL Reference Manual
-
-####################
-# AVANT LA DISTRIB #
-####################
-
-- user manual
-- make distrib

src/plugins/e-acsl/VERSION

+0.1

src/plugins/e-acsl/configure.ac

 ##########################################################################
 #                                                                        #
-#  This file is part of the E-ACSL plug-in of Frama-C.                   #
+#  This file is part of the Frama-C's E-ACSL plug-in.                    #
 #                                                                        #
-#  Copyright (C) 2011                                                    #
+#  Copyright (C) 2012                                                    #
 #    CEA (Commissariat  l'nergie atomique et aux nergies              #
 #         alternatives)                                                  #
 #                                                                        #
@@ -38,11 +38,36 @@ m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
 check_plugin(e_acsl,PLUGIN_RELATIVE_PATH(plugin_file),
 	     [support for E-ACSL plug-in],yes,yes)
 
+# Check Frama-C version
+#######################
+
+AC_MSG_CHECKING(for Frama-C version)
+
+FRAMAC_VERSION=`frama-c -version | sed -e 's/Version: \(.*\)/\1/' -e '2,$d' `
+AC_MSG_RESULT($FRAMAC_VERSION)
+
+DEV_VERSION_NUMBER=`echo $FRAMAC_VERSION | sed -e 's/.*-\(.*\)/\1/' `
+VERSION_NUMBER=`echo $DEV_VERSION_NUMBER | sed -e 's/\(.*\)+dev/\1/' `
+
+# at the time being, using the Frama-C development version is ok
+# DEV=`echo $DEV_VERSION_NUMBER | sed -e 's/.*\(+dev\)/\1/' `
+
+if test $VERSION_NUMBER -lt 20111001; then
+  AC_MSG_ERROR(Frama-C version must be Nitrogen-20111001.)
+else if test $VERSION_NUMBER -gt 20111001; then
+  AC_MSG_WARN(Frama-C version higher than Nitrogen-20111001 not tested: use it at your own risk.)
+fi
+fi
+
+# OCaml version
+###############
+
+OCAMLVERSION=`ocamlc -v | sed -n -e 's|.*version *\(.*\)$|\1|p' `
+
 ###############################
 # C specific stuff for E-ACSL #
 ###############################
 
-MAY_USE_ASSERT=true
 MAY_RUN_TESTS=yes
 
 # C compiler and stdio.h
@@ -62,17 +87,6 @@ if test -z $HAVE_STDIO_H; then
   AC_MSG_WARN([stdio.h missing: non-regression tests unavailable.])
 fi
 
-# assert.h
-##########
-
-AC_CHECK_HEADER(assert.h,HAVE_ASSERT_H=yes,)
-
-if test -z $HAVE_ASSERT_H; then
-  MAY_USE_ASSERT=false
-  MAY_RUN_TESTS=no
-  AC_MSG_WARN([assert.h missing: cannot use E-ACSL option -e-acsl-use-assert.])
-fi
-
 # GMP library
 #############
 
@@ -89,9 +103,7 @@ fi # testing $CC
 # Generating Makefile #
 #######################
 
-AC_SUBST(MAY_COMPILE_WITH_CC)
-AC_SUBST(MAY_USE_ASSERT)
 AC_SUBST(MAY_RUN_TESTS)
-AC_SUBST(GMPSRC_DIR)
+AC_SUBST(OCAMLVERSION)
 
 write_plugin_config(Makefile)

src/plugins/e-acsl/env.ml

 (**************************************************************************)
 (*                                                                        *)
-(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
 (*                                                                        *)
-(*  Copyright (C) 2011                                                    *)
+(*  Copyright (C) 2012                                                    *)
 (*    CEA (Commissariat  l'nergie atomique et aux nergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -44,6 +44,7 @@ type local_env = { block_info: block_info; mpz_tbl: mpz_tbl }
 
 type t = 
     { visitor: Visitor.frama_c_visitor; 
+      annotation_kind: Misc.annotation_kind;
       new_global_vars: varinfo list; (* generated variables at function level *)
       global_mpz_tbl: mpz_tbl;
       env_stack: local_env list;
@@ -64,6 +65,7 @@ let dummy =
       new Visitor.generic_frama_c_visitor 
 	Project_skeleton.dummy
 	(inplace_visit ()); 
+    annotation_kind = Misc.Assertion;
     new_global_vars = [];
     global_mpz_tbl = empty_mpz_tbl; 
     env_stack = []; 
@@ -72,6 +74,7 @@ let dummy =
 
 let empty v = 
   { visitor = v; 
+    annotation_kind = Misc.Assertion;
     new_global_vars = [];
     global_mpz_tbl = empty_mpz_tbl; 
     env_stack = []; 
@@ -291,6 +294,9 @@ let stmt_of_label env = function
      with Kernel_function.No_Statement -> assert false)
   | LogicLabel(_, _label) -> assert false
 
+let annotation_kind env = env.annotation_kind
+let set_annotation_kind env k = { env with annotation_kind = k }
+
 (*
 Local Variables:
 compile-command: "make"

src/plugins/e-acsl/env.mli

 (**************************************************************************)
 (*                                                                        *)
-(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
 (*                                                                        *)
-(*  Copyright (C) 2011                                                    *)
+(*  Copyright (C) 2012                                                    *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -93,6 +93,13 @@ val get_visitor: t -> Visitor.generic_frama_c_visitor
 
 val stmt_of_label: t -> logic_label -> stmt
 
+(* ************************************************************************** *)
+(** {2 Current annotation kind} *)
+(* ************************************************************************** *)
+
+val annotation_kind: t -> Misc.annotation_kind
+val set_annotation_kind: t -> Misc.annotation_kind -> t
+
 (*
 Local Variables:
 compile-command: "make"

src/plugins/e-acsl/error.ml

 (**************************************************************************)
 (*                                                                        *)
-(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
 (*                                                                        *)
-(*  Copyright (C) 2011                                                    *)
+(*  Copyright (C) 2012                                                    *)
 (*    CEA (Commissariat  l'nergie atomique et aux nergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)

src/plugins/e-acsl/error.mli

 (**************************************************************************)
 (*                                                                        *)
-(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
 (*                                                                        *)
-(*  Copyright (C) 2011                                                    *)
+(*  Copyright (C) 2012                                                    *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -23,13 +23,14 @@
 (** Handling errors. *)
 
 val untypable: string -> 'a
-(** type error built from the given argument. *)
+(** Type error built from the given argument. *)
   
 val not_yet: string -> 'a
-(** not_yet_implemented error built from the given argument. *)
+(** Not_yet_implemented error built from the given argument. *)
   
 val handle: ('a -> 'a) -> 'a -> 'a
-(** run the closure with the given argument and handle potential errors. *)
+(** Run the closure with the given argument and handle potential errors. 
+    Return the provide argument in case of errors. *)
 
 val nb_untypable: unit -> int
 (** Number of untypable annotations. *)

src/plugins/e-acsl/license/CEA_LGPL

 
-This file is part of the E-ACSL plug-in of Frama-C.
+This file is part of the Frama-C's E-ACSL plug-in.
 
-Copyright (C) 2011
+Copyright (C) 2012
   CEA (Commissariat à l'énergie atomique et aux énergies
        alternatives)
 

src/plugins/e-acsl/local_config.mli

 (**************************************************************************)
 (*                                                                        *)
-(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
 (*                                                                        *)
-(*  Copyright (C) 2011                                                    *)
+(*  Copyright (C) 2012                                                    *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -20,7 +20,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-val may_use_assert: bool
+val version: string
 
 (*
 Local Variables:

src/plugins/e-acsl/main.ml

 (**************************************************************************)
 (*                                                                        *)
-(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
 (*                                                                        *)
-(*  Copyright (C) 2011                                                    *)
+(*  Copyright (C) 2012                                                    *)
 (*    CEA (Commissariat  l'nergie atomique et aux nergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -51,7 +51,7 @@ module Resulting_projects =
       let name = "E-ACSL resulting projects"
       let size = 7
       let kind = `Correctness
-      let dependencies = [ Ast.self; Options.Use_assert.self ]
+      let dependencies = [ Ast.self ]
      end)
 
 let () = Env.global_state := Resulting_projects.self

src/plugins/e-acsl/misc.ml

 (**************************************************************************)
 (*                                                                        *)
-(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
 (*                                                                        *)
-(*  Copyright (C) 2011                                                    *)
+(*  Copyright (C) 2012                                                    *)
 (*    CEA (Commissariat  l'nergie atomique et aux nergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -40,16 +40,30 @@ let mk_call ?(loc=Location.unknown) ?result fname args =
   let f = new_lval ~loc (makeGlobalVar fname ty) in
   mkStmt ~valid_sid:true (Instr(Call(result, f, args, loc)))
 
+type annotation_kind = Assertion | Precondition | Postcondition | Invariant
+
+let kind_to_string loc k = 
+  mkString 
+    ~loc
+    (match k with
+    | Assertion -> "Assertion"
+    | Precondition -> "Precondition"
+    | Postcondition -> "Postcondition"
+    | Invariant -> "Invariant")
+
 (* Build a C conditional doing a runtime assertion check. *)
-let mk_e_acsl_guard ?(reverse=false) e p =
+let mk_e_acsl_guard ?(reverse=false) kind e p =
   let loc = p.loc in
-  let unicode = Kernel.Unicode.get () in
-  Kernel.Unicode.off ();
-  let msg = Pretty_utils.sfprintf "%a@?" Cil.d_predicate_named p in
-  Kernel.Unicode.set unicode;
-  let s = mk_call ~loc "e_acsl_fail" [ mkString loc msg ] in
+  let msg = 
+    Kernel.Unicode.without_unicode
+      (Pretty_utils.sfprintf "%a@?" Cil.d_predicate_named) p 
+  in
+  let line = (fst loc).Lexing.pos_lnum in
   let e = if reverse then new_exp ~loc:e.eloc (UnOp(LNot, e, intType)) else e in
-  mkStmt ~valid_sid:true (If(e, mkBlock [ s ], mkBlock [], loc))
+  mk_call 
+    ~loc 
+    "e_acsl_assert" 
+    [ e; kind_to_string loc kind; mkString loc msg; Cil.integer loc line ] 
 
 (*
 Local Variables:

src/plugins/e-acsl/misc.mli

 (**************************************************************************)
 (*                                                                        *)
-(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
 (*                                                                        *)
-(*  Copyright (C) 2011                                                    *)
+(*  Copyright (C) 2012                                                    *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -34,7 +34,11 @@ val new_lval: ?loc:Location.t -> varinfo -> exp
 
 val mk_call: ?loc:Location.t -> ?result:lval -> string -> exp list -> stmt
 
-val mk_e_acsl_guard: ?reverse:bool -> exp -> predicate named -> stmt
+type annotation_kind = Assertion | Precondition | Postcondition | Invariant
+
+val mk_e_acsl_guard: 
+  ?reverse:bool -> annotation_kind -> exp -> predicate named -> stmt
+
 val e_acsl_header: unit -> global
 
 (*

src/plugins/e-acsl/mpz.ml

 (**************************************************************************)
 (*                                                                        *)
-(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
 (*                                                                        *)
-(*  Copyright (C) 2011                                                    *)
+(*  Copyright (C) 2012                                                    *)
 (*    CEA (Commissariat  l'nergie atomique et aux nergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)

src/plugins/e-acsl/mpz.mli

 (**************************************************************************)
 (*                                                                        *)
-(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
 (*                                                                        *)
-(*  Copyright (C) 2011                                                    *)
+(*  Copyright (C) 2012                                                    *)
 (*    CEA (Commissariat  l'nergie atomique et aux nergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)

src/plugins/e-acsl/options.ml

 (**************************************************************************)
 (*                                                                        *)
-(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
 (*                                                                        *)
-(*  Copyright (C) 2011                                                    *)
+(*  Copyright (C) 2012                                                    *)
 (*    CEA (Commissariat  l'nergie atomique et aux nergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -58,15 +58,27 @@ module Project_name =
       let arg_name = "prj"
      end)
 
-module Use_assert =
+let () = Plugin.set_group help
+module Version =
   False
     (struct
-      let option_name = "-e-acsl-use-assert"
-      let help = "use C macro `assert' instead of `exit' in the new project \
-(by default, use it whenever possible)"
-      let kind = `Correctness
+      let option_name = "-e-acsl-version"
+      let help = "version of plug-in E-ACSL"
+      let kind = `Tuning
      end)
 
+let version () =
+  if Version.get () then begin
+    Log.print_on_output 
+      (fun fmt -> 
+	Format.fprintf 
+	  fmt
+	  "Version of plug-in E-ACSL: %s@?"
+	  Local_config.version);
+    raise Cmdline.Exit
+  end
+let () = Cmdline.run_after_configuring_stage version
+
 (*
 Local Variables:
 compile-command: "make"

src/plugins/e-acsl/options.mli

 (**************************************************************************)
 (*                                                                        *)
-(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
 (*                                                                        *)
-(*  Copyright (C) 2011                                                    *)
+(*  Copyright (C) 2012                                                    *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -28,8 +28,6 @@ module Check: Bool
 module Run: Bool
 module Project_name: String
 
-module Use_assert: Bool
-
 (*
 Local Variables:
 compile-command: "make"