[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

@@ -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

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.

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

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) =

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