[e-acsl] little refactoring

src/plugins/e-acsl/TODO

-- utiliser Options.use_asserts
+########
+# CODE #
+########
 
+- utiliser Options.use_asserts
 - gestion des initialiseurs des globals: requiert un main
-
-- ajouter des gardes dans les specs devant les termes indéfinis
-
-/*@ assert \forall integer x; -1<= x<= 1 ==>  1/x == 0 || 1/x != 0; */
-
-the plug-in would generate something like
-
-/*@ assert \forall integer x; -1<= x<= 1 ==>  (x != 0&&  1/x == 0) || (x != 0
-&&  1/x != 0); */ 
-
 - 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)
-
-- tester les opérations binaires sur les pointeurs (requiert complex left value)
-
 - 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.
 
+#########
+# TESTS #
+#########
+
+- tester les opérations binaires sur les pointeurs (requiert complex left value)
 - améliorer test "integer_constant.i" quand bug fixed #745
 - améliorer test "arith.i" quand bug fixed #751
 
+####################
+# AVANT LA DISTRIB #
+####################
+
 en lien avec bts #743:
 - make distrib
 - headers (copyright 2011)

src/plugins/e-acsl/visit.ml

@@ -46,7 +46,7 @@ let not_yet s =
 let e_acsl_header () = GText (Read_header.text ())
 
 (* Build a C conditional doing a runtime assertion check. *)
-let mk_if e p =
+let mk_e_acsl_guard e p =
   let loc = p.loc in
   let unicode = Parameters.Unicode.get () in
   Parameters.Unicode.off ();
@@ -65,10 +65,10 @@ module Mpz : sig
   val is_t: typ -> bool (* is the type equal to "mpz_t"? *)
   val e_got_t: exp -> bool (* is the type of e is equal to "mpz_t"? *)
   val init: exp -> stmt (* build stmt "mpz_init(v)" *)
-  val clear: exp -> stmt (* build stmt "mpz_clear(v)" *)
   val init_set: exp -> exp -> stmt
 (* build stmt "mpz_init_set_*(v, e)" with the good function 'set' according to
    the type of e *)
+  val clear: exp -> stmt (* build stmt "mpz_clear(v)" *)
 end = struct
 
   let t_torig =
@@ -237,7 +237,9 @@ let constant_to_exp ?(loc=Location.unknown) = function
     kinteger64_repr ?loc k n s
   | CInt64(n, (ILongLong | IULongLong), _s) -> 
     (* cannot use the string [s] if any since we do not know the base in which
-       it is written. Such a base is required by GMP. *)
+       it is written. Such a base is required by GMP.
+       [TODO] Actually possible to find the base for the string, but not done
+       yet *)
     mkString ?loc (Int64.to_string n)
   | CStr _ | CWStr _ | CChr _ | CReal _ | CEnum _ as c -> 
     new_exp ?loc (Const c)
@@ -321,7 +323,7 @@ let rec term_to_exp env t =
       let call = mk_call ~loc name [ e; e1; e2 ]  in
       match bop with
       | Div | Mod ->
-	let cond = mk_if guard (Logic_const.prel (Req, t2, zero)) in
+	let cond = mk_e_acsl_guard guard (Logic_const.prel (Req, t2, zero)) in
 	Env.add_assert cond (Logic_const.prel (Rneq, t2, zero));
 	[ cond; call ]
       | _ ->
@@ -465,7 +467,9 @@ let rec named_predicate_to_exp env p =
 let convert_named_predicate env p =
   let e, env = named_predicate_to_exp env p in
   assert (Typ.equal (typeOf e) intType);
-  Env.add_stmt env (mk_if (new_exp ~loc:e.eloc (UnOp(LNot, e, intType))) p)
+  Env.add_stmt
+    env
+    (mk_e_acsl_guard (new_exp ~loc:e.eloc (UnOp(LNot, e, intType))) p)
 
 let convert_annotation env annot =
   try