From 80b25403fca75c095076ce57884a90f1a486f427 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 12 May 2011 14:48:12 +0000
Subject: [PATCH] [e-acsl] little refactoring
---
src/plugins/e-acsl/TODO | 30 +++++++++++++++---------------
src/plugins/e-acsl/visit.ml | 14 +++++++++-----
2 files changed, 24 insertions(+), 20 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index af8f4f3c946..c56fe8cb776 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -1,28 +1,28 @@
-- 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)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 71b84af223a..20254dda5f1 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/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
--
GitLab