[e-acsl] implement options for direct linking with GMP

[e-acsl] Makefile's target 'install'
[e-acsl] test GMP linkage in non-regression suite ('make tests' now requires GMP >= 4.3.2)
[e-acsl] fixed bugs of GMP compatibility

src/plugins/e-acsl/Makefile.in

@@ -44,7 +44,6 @@ $(PLUGIN_DIR)/local_config.ml: $(PLUGIN_DIR)/Makefile.in
 	$(ECHO) "(* This file was automatically generated from $<. Don't edit it. *)" >> $@
 	$(ECHO) "let may_compile_with_cc = @MAY_COMPILE_WITH_CC@" >> $@
 	$(ECHO) "let may_use_assert = @MAY_USE_ASSERT@" >> $@
-	$(ECHO) "let gmpsrc_dir = \"@GMPSRC_DIR@\"" >> $@
 	$(CHMOD_RO) $@
 
 PLUGIN_GENERATED:= $(PLUGIN_DIR)/local_config.ml
@@ -67,6 +66,14 @@ tests:: tests/test_config
 
 endif
 
+###########
+# Install #
+###########
+
+install::
+	$(PRINT_CP) E-ACSL share files
+	$(CP) -R share/e-acsl $(FRAMAC_SHARE)
+
 ################
 # Generic part #
 ################

src/plugins/e-acsl/configure.ac

@@ -60,7 +60,7 @@ fi
 if test -z $HAVE_STDIO_H; then
   MAY_COMPILE_WITH_CC=false
   MAY_RUN_TESTS=no
-  AC_MSG_WARN([stdio.h missing: cannot use option -e-acsl-link-headers.])
+  AC_MSG_WARN([stdio.h missing: cannot use option -e-acsl-include-headers.])
   AC_MSG_WARN([stdio.h missing: non-regression tests unavailable.])
 fi
 
@@ -84,31 +84,10 @@ AC_CHECK_LIB(gmp,__gmpz_init,HAVE_GMP=yes,) # also set LIBS
 if test -z $HAVE_GMP; then
   MAY_COMPILE_WITH_CC=false
   MAY_RUN_TESTS=no
-  AC_MSG_WARN([GMP library missing: cannot use E-ACSL option -e-acsl-link-headers.])
+  AC_MSG_WARN([GMP library missing: cannot use E-ACSL option -e-acsl-include-headers.])
   AC_MSG_WARN([GMP library missing: non-regression tests unavailable.])
 fi
 
-# GMP sources
-#############
-
-GMPSRC_DIR=
-
-AC_ARG_WITH(gmp-src,
-  AC_HELP_STRING(
-    [--with-gmp-src],
-    [directory containing the source of the GMP library]
-    ))
-
-if test "$with_gmp_src" = "yes" -o "$with_gmp_src" = "no" -o "$with_gmp_src" = ""; \
-then
-  AC_MSG_WARN([GMP sources missing: cannot use E-ACSL option -e-acsl-link-gmpsrc. Set the directory containing these sources with --with-gmp-src=<dirname>. Sources are available from ftp://ftp.gmplib.org/pub/gmp-4.3.2/gmp-4.3.2.tar.bz2])
-else
-  GMPSRC_DIR=$with_gmp_src
-  AC_CHECK_FILE($GMPSRC_DIR/mpz/init.c,
-    AC_MSG_NOTICE([GMP sources got from $GMPSRC_DIR]),
-    AC_MSG_ERROR([Directory $GMPSRC_DIR does not contain GMP sources.]))
-fi
-
 #######################
 # Generating Makefile #
 #######################

src/plugins/e-acsl/local_config.mli

@@ -21,7 +21,6 @@
 
 val may_compile_with_cc: bool
 val may_use_assert: bool
-val gmpsrc_dir: string
 
 (*
 Local Variables:

src/plugins/e-acsl/main.ml

@@ -56,10 +56,7 @@ module Resulting_projects =
       let size = 7
       let kind = `Correctness
       let dependencies =
-	[ Ast.self;
-	  Options.H_link.self;
-	  Options.Gmpsrc_link.self;
-	  Options.Use_assert.self ]
+	[ Ast.self; Options.Include_headers.self; Options.Use_assert.self ]
      end)
 
 let generate_code =
@@ -67,7 +64,20 @@ let generate_code =
     (fun name ->
       try
 	let visit prj = Visit.do_visit ~prj true in
-	File.create_rebuilt_project_from_visitor name visit
+	let preprocess =
+	  if Options.Include_headers.get () then
+	    if Local_config.may_compile_with_cc then begin
+	      if Local_config.may_use_assert then Options.Use_assert.on ();
+	      true
+	    end else begin
+	      Options.warning "option `-e-acsl-include-headers' not available \
+(see configure warning) : ignoring it.";
+	      false
+	    end
+	  else
+	    false
+	in
+	File.create_rebuilt_project_from_visitor ~preprocess name visit
       with Visit.Typing_error s ->
 	Options.abort ~current:true "%s" s)
 

src/plugins/e-acsl/options.ml

@@ -46,24 +46,15 @@ module Project_name =
       let arg_name = "prj"
      end)
 
-module H_link =
+module Include_headers =
   False
     (struct
-      let option_name = "-e-acsl-link-headers"
+      let option_name = "-e-acsl-include-headers"
       let help = "include standard headers in the new project \
 (unset by default)"
       let kind = `Correctness
      end)
 
-module Gmpsrc_link =
-  False
-    (struct
-      let option_name = "-e-acsl-link-gmpsrc"
-      let help = "link against GMP source code in the new project \
-(unset by default)"
-      let kind = `Correctness
-     end)
-
 module Use_assert =
   False
     (struct

src/plugins/e-acsl/options.mli

@@ -26,8 +26,7 @@ include S (** implementation of Log.S for E-ACSL *)
 module Check: BOOL
 module Project_name: STRING
 
-module H_link: BOOL
-module Gmpsrc_link: BOOL
+module Include_headers: BOOL
 module Use_assert: BOOL
 
 (*

src/plugins/e-acsl/read_header.ml

@@ -19,13 +19,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-let text =
-  let buf = Buffer.create 97 in
-  fun () ->
-    if Buffer.length buf = 0 then begin
-      let fname = Filename.concat Config.datadir "e_acsl.h" in
+let put_file_in_buffer fname buf =
       try
-	let cin = open_in fname in
+	let cin =
+	  open_in
+	    (Filename.concat Config.datadir (Filename.concat "e-acsl" fname))
+	in
 	try
 	  while true do
 	    let l = input_line cin in
@@ -36,6 +35,25 @@ let text =
 	  close_in cin
       with Sys_error s ->
 	Options.abort "cannot read file `%s': %s" fname s
+
+(* TODO: must be project-compliant. The memoized buffer should be reset when we
+   have to redo the visitor in a different setting. *)
+
+let add_include buf hfile =
+  Buffer.add_string buf (Format.sprintf "#include %S\n" hfile)
+
+let text =
+  let buf = Buffer.create 97 in
+  fun () ->
+    if Buffer.length buf = 0 then begin
+      if Options.Include_headers.get () then begin
+	add_include buf "stdio.h";
+	if Options.Use_assert.get () then add_include buf "assert.h";
+	add_include buf "gmp.h";
+      end else
+	put_file_in_buffer "e_acsl_gmp_types.h" buf;
+      put_file_in_buffer "e_acsl_gmp.h" buf;
+      put_file_in_buffer "e_acsl.h" buf
     end;
     Buffer.contents buf
 

src/plugins/e-acsl/share/e-acsl/e_acsl.h

+// TODO: remplacer par un e_acsl.h.in
+// faire gnrer par le makefile un e_acsl.h
+// avec des #include "FRAMAC_SHARE/libc/stdio.h", etc
+
+// [TODO] ne pas gnrer les typedef si on veut linker avec GMP derrire
+
+// [TODO] utiliser un champ modle de type integer pour modliser
+// l'entier exact correspondant  un mpz_t.
+// Not yet implemented in ACSL.
+
+/************************/
+/* Standard C functions */
+/************************/
+
+/*@ terminates \false;
+  @ assigns \nothing;
+  @ ensures \false; */
+extern void exit(int status);
+
+/*@ assigns \nothing; */
+extern int printf(const char *, ...);
+
+/*****************************/
+/* Dedicated E-ACSL function */
+/*****************************/
+
+void e_acsl_fail(char *msg) { printf("%s\n", msg); exit(1); }

src/plugins/e-acsl/share/e_acsl.h → src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h

-// TODO: remplacer par un e_acsl.h.in
-// faire gnrer par le makefile un e_acsl.h
-// avec des #include "FRAMAC_SHARE/libc/stdio.h", etc
-
-/*************/
-/* GMP types */
-/*************/
-
-// [TODO] ne pas gnrer les typedef si on veut linker avec GMP derrire
-
-// [TODO] utiliser un champ modle de type integer pour modliser
-// l'entier exact correspondant  un mpz_t.
-// Not yet implemented in ACSL.
-
-typedef struct {
-  int _mp_alloc;
-  int _mp_size;
-  unsigned long int *_mp_d;
-} __mpz_struct;
-
-typedef __mpz_struct mpz_t[1];
 
 /*****************/
 /* GMP functions */
@@ -40,7 +19,7 @@ extern void mpz_init_set_si(mpz_t z, signed long int n);
 
 /*@ ensures \valid(z);
   @ assigns *z; */
-extern void mpz_init_set_str(mpz_t z, const char *str, int base);
+extern int mpz_init_set_str(mpz_t z, const char *str, int base);
 
 // finalizer
 
@@ -63,52 +42,34 @@ extern int mpz_comp(mpz_t z1, const mpz_t z2);
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ assigns *z1; */
-extern int mpz_neg(mpz_t z1, const mpz_t z2);
+extern void mpz_neg(mpz_t z1, const mpz_t z2);
 
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ requires \valid(z3);
   @ assigns *z1; */
-extern int mpz_add(mpz_t z1, const mpz_t z2, const mpz_t z3);
+extern void mpz_add(mpz_t z1, const mpz_t z2, const mpz_t z3);
 
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ requires \valid(z3);
   @ assigns *z1; */
-extern int mpz_sub(mpz_t z1, const mpz_t z2, const mpz_t z3);
+extern void mpz_sub(mpz_t z1, const mpz_t z2, const mpz_t z3);
 
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ requires \valid(z3);
   @ assigns *z1; */
-extern int mpz_mul(mpz_t z1, const mpz_t z2, const mpz_t z3);
+extern void mpz_mul(mpz_t z1, const mpz_t z2, const mpz_t z3);
 
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ requires \valid(z3);
   @ assigns *z1; */
-extern int mpz_cdiv_q(mpz_t z1, const mpz_t z2, const mpz_t z3);
+extern void mpz_cdiv_q(mpz_t z1, const mpz_t z2, const mpz_t z3);
 
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ requires \valid(z3);
   @ assigns *z1; */
-extern int mpz_mod(mpz_t z1, const mpz_t z2, const mpz_t z3);
-
-/************************/
-/* Standard C functions */
-/************************/
-
-/*@ terminates \false;
-  @ assigns \nothing;
-  @ ensures \false; */
-extern void exit(int status);
-
-/*@ assigns \nothing; */
-extern int printf(const char *, ...);
-
-/*****************************/
-/* Dedicated E-ACSL function */
-/*****************************/
-
-void e_acsl_fail(char *msg) { printf(msg); exit(1); }
+extern void mpz_mod(mpz_t z1, const mpz_t z2, const mpz_t z3);

src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_types.h

+
+/*************/
+/* GMP types */
+/*************/
+
+typedef struct {
+  int _mp_alloc;
+  int _mp_size;
+  unsigned long int *_mp_d;
+} __mpz_struct;
+
+typedef __mpz_struct mpz_t[1];

src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i

 /* run.config
-   COMMENT: addrOf */
+   COMMENT: addrOf
+   EXECNOW: LOG gen_addrOf.c BIN gen_addrOf.out FRAMAC_SHARE=./share frama-c -load-module E_ACSL ./tests/e-acsl-runtime/addrOf.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_addrOf.out ./tests/e-acsl-runtime/result/gen_addrOf.c
+*/
 void main() {
   int x = 0;
   /*@ assert &x == &x; */ ;

src/plugins/e-acsl/tests/e-acsl-runtime/arith.i

 /* run.config
    COMMENT: arithmetic operations
-   COMMENT: add the last assertion when fixing BTS #751 */
+   COMMENT: add the last assertion when fixing BTS #751
+   EXECNOW: LOG gen_arith.c BIN gen_arith.out FRAMAC_SHARE=./share frama-c -load-module E_ACSL ./tests/e-acsl-runtime/arith.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_arith.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_arith.out -lgmp ./tests/e-acsl-runtime/result/gen_arith.c
+*/
 
 void main() {
   int x = -3;

src/plugins/e-acsl/tests/e-acsl-runtime/cast.i

 /* run.config
-   COMMENT: cast */
+   COMMENT: cast
+   EXECNOW: LOG gen_cast.c BIN gen_cast.out FRAMAC_SHARE=./share frama-c -load-module E_ACSL ./tests/e-acsl-runtime/cast.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_cast.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_cast.out ./tests/e-acsl-runtime/result/gen_cast.c
+*/
 
 void main() {
   long x = 0;

src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i

 /* run.config
-   COMMENT: comparison operators */
+   COMMENT: comparison operators
+   EXECNOW: LOG gen_comparison.c BIN gen_comparison.out FRAMAC_SHARE=./share frama-c -load-module E_ACSL ./tests/e-acsl-runtime/comparison.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_comparison.c > /dev/null &&  gcc -o ./tests/e-acsl-runtime/result/gen_comparison.out -lgmp ./tests/e-acsl-runtime/result/gen_comparison.c
+*/
 
 void main() {
   int x = 0, y = 1;

src/plugins/e-acsl/tests/e-acsl-runtime/empty.i

 /* run.config
    COMMENT: empty file
-   OPT: -e-acsl-project p -then-on p -print */
+   OPT: -e-acsl-check -e-acsl-project p -then-on p -print */

src/plugins/e-acsl/tests/e-acsl-runtime/false.i

 /* run.config
-   COMMENT: assert \false */
+   COMMENT: assert \false
+   EXECNOW: LOG gen_false.c BIN gen_false.out FRAMAC_SHARE=./share frama-c -load-module E_ACSL ./tests/e-acsl-runtime/false.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_false.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_false.out ./tests/e-acsl-runtime/result/gen_false.c
+*/
 void main() {
   int x = 0;
   if (x) /*@ assert \false; */ ;

src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i

 /* run.config
    COMMENT: integer constant
-   COMMENT: waiting for fixing BTS #745 */
+   COMMENT: waiting for fixing BTS #745
+   EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out FRAMAC_SHARE=./share frama-c -load-module E_ACSL ./tests/e-acsl-runtime/integer_constant.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_integer_constant.out -lgmp ./tests/e-acsl-runtime/result/gen_integer_constant.c
+*/
 void main() {
   /*@ assert 0 == 0; */
   /*@ assert 0 != 1; */

src/plugins/e-acsl/tests/e-acsl-runtime/not.i

 /* run.config
-   COMMENT: predicate [!p] */
+   COMMENT: predicate [!p]
+   EXECNOW: LOG gen_not.c BIN gen_not.out FRAMAC_SHARE=./share frama-c -load-module E_ACSL ./tests/e-acsl-runtime/not.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_not.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_not.out ./tests/e-acsl-runtime/result/gen_not.c
+*/
 void main() {
   int x = 0;
   /*@ assert ! x; */

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle

@@ -2,7 +2,7 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-PROJECT_FILE:121:[value] Assertion got status valid.
+PROJECT_FILE.i:121:[value] Assertion got status valid.
 [value] Recording results for main
 [value] done for function main
 [dominators] computing for function main
@@ -19,7 +19,7 @@ extern void exit(int status ) ;
 extern int printf(char const   *  , ...) ;
 void e_acsl_fail(char *msg ) 
 {
-  printf((char const   *)msg);
+  printf("%s\n",msg);
   exit(1);
   return;
 }