From dbb4f7a6bf03bc37fd3b23f4a1bcafb1dbc341cf Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 19 Nov 2012 13:43:57 +0000
Subject: [PATCH] [E-ACSL] support of float in specification. Reals are
approximated by float. [E-ACSL] fixed bug #1307 (typing crash in presence of
reals) [E-ACSL] fixed bug in the pre-analysis on function call [E-ACSL] fixed
bug with non-integer operators with a GMP operand
---
src/plugins/e-acsl/TODO | 6 +++---
src/plugins/e-acsl/doc/Changelog | 2 ++
src/plugins/e-acsl/pre_analysis.ml | 10 ++++-----
src/plugins/e-acsl/translate.ml | 5 ++++-
src/plugins/e-acsl/typing.ml | 34 ++++++++++++++++++------------
5 files changed, 34 insertions(+), 23 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 48e997d5197..ba4ed51a737 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -5,7 +5,6 @@
- [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
########
@@ -13,7 +12,9 @@
########
- grep TODO *.ml*
-- gestion des initialiseurs des globals: requiert un main
+- Gestion du mode -lib-entry
+- init du main dans une fonction séparée
+- l'init du main doit être généré même quand il n'y a pas de main
- mkcall ne devrait pas générer de nouvelles variables pour une même fonction
- variable GMP potentiellement initialisé mais non utilisé en présence de \at
(voir test result.i, cas -e-acsl-gmp-only)
@@ -43,4 +44,3 @@
- inclure exemple du E-ACSL Reference Manual
- test arith.i: mettre les exemples du ACSL manual about div and modulo
-- tests intensifs modèle mémoire
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 653d3355f8f..23ea24dfff9 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+- E-ACSL [2012/11/19] Support of floats in annotations. Approximate
+ reals by floats.
- E-ACSL [2012/10/25] Support of \valid.
- E-ACSL [2012/10/25] Support of \initialized.
- E-ACSL [2012/10/25] Support of \block_length.
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index a8b75b100e0..06b677de5c7 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -259,7 +259,9 @@ module rec Transfer
(match lv with
| Var vi, _ -> Varinfo.Set.add vi varinfos
| Mem e, _ -> register_exp varinfos e)
- | UnOp(_, e, _) | CastE(_, e) | Info(e, _) -> register_exp varinfos e
+ | UnOp(_, e, _) | CastE(_, e) | Info(e, _)
+ | BinOp((MinusPI | PlusPI | IndexPI), e, _, _) ->
+ register_exp varinfos e
| BinOp(_, e1, e2, _) ->
let s = register_exp varinfos e1 in
register_exp s e2
@@ -330,10 +332,8 @@ module rec Transfer
kept *)
List.fold_left2
(fun acc p a ->
- if Varinfo.Set.mem p state_kf then
- extend_to_expr acc (Var p) a
- else
- acc)
+ if Varinfo.Set.mem p state_kf then register_exp acc a
+ else acc)
state
params
l
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 9d84040af37..9eb88f7d4ea 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -76,7 +76,10 @@ let constant_to_exp ?(loc=Location.unknown) = function
| LStr s -> Cil.new_exp ?loc (Const (CStr s)), false
| LWStr s -> Cil.new_exp ?loc (Const (CWStr s)), false
| LChr c -> Cil.new_exp ?loc (Const (CChr c)), false
- | LReal _ -> Error.not_yet "real"
+ | LReal(f, s) ->
+ Options.feedback ~current:true ~once:true
+ "approximating a real number by a float";
+ Cil.new_exp ?loc (Const (CReal (f, FLongDouble, Some s))), false
| LEnum e -> Cil.new_exp ?loc (Const (CEnum e)), false
let conditional_to_exp ?(name="if") loc ctx e1 (e2, env2) (e3, env3) =
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 433dde032bf..09fda14e454 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -67,7 +67,7 @@ let typ_of_eacsl_typ = function
let is_pos = BI.ge l BI.zero in
(try
let mk n k =
- if is_representable n k then TInt(k, [])
+ if is_representable n k then TInt(k, [])
else raise Not_representable
in
let ty_l = mk l (Cil.intKindForValue l is_pos) in
@@ -81,7 +81,10 @@ let typ_of_eacsl_typ = function
| No_integral (Ltype _) -> Error.not_yet "typing of user-defined logic type"
| No_integral (Lvar _) -> Error.not_yet "type variable"
| No_integral Linteger -> assert false
- | No_integral Lreal -> Error.not_yet "real numbers"
+ | No_integral Lreal ->
+ Options.warning ~current:true ~once:true
+ "approximating type `real' by `long double'";
+ TFloat(FLongDouble, [])
| No_integral (Larrow _) -> Error.not_yet "functional type"
let eacsl_typ_of_typ ty = match Cil.unrollType ty with
@@ -153,7 +156,10 @@ let typ_of_term t =
| Ltype _ as ty when Logic_const.is_boolean_type ty -> Mpz.t ()
| Ltype _ -> Error.not_yet "typing of user-defined logic type"
| Lvar _ -> Error.not_yet "type variable"
- | Lreal -> Error.not_yet "real numbers"
+ | Lreal ->
+ Options.warning ~current:true ~once:true
+ "approximating type `real' by `long double'";
+ TFloat(FLongDouble, [])
| Larrow _ -> Error.not_yet "functional type"
else
try
@@ -220,15 +226,15 @@ let rec type_term t =
Interv(BI.zero, BI.one)
| TBinOp(PlusA, t1, t2) ->
let add l1 u1 l2 u2 = BI.add l1 l2, BI.add u1 u2 in
- binary_arithmetic add t1 t2
+ binary_arithmetic t.term_type add t1 t2
| TBinOp((PlusPI | IndexPI | MinusPI | MinusPP), t1, t2) ->
ignore (type_term t1);
ignore (type_term t2);
No_integral lty
| TBinOp(MinusA, t1, t2) ->
let sub l1 u1 l2 u2 = BI.sub l1 u2, BI.sub u1 l2 in
- binary_arithmetic sub t1 t2
- | TBinOp(Mult, t1, t2) -> signed_rule BI.mul t1 t2
+ binary_arithmetic t.term_type sub t1 t2
+ | TBinOp(Mult, t1, t2) -> signed_rule t.term_type BI.mul t1 t2
| TBinOp(Div, t1, t2) ->
let div a b =
try BI.c_div a b
@@ -240,12 +246,12 @@ let rec type_term t =
order to be as more precise as possible. *)
BI.zero
in
- signed_rule div t1 t2
+ signed_rule t.term_type div t1 t2
| TBinOp(Mod, t1, t2) ->
let modu a b =
try BI.c_rem a b with Division_by_zero -> BI.zero (* see Div *)
in
- signed_rule modu t1 t2
+ signed_rule t.term_type modu t1 t2
| TBinOp(Shiftlt, _t1, _t2) | TBinOp(Shiftrt, _t1, _t2) ->
Error.not_yet "left/right shift"
| TBinOp((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), t1, t2) ->
@@ -344,17 +350,17 @@ and unary_arithmetic op t =
| Z -> Z
| No_integral _ -> assert false
-and binary_arithmetic op t1 t2 =
+and binary_arithmetic ty op t1 t2 =
let ty1 = type_term t1 in
let ty2 = type_term t2 in
match ty1, ty2 with
| Interv(l1, u1), Interv(l2, u2) ->
let l, u = op l1 u1 l2 u2 in
Interv (l, u)
- | No_integral _, _ | _, No_integral _ -> assert false
+ | No_integral _, _ | _, No_integral _ -> No_integral ty
| _, Z | Z, _ -> Z
-and signed_rule op t1 t2 =
+and signed_rule ty op t1 t2 =
(* probably not the most efficient way to compute the result, but the
shortest *)
let compute l1 u1 l2 u2 =
@@ -364,7 +370,7 @@ and signed_rule op t1 t2 =
let d = op u1 u2 in
BI.min a (BI.min b (BI.min c d)), BI.max a (BI.max b (BI.max c d))
in
- binary_arithmetic compute t1 t2
+ binary_arithmetic ty compute t1 t2
let compute_quantif_guards_ref
: (predicate named -> logic_var list -> predicate named ->
@@ -500,8 +506,8 @@ C-representable@]";
in
mk_mpz e
end
- else if Cil.isIntegralType ctx then do_int_ctx ty
- else e, env
+ else
+ do_int_ctx ty
let principal_type t1 t2 =
let ty1 = typ_of_term t1 in
--
GitLab