[e-acsl] remove option -e-acsl-include-headers

[e-acsl] tests now independent of GMP version (but GMP still required)

src/plugins/e-acsl/Makefile.in

@@ -55,7 +55,6 @@ $(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_compile_with_cc = @MAY_COMPILE_WITH_CC@" >> $@
 	$(ECHO) "let may_use_assert = @MAY_USE_ASSERT@" >> $@
 	$(CHMOD_RO) $@
 

src/plugins/e-acsl/TODO

@@ -18,8 +18,23 @@
 - minimiser le nombre de variables générées
 - constante entière longue: utiliser la représentation sous forme de string et 
   rechercher la base appropriée.
-- introduire feature wishes Bernard (voir mail du 9 juin)
 - 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:
+  if (assume_bhv) {
+    e_acsl_trace_behavior(bhv_name);
+    requires_bhv;
+    run_function;
+    ensures_bhv;
+  }
 
 ##############
 # KNOWN BUGS #
@@ -32,7 +47,6 @@
 #########
 
 - fonction sans code
-- ajouter -Wall -pedantic -c99
 - exécuter rte
 - tester plusieurs fonctions contenant des annotations
 - améliorer test "integer_constant.i" quand bug fixed #745

src/plugins/e-acsl/configure.ac

@@ -41,7 +41,6 @@ check_plugin(e_acsl,PLUGIN_RELATIVE_PATH(plugin_file),
 # C specific stuff for E-ACSL #
 ###############################
 
-MAY_COMPILE_WITH_CC=true
 MAY_USE_ASSERT=true
 MAY_RUN_TESTS=yes
 
@@ -58,9 +57,7 @@ if test -z $CC; then
 else
 
 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-include-headers.])
   AC_MSG_WARN([stdio.h missing: non-regression tests unavailable.])
 fi
 
@@ -73,7 +70,6 @@ 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.])
-  AC_MSG_WARN([assert.h missing: non-regression tests unavailable.])
 fi
 
 # GMP library
@@ -82,9 +78,7 @@ fi
 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-include-headers.])
   AC_MSG_WARN([GMP library missing: non-regression tests unavailable.])
 fi
 

src/plugins/e-acsl/local_config.mli

@@ -19,7 +19,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-val may_compile_with_cc: bool
 val may_use_assert: bool
 
 (*

src/plugins/e-acsl/main.ml

@@ -55,8 +55,7 @@ module Resulting_projects =
       let name = "E-ACSL resulting projects"
       let size = 7
       let kind = `Correctness
-      let dependencies =
-	[ Ast.self; Options.Include_headers.self; Options.Use_assert.self ]
+      let dependencies = [ Ast.self; Options.Use_assert.self ]
      end)
 
 let () = Env.global_state := Resulting_projects.self
@@ -66,20 +65,7 @@ let generate_code =
     (fun name ->
       try
 	let visit prj = Visit.do_visit ~prj true in
-	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
+	File.create_rebuilt_project_from_visitor ~preprocess:false name visit
       with Misc.Typing_error s ->
 	Options.abort ~current:true "%s" s)
 

src/plugins/e-acsl/mpz.ml

@@ -34,14 +34,14 @@ let is_now_referenced () = t_torig.treferenced <- true
 let t = TNamed(t_torig, [])
 let is_t ty = Cil_datatype.Typ.equal ty t
 
-let apply_on_var funname e = Misc.mk_call ("mpz_" ^ funname) [ e ]
+let apply_on_var funname e = Misc.mk_call ("__gmpz_" ^ funname) [ e ]
 let init = apply_on_var "init"
 let clear = apply_on_var "clear"
 
 let init_set v e =
   let ty = typeOf e in
   if is_t ty then
-    Misc.mk_call "mpz_init_set" [ v; e ]
+    Misc.mk_call "__gmpz_init_set" [ v; e ]
   else
     let fname, args = match ty with
       | TInt((IBool | IChar | IUChar | IUInt | IUShort | IULong), _) ->
@@ -54,7 +54,7 @@ let init_set v e =
 	[ e; integer ~loc:Location.unknown 10 ]
       | _ -> assert false
     in
-    Misc.mk_call ("mpz_init_set_" ^ fname) (v :: args)
+    Misc.mk_call ("__gmpz_init_set_" ^ fname) (v :: args)
 
 (*
 Local Variables:

src/plugins/e-acsl/options.ml

@@ -46,15 +46,6 @@ module Project_name =
       let arg_name = "prj"
      end)
 
-module Include_headers =
-  False
-    (struct
-      let option_name = "-e-acsl-include-headers"
-      let help = "include standard headers in the new project \
-(unset by default)"
-      let kind = `Correctness
-     end)
-
 module Use_assert =
   False
     (struct

src/plugins/e-acsl/options.mli

@@ -26,7 +26,6 @@ include S (** implementation of Log.S for E-ACSL *)
 module Check: Bool
 module Project_name: String
 
-module Include_headers: Bool
 module Use_assert: Bool
 
 (*

src/plugins/e-acsl/read_header.ml

@@ -46,12 +46,7 @@ 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_types.h" buf;
       put_file_in_buffer "e_acsl_gmp.h" buf;
       put_file_in_buffer "e_acsl.h" buf
     end;

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

@@ -7,83 +7,83 @@
 
 /*@ ensures \valid(x);
   @ assigns *x; */
-extern void mpz_init(mpz_t x);
+extern void __gmpz_init(mpz_t x);
 
 /*@ ensures \valid(z);
   @ assigns *z; */
-extern void mpz_init_set(mpz_t z, const mpz_t z_orig);
+extern void __gmpz_init_set(mpz_t z, const mpz_t z_orig);
 
 /*@ ensures \valid(z);
   @ assigns *z \from n; */
-extern void mpz_init_set_ui(mpz_t z, unsigned long int n);
+extern void __gmpz_init_set_ui(mpz_t z, unsigned long int n);
 
 /*@ ensures \valid(z);
   @ assigns *z \from n; */
-extern void mpz_init_set_si(mpz_t z, signed long int n);
+extern void __gmpz_init_set_si(mpz_t z, signed long int n);
 
 /*@ ensures \valid(z);
   @ assigns *z; */
-extern int mpz_init_set_str(mpz_t z, const char *str, int base);
+extern int __gmpz_init_set_str(mpz_t z, const char *str, int base);
 
 // finalizer
 
 /*@ requires \valid(x);
   @ assigns *x; */
-extern void mpz_clear(mpz_t x);
+extern void __gmpz_clear(mpz_t x);
 
 // logical and arithmetic operators
 
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ assigns \nothing; */
-extern int mpz_cmp(const mpz_t z1, const mpz_t z2);
+extern int __gmpz_cmp(const mpz_t z1, const mpz_t z2);
 
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ assigns *z1; */
-extern int mpz_comp(mpz_t z1, const mpz_t z2);
+extern int __gmpz_comp(mpz_t z1, const mpz_t z2);
 
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ assigns *z1; */
-extern void mpz_neg(mpz_t z1, const mpz_t z2);
+extern void __gmpz_neg(mpz_t z1, const mpz_t z2);
 
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ requires \valid(z3);
   @ assigns *z1; */
-extern void mpz_add(mpz_t z1, const mpz_t z2, const mpz_t z3);
+extern void __gmpz_add(mpz_t z1, const mpz_t z2, const mpz_t z3);
 
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ requires \valid(z3);
   @ assigns *z1; */
-extern void mpz_sub(mpz_t z1, const mpz_t z2, const mpz_t z3);
+extern void __gmpz_sub(mpz_t z1, const mpz_t z2, const mpz_t z3);
 
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ requires \valid(z3);
   @ assigns *z1; */
-extern void mpz_mul(mpz_t z1, const mpz_t z2, const mpz_t z3);
+extern void __gmpz_mul(mpz_t z1, const mpz_t z2, const mpz_t z3);
 
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ requires \valid(z3);
   @ assigns *z1; */
-extern void mpz_tdiv_q(mpz_t z1, const mpz_t z2, const mpz_t z3);
+extern void __gmpz_tdiv_q(mpz_t z1, const mpz_t z2, const mpz_t z3);
 
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ requires \valid(z3);
   @ assigns *z1; */
-extern void mpz_tdiv_r(mpz_t z1, const mpz_t z2, const mpz_t z3);
+extern void __gmpz_tdiv_r(mpz_t z1, const mpz_t z2, const mpz_t z3);
 
 // coercions to C int
 
 /*@ requires \valid(z); 
   @ assigns \nothing; */
-extern long mpz_get_si(const mpz_t z);
+extern long __gmpz_get_si(const mpz_t z);
 
 /*@ requires \valid(z); 
   @ assigns \nothing; */
-extern unsigned long mpz_get_ui(const mpz_t z);
+extern unsigned long __gmpz_get_ui(const mpz_t z);

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

 /* run.config
    COMMENT: addrOf
-   EXECNOW: LOG gen_addrOf.c BIN gen_addrOf.out FRAMAC_SHARE=./share @frama-c@ ./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 && ./tests/e-acsl-runtime/result/gen_addrOf.out
+   EXECNOW: LOG gen_addrOf.c BIN gen_addrOf.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/addrOf.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_addrOf.out ./tests/e-acsl-runtime/result/gen_addrOf.c && ./tests/e-acsl-runtime/result/gen_addrOf.out
 */
 int main(void) {
   int x = 0;

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

 /* run.config
    COMMENT: arithmetic operations
    COMMENT: add the last assertion when fixing BTS #751
-   EXECNOW: LOG gen_arith.c BIN gen_arith.out FRAMAC_SHARE=./share @frama-c@ ./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 ./tests/e-acsl-runtime/result/gen_arith.c -lgmp && ./tests/e-acsl-runtime/result/gen_arith.out
+   EXECNOW: LOG gen_arith.c BIN gen_arith.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/arith.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_arith.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_arith.out ./tests/e-acsl-runtime/result/gen_arith.c -lgmp && ./tests/e-acsl-runtime/result/gen_arith.out
 */
 
 int main(void) {

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

 /* run.config
    COMMENT: arrays
-   EXECNOW: LOG gen_array.c BIN gen_array.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/array.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_array.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_array.out ./tests/e-acsl-runtime/result/gen_array.c -lgmp && ./tests/e-acsl-runtime/result/gen_array.out
+   EXECNOW: LOG gen_array.c BIN gen_array.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/array.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_array.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_array.out ./tests/e-acsl-runtime/result/gen_array.c -lgmp && ./tests/e-acsl-runtime/result/gen_array.out
 */
 
 int T1[3],T2[4];

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

 /* run.config
    COMMENT: \at
-   EXECNOW: LOG gen_at.c BIN gen_at.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/at.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_at.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_at.out ./tests/e-acsl-runtime/result/gen_at.c -lgmp && ./tests/e-acsl-runtime/result/gen_at.out
+   EXECNOW: LOG gen_at.c BIN gen_at.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/at.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_at.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_at.out ./tests/e-acsl-runtime/result/gen_at.c -lgmp && ./tests/e-acsl-runtime/result/gen_at.out
 */
 
 int A = 0;

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

 /* run.config
    COMMENT: cast
-   EXECNOW: LOG gen_cast.c BIN gen_cast.out FRAMAC_SHARE=./share @frama-c@ ./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 -lgmp && ./tests/e-acsl-runtime/result/gen_cast.out
+   EXECNOW: LOG gen_cast.c BIN gen_cast.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/cast.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_cast.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_cast.out ./tests/e-acsl-runtime/result/gen_cast.c -lgmp && ./tests/e-acsl-runtime/result/gen_cast.out
 */
 
 int main(void) {

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

 /* run.config
    COMMENT: comparison operators
-   EXECNOW: LOG gen_comparison.c BIN gen_comparison.out FRAMAC_SHARE=./share @frama-c@ ./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 ./tests/e-acsl-runtime/result/gen_comparison.c -lgmp && ./tests/e-acsl-runtime/result/gen_comparison.out
+   EXECNOW: LOG gen_comparison.c BIN gen_comparison.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/comparison.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_comparison.c > /dev/null &&  gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_comparison.out ./tests/e-acsl-runtime/result/gen_comparison.c -lgmp && ./tests/e-acsl-runtime/result/gen_comparison.out
 */
 
 int main(void) {

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

 /* run.config
    COMMENT: assert \false
-   EXECNOW: LOG gen_false.c BIN gen_false.out FRAMAC_SHARE=./share @frama-c@ ./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 && ./tests/e-acsl-runtime/result/gen_false.out
+   EXECNOW: LOG gen_false.c BIN gen_false.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/false.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_false.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_false.out ./tests/e-acsl-runtime/result/gen_false.c && ./tests/e-acsl-runtime/result/gen_false.out
 */
 int main(void) {
   int x = 0;

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

 /* run.config
    COMMENT: function contract
-   EXECNOW: LOG gen_function_contract.c BIN gen_function_contract.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/function_contract.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_function_contract.out ./tests/e-acsl-runtime/result/gen_function_contract.c -lgmp && ./tests/e-acsl-runtime/result/gen_function_contract.out
+   EXECNOW: LOG gen_function_contract.c BIN gen_function_contract.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/function_contract.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_function_contract.out ./tests/e-acsl-runtime/result/gen_function_contract.c -lgmp && ./tests/e-acsl-runtime/result/gen_function_contract.out
 */
 
 int X = 0, Y = 2;

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

 /* run.config
    COMMENT: integer constant + a stmt after the assertion
    COMMENT: waiting for fixing BTS #745
-   EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out FRAMAC_SHARE=./share @frama-c@ ./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 ./tests/e-acsl-runtime/result/gen_integer_constant.c -lgmp && ./tests/e-acsl-runtime/result/gen_integer_constant.out
+   EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/integer_constant.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_integer_constant.out ./tests/e-acsl-runtime/result/gen_integer_constant.c -lgmp && ./tests/e-acsl-runtime/result/gen_integer_constant.out
 */
 int main(void) {
   int x;

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

 /* run.config
    COMMENT: predicate using lazy operators
-   EXECNOW: LOG gen_lazy.c BIN gen_lazy.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/lazy.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_lazy.c > /dev/null &&  gcc -o ./tests/e-acsl-runtime/result/gen_lazy.out ./tests/e-acsl-runtime/result/gen_lazy.c -lgmp 2> /dev/null && ./tests/e-acsl-runtime/result/gen_lazy.out
+   EXECNOW: LOG gen_lazy.c BIN gen_lazy.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/lazy.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_lazy.c > /dev/null &&  gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_lazy.out ./tests/e-acsl-runtime/result/gen_lazy.c -lgmp 2> /dev/null && ./tests/e-acsl-runtime/result/gen_lazy.out
 */
 
 int main(void) {