diff --git a/src/plugins/e-acsl/at_with_lscope.ml b/src/plugins/e-acsl/at_with_lscope.ml
index dbb8338c3907bd51be8159743fd4701cf0205250..af7ff2a1f0c51f5998ff0b9b00bf3d205e10a7d6 100644
--- a/src/plugins/e-acsl/at_with_lscope.ml
+++ b/src/plugins/e-acsl/at_with_lscope.ml
@@ -95,10 +95,7 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
| _ ->
Options.fatal "Unexpected comparison operator"
in
- let i =
- try Interval.infer t_size
- with Interval.Not_a_number | Interval.Is_a_real -> assert false
- in
+ let iv = Interval.(extract_ival (infer t_size)) in
(* The EXACT amount of memory that is needed can be known at runtime. This
is because the tightest bounds for the variables can be known at runtime.
Example: In the following predicate
@@ -116,7 +113,7 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
beneficial. In particular, though we may allocate more memory than
needed, the number of reads/writes into it is the same in both cases.
Conclusion: over-approximate [t_size] *)
- let t_size = match Ival.min_and_max i with
+ let t_size = match Ival.min_and_max iv with
| _, Some max ->
Logic_const.tint ~loc max
| _, None ->
@@ -233,9 +230,9 @@ let to_exp ~loc kf env pot label =
Cil.intType
| Misc.PoT_term t ->
begin match Typing.get_number_ty t with
- | Typing.C_type _ | Typing.Nan ->
+ | Typing.(C_integer _ | C_float _ | Nan) ->
Typing.get_typ t
- | Typing.Real ->
+ | Typing.(Rational | Real) ->
Error.not_yet "\\at on purely logic variables and over real type"
| Typing.Gmpz ->
Error.not_yet "\\at on purely logic variables and over gmp type"
@@ -259,20 +256,19 @@ let to_exp ~loc kf env pot label =
in
Typing.type_term ~use_gmp_opt:false t_size;
let malloc_stmt = match Typing.get_number_ty t_size with
- | Typing.C_type IInt ->
+ | Typing.C_integer IInt ->
let e_size, _ = term_to_exp kf env t_size in
let e_size = Cil.constFold false e_size in
let malloc_stmt =
Misc.mk_call ~loc ~result:(Cil.var vi) "malloc" [e_size]
in
malloc_stmt
- | Typing.C_type _ | Typing.Gmpz ->
+ | Typing.(C_integer _ | C_float _ | Gmpz) ->
Error.not_yet
"\\at on purely logic variables that needs to allocate \
- too much memory (bigger than int_max bytes)"
- | Typing.Real | Typing.Nan ->
- Options.fatal
- "quantification over non-integer type is not part of E-ACSL"
+ too much memory (bigger than int_max bytes)"
+ | Typing.(Rational | Real | Nan) ->
+ Error.not_yet "quantification over non-integer type"
in
let free_stmt = Misc.mk_call ~loc "free" [e] in
(* The list of stmts returned by the current closure are inserted
@@ -306,7 +302,7 @@ let to_exp ~loc kf env pot label =
[ Cil.mkStmt ~valid_sid:true (Block block) ], env
| Misc.PoT_term t ->
begin match Typing.get_number_ty t with
- | Typing.C_type _ | Typing.Nan ->
+ | Typing.(C_integer _ | C_float _ | Nan) ->
let env = Env.push env in
let lval, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
let e, env = term_to_exp kf env t in
@@ -320,7 +316,7 @@ let to_exp ~loc kf env pot label =
(* We CANNOT return [block.bstmts] because it does NOT contain
variable declarations. *)
[ Cil.mkStmt ~valid_sid:true (Block block) ], env
- | Typing.Real ->
+ | Typing.(Rational | Real) ->
Error.not_yet "\\at on purely logic variables and over real type"
| Typing.Gmpz ->
Error.not_yet "\\at on purely logic variables and over gmp type"
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index e2e7dc95323b11f513de5d200d007cc98184497f..3aab01f01d3d31e387085dadc8538cde56f8e824 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -30,20 +30,151 @@ open Cil_types
(* Basic datatypes and operations *)
(* ********************************************************************* *)
-exception Is_a_real
-exception Not_a_number
+type ival =
+ | Ival of Ival.t
+ | Float of fkind * float option (* a float constant, if any *)
+ | Rational
+ | Real
+ | Nan
+
+module D =
+ Datatype.Make_with_collections
+ (struct
+ type t = ival
+ let name = "E_ACSL.Interval.t"
+ let reprs = [ Float (FFloat, Some 0.); Rational; Real; Nan ]
+ include Datatype.Undefined
+
+ let compare i1 i2 =
+ if i1 == i2 then 0
+ else
+ match i1, i2 with
+ | Ival i1, Ival i2 ->
+ Ival.compare i1 i2
+ | Float (k1, f1), Float (k2, f2) ->
+ (* faster to compare a kind than a float *)
+ let n = Stdlib.compare k1 k2 in
+ if n = 0 then Stdlib.compare f1 f2 else n
+ | Ival _, (Float _ | Rational | Real | Nan)
+ | Float _, (Rational | Real | Nan)
+ | Rational, (Real | Nan)
+ | Real, Nan ->
+ -1
+ | Nan, (Ival _ | Float _ | Rational | Real)
+ | Real, (Ival _ | Float _ | Rational)
+ | Rational, (Ival _ | Float _)
+ | Float _, Ival _ ->
+ 1
+ | Rational, Rational | Real, Real | Nan, Nan ->
+ assert false
+
+ let equal = Datatype.from_compare
+
+ let hash = function
+ | Ival i -> 7 * Ival.hash i
+ | Float(k, f) -> 17 * Hashtbl.hash f + 97 * Hashtbl.hash k
+ | Rational -> 787
+ | Real -> 1011
+ | Nan -> 1277
+
+ let pretty fmt = function
+ | Ival i -> Ival.pretty fmt i
+ | Float(_, Some f) -> Format.pp_print_float fmt f
+ | Float(FFloat, None) -> Format.pp_print_string fmt "float"
+ | Float(FDouble, None) -> Format.pp_print_string fmt "double"
+ | Float(FLongDouble, None) -> Format.pp_print_string fmt "long double"
+ | Rational -> Format.pp_print_string fmt "Rational"
+ | Real -> Format.pp_print_string fmt "Real"
+ | Nan -> Format.pp_print_string fmt "NaN"
+
+ end)
+
+let is_included i1 i2 = match i1, i2 with
+ | Ival i1, Ival i2 -> Ival.is_included i1 i2
+ | Float(k1, f1), Float(k2, f2) ->
+ Stdlib.compare k1 k2 <= 0
+ && (match f1, f2 with
+ | None, None | Some _, None -> true
+ | None, Some _ -> false
+ | Some f1, Some f2 -> f1 = f2)
+ | (Ival _ | Float _ | Rational), (Rational | Real)
+ | Real, Real
+ | Nan, Nan ->
+ true
+ (* floats and integer are not comparable: *)
+ | Ival _, Float _ | Float _, Ival _
+ (* nan is comparable to noone, but itself: *)
+ | (Ival _ | Float _ | Rational | Real), Nan
+ | Nan, (Ival _ | Float _ | Rational | Real)
+ (* cases for reals and rationals: *)
+ | Real, (Ival _ | Float _ | Rational)
+ | Rational, (Ival _ | Float _) ->
+ false
+
+let lift_unop f = function
+ | Ival iv -> Ival (f iv)
+ | Float _ ->
+ (* any unary operator over a float generates a rational
+ TODO: actually, certainly possible to generate a float *)
+ Rational
+ | Rational | Real | Nan as i -> i
+
+let lift_binop ~safe_float f i1 i2 = match i1, i2 with
+ | Ival i1, Ival i2 ->
+ Ival (f i1 i2)
+ | Float(k1, _), Float(k2, _) when safe_float ->
+ let k = if Stdlib.compare k1 k2 >= 0 then k1 else k2 in
+ Float(k, None (* lost value, if any before *))
+ | (Ival _ | Float _ | Rational), (Float _ | Rational)
+ | (Float _ | Rational), Ival _ ->
+ (* any binary operator over a float or a rational generates a rational *)
+ Rational
+ | (Ival _ | Float _ | Rational | Real), Real
+ | Real, (Ival _ | Float _ | Rational) ->
+ Real
+ | (Ival _ | Float _ | Rational | Real | Nan), Nan
+ | Nan, (Ival _ | Float _ | Rational | Real) ->
+ Nan
+
+let join = lift_binop ~safe_float:true Ival.join
+
+(* TODO: soundness of any downcast is not checked *)
+let cast ~src ~dst = match src, dst with
+ | Ival i1, Ival i2 ->
+ Ival (Ival.meet i1 i2)
+ | _, Float(_, Some _) ->
+ assert false
+ | Rational, Real
+ | Float _, (Rational | Real) ->
+ src
+ | _, _ ->
+ (* No need to optimize the other cases: if someone writes a cast
+ (in particular, from integer to float/real or conversely), it is
+ certainly on purpose . *)
+ dst
-(* constructors *)
+(* ********************************************************************* *)
+(* constructors and destructors *)
+(* ********************************************************************* *)
-let singleton_of_int n = Ival.inject_singleton (Integer.of_int n)
+let extract_ival = function
+ | Ival iv -> iv
+ | Float _ | Rational | Real | Nan -> assert false
+
+let bottom = Ival Ival.bottom
+let top_ival = Ival (Ival.inject_range None None)
+let singleton n = Ival (Ival.inject_singleton n)
+let singleton_of_int n = singleton (Integer.of_int n)
+let ival min max = Ival (Ival.inject_range (Some min) (Some max))
let interv_of_unknown_block =
(* since we have no idea of the size of this block, we take the largest
possible one which is unfortunately quite large *)
- lazy
- (Ival.inject_range
- (Some Integer.zero)
- (Some (Bit_utils.max_byte_address ())))
+ lazy (ival Integer.zero (Bit_utils.max_byte_address ()))
+
+(* ********************************************************************* *)
+(* main algorithm *)
+(* ********************************************************************* *)
(* The boolean indicates whether we have real numbers *)
let rec interv_of_typ ty = match Cil.unrollType ty with
@@ -53,29 +184,31 @@ let rec interv_of_typ ty = match Cil.unrollType ty with
if Cil.isSigned k then Cil.min_signed_number n, Cil.max_signed_number n
else Integer.zero, Cil.max_unsigned_number n
in
- Ival.inject_range (Some l) (Some u)
+ ival l u
| TEnum(enuminfo, _) ->
- interv_of_typ (TInt (enuminfo.ekind, []))
- | TFloat _ ->
- raise Is_a_real
+ interv_of_typ (TInt(enuminfo.ekind, []))
+ | _ when Gmp.Z.is_t ty ->
+ top_ival
+ | TFloat (k, _) ->
+ Float(k, None)
| _ when Real.is_t ty ->
- raise Is_a_real
+ Rational (* only rationals are implemented *)
| TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ ->
- raise Not_a_number
+ Nan
| TNamed _ ->
assert false
let interv_of_logic_typ = function
| Ctype ty -> interv_of_typ ty
- | Linteger -> Ival.inject_range None None
- | Lreal -> raise Is_a_real
+ | Linteger -> top_ival
+ | Lreal -> Real
| Ltype _ -> Error.not_yet "user-defined logic type"
| Lvar _ -> Error.not_yet "type variable"
- | Larrow _ -> Error.not_yet "functional type"
+ | Larrow _ -> Nan
-let ikind_of_interv i =
- if Ival.is_bottom i then IInt
- else match Ival.min_and_max i with
+let ikind_of_ival iv =
+ if Ival.is_bottom iv then IInt
+ else match Ival.min_and_max iv with
| Some l, Some u ->
let is_pos = Integer.ge l Integer.zero in
let lkind = Cil.intKindForValue l is_pos in
@@ -85,31 +218,31 @@ let ikind_of_interv i =
(* convert the kind to [IInt] whenever smaller. *)
if Cil.intTypeIncluded kind IInt then IInt else kind
| None, None -> raise Cil.Not_representable (* GMP *)
+ (* TODO: do not raise an exception, but returns a value instead *)
| None, Some _ | Some _, None ->
- Kernel.fatal ~current:true "unexpected ival: %a" Ival.pretty i
+ Kernel.fatal ~current:true "unexpected ival: %a" Ival.pretty iv
(* function call profiles (intervals for their formal parameters) *)
module Profile = struct
include Datatype.List_with_collections
- (Ival)
+ (D)
(struct
let module_name = "E_ACSL.Interval.Logic_function_env.Profile"
end)
- let is_included p1 p2 = List.for_all2 Ival.is_included p1 p2
- let _join p1 p2 = List.map2 Ival.join p1 p2 (* TODO: to be removed *)
+ let is_included p1 p2 = List.for_all2 is_included p1 p2
end
(* Imperative environments *)
module rec Env: sig
val clear: unit -> unit
- val add: Cil_types.logic_var -> Ival.t -> unit
- val find: Cil_types.logic_var -> Ival.t
+ val add: Cil_types.logic_var -> ival -> unit
+ val find: Cil_types.logic_var -> ival
val remove: Cil_types.logic_var -> unit
- val replace: Cil_types.logic_var -> Ival.t -> unit
+ val replace: Cil_types.logic_var -> ival -> unit
end = struct
open Cil_datatype
- let tbl: Ival.t Logic_var.Hashtbl.t = Logic_var.Hashtbl.create 7
+ let tbl: ival Logic_var.Hashtbl.t = Logic_var.Hashtbl.create 7
(* TODO: when adding, also join with the old value (if any). Would certainly
be the correct way to handle a \let in a recursive logic functions (if the
@@ -127,7 +260,7 @@ end
(* Environment for handling logic functions *)
and Logic_function_env: sig
- val widen: infer:(term -> Ival.t) -> term -> Ival.t -> bool * Ival.t
+ val widen: infer:(term -> ival) -> term -> ival -> bool * ival
val clear: unit -> unit
end = struct
@@ -161,13 +294,15 @@ end = struct
Terms.clear terms;
LF.Hashtbl.clear named_profiles
- let interv_of_typ_containing_interv i =
- try
- let kind = ikind_of_interv i in
- interv_of_typ (TInt(kind, []))
- with Cil.Not_representable ->
- (* infinity *)
- Ival.inject_range None None
+ let interv_of_typ_containing_interv = function
+ | Float _ | Rational | Real | Nan as x ->
+ x
+ | Ival i ->
+ try
+ let kind = ikind_of_ival i in
+ interv_of_typ (TInt(kind, []))
+ with Cil.Not_representable ->
+ top_ival
let rec map3 f l1 l2 l3 = match l1, l2, l3 with
| [], [], [] -> []
@@ -177,24 +312,20 @@ end = struct
let extract_profile ~infer old_profile t = match t.term_node with
| Tapp(li, _, args) ->
let old_profile = match old_profile with
- | None -> List.map (fun _ -> Ival.bottom) li.l_profile
+ | None -> List.map (fun _ -> bottom) li.l_profile
| Some p -> p
in
li.l_var_info.lv_name,
map3
(fun param old_i arg ->
- try
- let i = infer arg in
- (* over-approximation of the interval to reach the fixpoint
- faster, and to generate fewer specialized functions *)
- let larger_i = interv_of_typ_containing_interv i in
- (* merge the old profile and the new one *)
- let new_i = Ival.join larger_i old_i in
- Env.add param new_i;
- new_i
- with Not_a_number ->
- (* no need to add [param] to the environment *)
- Ival.bottom)
+ let i = infer arg in
+ (* over-approximation of the interval to reach the fixpoint
+ faster, and to generate fewer specialized functions *)
+ let larger_i = interv_of_typ_containing_interv i in
+ (* merge the old profile and the new one *)
+ let new_i = join larger_i old_i in
+ Env.add param new_i;
+ new_i)
li.l_profile
old_profile
args
@@ -205,9 +336,9 @@ end = struct
let (_, p as named_p) = extract_profile ~infer old_profile t in
try
let old_i = LF.Hashtbl.find named_profiles named_p in
- if Ival.is_included i old_i then true, p, old_i
+ if is_included i old_i then true, p, old_i
else begin
- let j = Ival.join i old_i in
+ let j = join i old_i in
LF.Hashtbl.replace named_profiles named_p j;
false, p, j
end
@@ -244,17 +375,17 @@ let infer_alignof ty = singleton_of_int (Cil.bytesAlignOf ty)
let rec infer t =
let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in
match t.term_node with
- | TConst (Integer (n, _)) -> Ival.inject_singleton n
+ | TConst (Integer (n, _)) -> singleton n
| TConst (LChr c) ->
let n = Cil.charConstToInt c in
- Ival.inject_singleton n
+ singleton n
| TConst (LEnum enumitem) ->
let rec find_idx n = function
| [] -> assert false
| ei :: l -> if ei == enumitem then n else find_idx (n + 1) l
in
let n = Integer.of_int (find_idx 0 enumitem.eihost.eitems) in
- Ival.inject_singleton n
+ singleton n
| TLval lv -> infer_term_lval lv
| TSizeOf ty -> infer_sizeof ty
| TSizeOfE t -> infer_sizeof (get_cty t)
@@ -264,66 +395,53 @@ let rec infer t =
| TUnOp (Neg, t) ->
let i = infer t in
- Ival.neg_int i
+ lift_unop Ival.neg_int i
| TUnOp (BNot, t) ->
let i = infer t in
- Ival.bitwise_signed_not i
+ lift_unop Ival.bitwise_signed_not i
| TUnOp (LNot, _)
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _) ->
- Ival.zero_or_one
+ Ival Ival.zero_or_one
| TBinOp (PlusA, t1, t2) ->
let i1 = infer t1 in
let i2 = infer t2 in
- Ival.add_int i1 i2
+ lift_binop ~safe_float:false Ival.add_int i1 i2
| TBinOp (MinusA, t1, t2) ->
let i1 = infer t1 in
let i2 = infer t2 in
- Ival.sub_int i1 i2
+ lift_binop ~safe_float:false Ival.sub_int i1 i2
| TBinOp (Mult, t1, t2) ->
let i1 = infer t1 in
let i2 = infer t2 in
- Ival.mul i1 i2
+ lift_binop ~safe_float:false Ival.mul i1 i2
| TBinOp (Div, t1, t2) ->
let i1 = infer t1 in
let i2 = infer t2 in
- Ival.div i1 i2
+ lift_binop ~safe_float:false Ival.div i1 i2
| TBinOp (Mod, t1, t2) ->
let i1 = infer t1 in
let i2 = infer t2 in
- Ival.c_rem i1 i2
+ lift_binop ~safe_float:false Ival.c_rem i1 i2
| TBinOp (Shiftlt , _, _) -> Error.not_yet "right shift"
| TBinOp (Shiftrt , _, _) -> Error.not_yet "left shift"
| TBinOp (BAnd, _, _) -> Error.not_yet "bitwise and"
| TBinOp (BXor, t1, t2) ->
let i1 = infer t1 in
let i2 = infer t2 in
- Ival.bitwise_xor i1 i2
+ lift_binop ~safe_float:false Ival.bitwise_xor i1 i2
| TBinOp (BOr, t1, t2) ->
let i1 = infer t1 in
let i2 = infer t2 in
- Ival.bitwise_or i1 i2
+ lift_binop ~safe_float:false Ival.bitwise_or i1 i2
| TCastE (ty, t) ->
- (try
- let it = infer t in
- let ity = interv_of_typ ty in
- Ival.meet it ity
- with Not_a_number ->
- if Cil.isIntegralType ty then begin
- (* heterogeneous cast from a non-integral term to an integral type:
- consider that one eventually gets an integral type even if it is
- not sure. *)
- Options.warning
- ~once:true "possibly unsafe cast from term '%a' to type '%a'."
- Printer.pp_term t
- Printer.pp_typ ty;
- interv_of_typ ty
- end else
- raise Not_a_number)
+ let src = infer t in
+ let dst = interv_of_typ ty in
+ cast ~src ~dst
| Tif (_, t2, t3) ->
let i2 = infer t2 in
let i3 = infer t3 in
- Ival.join i2 i3
+ join i2 i3
| Tat (t, _) ->
infer t
| TBinOp (MinusPP, t, _) ->
@@ -332,10 +450,7 @@ let rec infer t =
(* the second argument must be in the same block than [t]. Consequently
the result of the difference belongs to [0; \block_length(t)] *)
let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
- let i =
- Ival.inject_range (Some Integer.zero) (Some (Integer.of_int nb_bytes))
- in
- i
+ ival Integer.zero (Integer.of_int nb_bytes)
| TArray _ | TPtr _ ->
Lazy.force interv_of_unknown_block
| _ -> assert false)
@@ -353,7 +468,7 @@ let rec infer t =
| Tapp (li, _, _args) ->
(match li.l_body with
| LBpred _ ->
- Ival.zero_or_one
+ Ival Ival.zero_or_one
| LBterm t' ->
let rec fixpoint i =
let is_included, new_i =
@@ -367,11 +482,7 @@ let rec infer t =
List.iter (fun lv -> Env.remove lv) li.l_profile;
fixpoint i
in
- let i = fixpoint Ival.bottom in
- (* call [interv_of_logic_typ] in order to raise Is_a_real or Not_a_number
- when the function does not return an integer *)
- Extlib.may (fun lty -> ignore (interv_of_logic_typ lty)) li.l_type;
- i
+ fixpoint bottom
| LBnone
| LBreads _ ->
(match li.l_type with
@@ -386,7 +497,7 @@ let rec infer t =
| Trange(Some n1, Some n2) ->
let i1 = infer n1 in
let i2 = infer n2 in
- Ival.join i1 i2
+ join i1 i2
| Trange(None, _) | Trange(_, None) ->
Options.abort "unbounded ranges are not part of E-ACSl"
@@ -398,8 +509,9 @@ let rec infer t =
let i2 = infer t in
Env.remove li_v;
i2
- | TConst (LReal _) ->
- raise Is_a_real
+ | TConst (LReal lr) ->
+ if lr.r_lower = lr.r_upper then Float(FDouble, Some lr.r_nearest)
+ else Rational
| TConst (LStr _ | LWStr _)
| TBinOp (PlusPI,_,_)
| TBinOp (IndexPI,_,_)
@@ -413,7 +525,7 @@ let rec infer t =
| Ttypeof _
| Ttype _
| Tempty_set ->
- raise Not_a_number
+ Nan
and infer_term_lval (host, offset as tlv) =
match offset with
@@ -425,11 +537,11 @@ and infer_term_lval (host, offset as tlv) =
and infer_term_host thost =
match thost with
| TVar v ->
- (try Env.find v
- with Not_found ->
+ (try Env.find v with Not_found ->
match v.lv_type with
- | Linteger -> Ival.inject_range None None
- | Ctype (TFloat _) | Lreal -> raise Is_a_real
+ | Linteger -> top_ival
+ | Ctype (TFloat(fk, _)) -> Float(fk, None)
+ | Lreal -> Real
| Ctype _ -> interv_of_typ (Logic_utils.logicCType v.lv_type)
| Ltype _ | Lvar _ | Larrow _ -> Options.fatal "unexpected logic type")
| TResult ty ->
@@ -444,6 +556,8 @@ and infer_term_host thost =
Printer.pp_typ ty
Printer.pp_term t
+include D
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/interval.mli b/src/plugins/e-acsl/interval.mli
index 9d7b5d59a91b56ff6aca9b15cb76a923b6637c9d..4260d80f8a3f8114ed328d15d20f0d9b8a4aa76c 100644
--- a/src/plugins/e-acsl/interval.mli
+++ b/src/plugins/e-acsl/interval.mli
@@ -51,15 +51,30 @@
(** {3 Useful operations on intervals} *)
(* ************************************************************************** *)
-exception Is_a_real
-exception Not_a_number
+type ival =
+ | Ival of Ival.t
+ | Float of Cil_types.fkind * float option
+ | Rational
+ | Real
+ | Nan
-val ikind_of_interv: Ival.t -> Cil_types.ikind
+include Datatype.S_with_collections with type t = ival
+
+val is_included: t -> t -> bool
+val join: t -> t -> t
+
+val top_ival: t
+val ival: Integer.t -> Integer.t -> t
+
+(** assume [Ival _] as argument *)
+val extract_ival: t -> Ival.t
+
+val ikind_of_ival: Ival.t -> Cil_types.ikind
(** @return the smallest ikind that contains the given interval.
@raise Cil.Not_representable if the given interval does not fit into any C
integral type. *)
-val interv_of_typ: Cil_types.typ -> Ival.t
+val interv_of_typ: Cil_types.typ -> t
(** @return the smallest interval which contains the given C type.
@raise Is_a_real if the given type is a float type.
@raise Not_a_number if the given type does not represent any number. *)
@@ -72,16 +87,16 @@ val interv_of_typ: Cil_types.typ -> Ival.t
be extended from outside. *)
module Env: sig
val clear: unit -> unit
- val add: Cil_types.logic_var -> Ival.t -> unit
+ val add: Cil_types.logic_var -> t -> unit
val remove: Cil_types.logic_var -> unit
- val replace: Cil_types.logic_var -> Ival.t -> unit
+ val replace: Cil_types.logic_var -> t -> unit
end
(* ************************************************************************** *)
(** {3 Inference system} *)
(* ************************************************************************** *)
-val infer: Cil_types.term -> Ival.t
+val infer: Cil_types.term -> t
(** [infer t] infers the smallest possible integer interval which the values
of the term can fit in.
@raise Is_a_real if the term is either a float or a real.
diff --git a/src/plugins/e-acsl/logic_functions.ml b/src/plugins/e-acsl/logic_functions.ml
index f688b954836842a39eca24a22da1be98733597ed..dfaec0c2b93c95c1c868027c8604917518b5894c 100644
--- a/src/plugins/e-acsl/logic_functions.ml
+++ b/src/plugins/e-acsl/logic_functions.ml
@@ -126,8 +126,11 @@ let generate_kf ~loc fname env ret_ty params_ty li =
(* GMP's integer are arrays: consider them as pointers in function's
parameters *)
Gmp.Z.t_as_ptr ()
- | Typing.C_type ik -> TInt(ik, [])
- | Typing.Real -> assert false (* TODO RATIONAL: to be implemented *)
+ | Typing.C_integer ik -> TInt(ik, [])
+ | Typing.C_float ik -> TFloat(ik, [])
+ (* for the time being, no reals but rationals instead *)
+ | Typing.Rational -> Real.t ()
+ | Typing.Real -> Error.not_yet "real number"
| Typing.Nan -> Typing.typ_of_lty lvi.lv_type
in
(* build the formals: cannot use [Cil.makeFormal] since the function
@@ -190,14 +193,7 @@ let generate_kf ~loc fname env ret_ty params_ty li =
before generating the code (code generation invokes typing) *)
let env =
let add env lvi vi =
- let i =
- try
- Interval.interv_of_typ vi.vtype
- with
- | Interval.Not_a_number
- | Interval.Is_a_real ->
- Ival.inject_range None None
- in
+ let i = Interval.interv_of_typ vi.vtype in
Interval.Env.add lvi i;
Env.Logic_binding.add_binding env lvi vi
in
diff --git a/src/plugins/e-acsl/loops.ml b/src/plugins/e-acsl/loops.ml
index a41da743536de9d61a684126e138fef6b9380331..7ed887499ba3ac1622f6727d2cff36319a5d56f6 100644
--- a/src/plugins/e-acsl/loops.ml
+++ b/src/plugins/e-acsl/loops.ml
@@ -117,51 +117,49 @@ let preserve_invariant prj env kf stmt = match stmt.skind with
Return: R with a guard guaranteeing that [lv] does not overflow *)
let bounds_for_small_type ~loc (t1, lv, t2) =
match lv.lv_type with
+ | Ltype _ | Lvar _ | Lreal | Larrow _ ->
+ Options.abort "quantification over non-integer type is not part of E-ACSL"
+
| Linteger ->
t1, t2, None
+
| Ctype ty ->
- (try
- let i1 = Interval.infer t1 in
- let i2 = Interval.infer t2 in
- let i =
- (* Ival.join would NOT be correct here:
- Eg: (Ival.join [-3..-3] [300..300]) gives {-3, 300}
- but NOT [-3..300] *)
- Ival.inject_range (Ival.min_int i1) (Ival.max_int i2)
- in
- let ity = Interval.interv_of_typ ty in
- if Ival.is_included i ity then
- (* case 1 *)
- t1, t2, None
- else if Ival.is_singleton_int i1 && Ival.is_singleton_int i2 then begin
- (* case 2 *)
- let i = Ival.meet i ity in
- (* now we potentially have a better interval for [lv]
- ==> update the binding *)
- Interval.Env.replace lv i;
- (* the smaller bounds *)
- let min, max = Misc.finite_min_and_max i in
- let t1 = Logic_const.tint ~loc min in
- let t2 = Logic_const.tint ~loc max in
- let ctx = Typing.number_ty_of_typ ty in
- (* we are assured that we will not have a GMP,
- once again because we intersected with [ity] *)
- Typing.type_term ~use_gmp_opt:false ~ctx t1;
- Typing.type_term ~use_gmp_opt:false ~ctx t2;
- t1, t2, None
- end else
- (* case 3 *)
- let min, max = Misc.finite_min_and_max ity in
- let guard_lower = Logic_const.tint ~loc min in
- let guard_upper = Logic_const.tint ~loc max in
- let lv_term = Logic_const.tvar ~loc lv in
- let guard_lower = Logic_const.prel ~loc (Rle, guard_lower, lv_term) in
- let guard_upper = Logic_const.prel ~loc (Rle, lv_term, guard_upper) in
- let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
- t1, t2, Some guard
- with Interval.Not_a_number | Interval.Is_a_real -> assert false)
- | Ltype _ | Lvar _ | Lreal | Larrow _ ->
- Options.abort "quantification over non-integer type is not part of E-ACSL"
+ let iv1 = Interval.(extract_ival (infer t1)) in
+ let iv2 = Interval.(extract_ival (infer t2)) in
+ (* Ival.join is NOT correct here:
+ Eg: (Ival.join [-3..-3] [300..300]) gives {-3, 300}
+ but NOT [-3..300] *)
+ let iv = Ival.inject_range (Ival.min_int iv1) (Ival.max_int iv2) in
+ let ity = Interval.extract_ival (Interval.interv_of_typ ty) in
+ if Ival.is_included iv ity then
+ (* case 1 *)
+ t1, t2, None
+ else if Ival.is_singleton_int iv1 && Ival.is_singleton_int iv2 then begin
+ (* case 2 *)
+ let i = Ival.meet iv ity in
+ (* now we potentially have a better interval for [lv]
+ ==> update the binding *)
+ Interval.Env.replace lv (Interval.Ival i);
+ (* the smaller bounds *)
+ let min, max = Misc.finite_min_and_max i in
+ let t1 = Logic_const.tint ~loc min in
+ let t2 = Logic_const.tint ~loc max in
+ let ctx = Typing.number_ty_of_typ ty in
+ (* we are assured that we will not have a GMP,
+ once again because we intersected with [ity] *)
+ Typing.type_term ~use_gmp_opt:false ~ctx t1;
+ Typing.type_term ~use_gmp_opt:false ~ctx t2;
+ t1, t2, None
+ end else
+ (* case 3 *)
+ let min, max = Misc.finite_min_and_max ity in
+ let guard_lower = Logic_const.tint ~loc min in
+ let guard_upper = Logic_const.tint ~loc max in
+ let lv_term = Logic_const.tvar ~loc lv in
+ let guard_lower = Logic_const.prel ~loc (Rle, guard_lower, lv_term) in
+ let guard_upper = Logic_const.prel ~loc (Rle, lv_term, guard_upper) in
+ let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
+ t1, t2, Some guard
let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let term_to_exp = !term_to_exp_ref in
@@ -224,9 +222,9 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let var_x, x, env = Env.Logic_binding.add ~ty env logic_x in
let lv_x = var var_x in
let env = match ctx_one with
- | Typing.C_type _ -> env
+ | Typing.C_integer _ -> env
| Typing.Gmpz -> Env.add_stmt env (Gmp.init ~loc x)
- | Typing.Real | Typing.Nan -> assert false
+ | Typing.(C_float _ | Rational | Real | Nan) -> assert false
in
(* build the inner loops and loop body *)
let body, env =
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 0c62fb7c2c9706683c5511a27af9488411945abd..2f886c8ce5492a491518d8b1751a9bfdcd4a9144 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -246,6 +246,7 @@ let rec ptr_index ?(loc=Location.unknown) ?(index=(Cil.zero loc)) exp =
| SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
-> assert false
+(* TODO: should not be in this file *)
let term_of_li li = match li.l_body with
| LBterm t -> t
| LBnone | LBreads _ | LBpred _ | LBinductive _ ->
diff --git a/src/plugins/e-acsl/mmodel_translate.ml b/src/plugins/e-acsl/mmodel_translate.ml
index 7457de1d8cda7bc72736ca81a586c1795fb9a226..314f9c38c1797c55db1469ed39beafe5409ca0c4 100644
--- a/src/plugins/e-acsl/mmodel_translate.ml
+++ b/src/plugins/e-acsl/mmodel_translate.ml
@@ -211,10 +211,10 @@ let call_memory_block ~loc kf name ctx env ptr r p =
let size, env = match Typing.get_number_ty size_term with
| Typing.Gmpz ->
gmp_to_sizet ~loc kf env size_term p
- | Typing.C_type _ ->
+ | Typing.(C_integer _ | C_float _) ->
let size, env = term_to_exp kf env size_term in
Cil.constFold false size, env
- | Typing.Real | Typing.Nan ->
+ | Typing.(Rational | Real | Nan) ->
assert false
in
(* base and base_addr *)
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index a1ae19acb6cf7623ae26e635d9857f1daf17ec7b..58dad26a6507d6b4025b464c686275835153f8c3 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -113,25 +113,21 @@ let rec has_empty_quantif_with_false_negative = function
(* case 2 *)
false
| (t1, rel1, _, rel2, t2) :: guards ->
- try
- let i1 = Interval.infer t1 in
- let i2 = Interval.infer t2 in
- let lower_bound, _ = Ival.min_and_max i1 in
- let _, upper_bound = Ival.min_and_max i2 in
- match lower_bound, upper_bound with
- | Some lower_bound, Some upper_bound ->
- let res = match rel1, rel2 with
- | Rle, Rle -> lower_bound > upper_bound
- | Rle, Rlt | Rlt, Rle -> lower_bound >= upper_bound
- | Rlt, Rlt -> lower_bound >= Z.sub upper_bound Z.one
- | _ -> assert false
- in
- res (* case 1 *) || has_empty_quantif_with_false_negative guards
- | None, _ | _, None ->
- has_empty_quantif_with_false_negative guards
- with
- | Interval.Not_a_number -> assert false
- | Interval.Is_a_real -> Error.not_yet "quantification over real numbers"
+ let iv1 = Interval.(extract_ival (infer t1)) in
+ let iv2 = Interval.(extract_ival (infer t2)) in
+ let lower_bound, _ = Ival.min_and_max iv1 in
+ let _, upper_bound = Ival.min_and_max iv2 in
+ match lower_bound, upper_bound with
+ | Some lower_bound, Some upper_bound ->
+ let res = match rel1, rel2 with
+ | Rle, Rle -> lower_bound > upper_bound
+ | Rle, Rlt | Rlt, Rle -> lower_bound >= upper_bound
+ | Rlt, Rlt -> lower_bound >= Z.sub upper_bound Z.one
+ | _ -> assert false
+ in
+ res (* case 1 *) || has_empty_quantif_with_false_negative guards
+ | None, _ | _, None ->
+ has_empty_quantif_with_false_negative guards
let () = Typing.compute_quantif_guards_ref := compute_quantif_guards
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index efbf831c0e626b5573f733d25e2ca2b6fa140bd0..c5ca246ce62c926a23616be2649c675d0a121fcf 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -126,79 +126,81 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
}
bar(Mtmin_in,Mwmin,Mtmin_out);
{
- __e_acsl_mpq_t __gen_e_acsl_;
- __e_acsl_mpq_t __gen_e_acsl__2;
- int __gen_e_acsl_eq;
+ int __gen_e_acsl_valid_read;
+ int __gen_e_acsl_valid_read_2;
int __gen_e_acsl_and;
int __gen_e_acsl_if;
- __gmpq_init(__gen_e_acsl_);
- __gmpq_set_d(__gen_e_acsl_,(double)*__gen_e_acsl_at);
- __gmpq_init(__gen_e_acsl__2);
- __gmpq_set_d(__gen_e_acsl__2,(double)*__gen_e_acsl_at_2);
- __gen_e_acsl_eq = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__2));
- if (__gen_e_acsl_eq == 0) {
- __e_acsl_mpq_t __gen_e_acsl__3;
- __e_acsl_mpq_t __gen_e_acsl__4;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
+ sizeof(float),
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
+ __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"bar",
+ (char *)"mem_access: \\valid_read(__gen_e_acsl_at_2)",26);
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
+ sizeof(float),
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"bar",
+ (char *)"mem_access: \\valid_read(__gen_e_acsl_at)",26);
+ if (*__gen_e_acsl_at == *__gen_e_acsl_at_2) {
+ __e_acsl_mpq_t __gen_e_acsl_;
+ __e_acsl_mpq_t __gen_e_acsl__2;
__e_acsl_mpq_t __gen_e_acsl_mul;
- __e_acsl_mpq_t __gen_e_acsl__5;
+ __e_acsl_mpq_t __gen_e_acsl__3;
int __gen_e_acsl_lt;
- __gmpq_init(__gen_e_acsl__3);
- __gmpq_set_str(__gen_e_acsl__3,"085/100",10);
- __gmpq_init(__gen_e_acsl__4);
- __gmpq_set_d(__gen_e_acsl__4,(double)*__gen_e_acsl_at_4);
+ __gmpq_init(__gen_e_acsl_);
+ __gmpq_set_str(__gen_e_acsl_,"085/100",10);
+ __gmpq_init(__gen_e_acsl__2);
+ __gmpq_set_d(__gen_e_acsl__2,(double)*__gen_e_acsl_at_4);
__gmpq_init(__gen_e_acsl_mul);
__gmpq_mul(__gen_e_acsl_mul,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__3),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__4));
- __gmpq_init(__gen_e_acsl__5);
- __gmpq_set_d(__gen_e_acsl__5,(double)*__gen_e_acsl_at_3);
- __gen_e_acsl_lt = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__5),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__2));
+ __gmpq_init(__gen_e_acsl__3);
+ __gmpq_set_d(__gen_e_acsl__3,(double)*__gen_e_acsl_at_3);
+ __gen_e_acsl_lt = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__3),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_mul));
__gen_e_acsl_and = __gen_e_acsl_lt < 0;
- __gmpq_clear(__gen_e_acsl__3);
- __gmpq_clear(__gen_e_acsl__4);
+ __gmpq_clear(__gen_e_acsl_);
+ __gmpq_clear(__gen_e_acsl__2);
__gmpq_clear(__gen_e_acsl_mul);
- __gmpq_clear(__gen_e_acsl__5);
+ __gmpq_clear(__gen_e_acsl__3);
}
else __gen_e_acsl_and = 0;
if (__gen_e_acsl_and) {
- __e_acsl_mpq_t __gen_e_acsl__6;
- __e_acsl_mpq_t __gen_e_acsl__7;
- int __gen_e_acsl_ne;
- __gmpq_init(__gen_e_acsl__6);
- __gmpq_set_str(__gen_e_acsl__6,"0/1",10);
- __gmpq_init(__gen_e_acsl__7);
- __gmpq_set_d(__gen_e_acsl__7,(double)*__gen_e_acsl_at_5);
- __gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__7),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__6));
- __gen_e_acsl_if = __gen_e_acsl_ne != 0;
- __gmpq_clear(__gen_e_acsl__6);
- __gmpq_clear(__gen_e_acsl__7);
+ int __gen_e_acsl_valid_read_3;
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at_5,
+ sizeof(float),
+ (void *)__gen_e_acsl_at_5,
+ (void *)(& __gen_e_acsl_at_5));
+ __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"bar",
+ (char *)"mem_access: \\valid_read(__gen_e_acsl_at_5)",
+ 26);
+ __gen_e_acsl_if = (double)*__gen_e_acsl_at_5 != 0.;
}
else {
- __e_acsl_mpq_t __gen_e_acsl__8;
- __e_acsl_mpq_t __gen_e_acsl__9;
+ __e_acsl_mpq_t __gen_e_acsl__4;
+ __e_acsl_mpq_t __gen_e_acsl__5;
__e_acsl_mpq_t __gen_e_acsl_mul_2;
- __e_acsl_mpq_t __gen_e_acsl__10;
- int __gen_e_acsl_ne_2;
- __gmpq_init(__gen_e_acsl__8);
- __gmpq_set_str(__gen_e_acsl__8,"085/100",10);
- __gmpq_init(__gen_e_acsl__9);
- __gmpq_set_d(__gen_e_acsl__9,(double)*__gen_e_acsl_at_6);
+ __e_acsl_mpq_t __gen_e_acsl__6;
+ int __gen_e_acsl_ne;
+ __gmpq_init(__gen_e_acsl__4);
+ __gmpq_set_str(__gen_e_acsl__4,"085/100",10);
+ __gmpq_init(__gen_e_acsl__5);
+ __gmpq_set_d(__gen_e_acsl__5,(double)*__gen_e_acsl_at_6);
__gmpq_init(__gen_e_acsl_mul_2);
__gmpq_mul(__gen_e_acsl_mul_2,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__8),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__9));
- __gmpq_init(__gen_e_acsl__10);
- __gmpq_set_str(__gen_e_acsl__10,"0/1",10);
- __gen_e_acsl_ne_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_mul_2),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__10));
- __gen_e_acsl_if = __gen_e_acsl_ne_2 != 0;
- __gmpq_clear(__gen_e_acsl__8);
- __gmpq_clear(__gen_e_acsl__9);
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
+ __gmpq_init(__gen_e_acsl__6);
+ __gmpq_set_d(__gen_e_acsl__6,0.);
+ __gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_mul_2),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__6));
+ __gen_e_acsl_if = __gen_e_acsl_ne != 0;
+ __gmpq_clear(__gen_e_acsl__4);
+ __gmpq_clear(__gen_e_acsl__5);
__gmpq_clear(__gen_e_acsl_mul_2);
- __gmpq_clear(__gen_e_acsl__10);
+ __gmpq_clear(__gen_e_acsl__6);
}
__e_acsl_assert(__gen_e_acsl_if,(char *)"Postcondition",(char *)"bar",
(char *)"*\\old(Mtmin_out) == *\\old(Mtmin_in) < 0.85 * *\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.:\n 0.85 * *\\old(Mwmin) != 0.",
@@ -206,8 +208,6 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_delete_block((void *)(& Mtmin_out));
__e_acsl_delete_block((void *)(& Mwmin));
__e_acsl_delete_block((void *)(& Mtmin_in));
- __gmpq_clear(__gen_e_acsl_);
- __gmpq_clear(__gen_e_acsl__2);
return;
}
}
diff --git a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
index 79a76e5072ff36d4a82c3117a1502245997c1ce1..603bb0736371a1433b57909d540fc680df08b111 100644
--- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
@@ -28,7 +28,7 @@
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:82: Warning:
- E-ACSL construct `logic functions with no definition nor reads clause'
+ E-ACSL construct `predicate with no definition nor reads clause'
is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:82: Warning:
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
index 7ac62ea8423fbba17d74651d7e521c862099f2b8..33fc270fbf28281dcc2a2ae460b83b6a31648ae2 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
@@ -1,6 +1,7 @@
[e-acsl] beginning translation.
[e-acsl] tests/gmp/cast.i:23: Warning:
- E-ACSL construct `R to Int' is not yet supported. Ignoring annotation.
+ E-ACSL construct `reals: cast from R to Z' is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_let.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_let.c
index 09ec8b4b6a9d92bee0ab1394102ea70ad26b73e4..33945c99959a19ca4e19697417b5ab475b0bf7d6 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_let.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_let.c
@@ -92,19 +92,10 @@ int main(void)
__e_acsl_full_init((void *)(& f));
/*@ assert \let u = f; u ≡ f; */
{
- __e_acsl_mpq_t __gen_e_acsl_u_10;
- __e_acsl_mpq_t __gen_e_acsl_;
- int __gen_e_acsl_eq;
- __gmpq_init(__gen_e_acsl_u_10);
- __gmpq_set_d(__gen_e_acsl_u_10,(double)f);
- __gmpq_init(__gen_e_acsl_);
- __gmpq_set_d(__gen_e_acsl_,(double)f);
- __gen_e_acsl_eq = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_u_10),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
- (char *)"\\let u = f; u == f",27);
- __gmpq_clear(__gen_e_acsl_u_10);
- __gmpq_clear(__gen_e_acsl_);
+ float __gen_e_acsl_u_10;
+ __gen_e_acsl_u_10 = f;
+ __e_acsl_assert(__gen_e_acsl_u_10 == f,(char *)"Assertion",
+ (char *)"main",(char *)"\\let u = f; u == f",27);
}
int t[4] = {1, 2, 3, 4};
/*@ assert \let u = &t[1]; 1 ≡ 1; */
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c
index d2eb693da9f9d5ebca059faf87aad3622b79fd6d..111063ef2ab67bf20e648ebee2ccb5dcfcac3202 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c
@@ -206,40 +206,37 @@ int main(void)
__e_acsl_full_init((void *)(& f));
/*@ assert \let u = f; u ≡ f; */
{
- __e_acsl_mpq_t __gen_e_acsl_u_14;
- __e_acsl_mpq_t __gen_e_acsl__10;
- int __gen_e_acsl_eq_4;
- __gmpq_init(__gen_e_acsl_u_14);
- __gmpq_set_d(__gen_e_acsl_u_14,(double)f);
- __gmpq_init(__gen_e_acsl__10);
- __gmpq_set_d(__gen_e_acsl__10,(double)f);
- __gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_u_14),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__10));
- __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
+ float __gen_e_acsl_u_14;
+ __gen_e_acsl_u_14 = f;
+ __e_acsl_assert(__gen_e_acsl_u_14 == f,(char *)"Assertion",
(char *)"main",(char *)"\\let u = f; u == f",27);
- __gmpq_clear(__gen_e_acsl_u_14);
- __gmpq_clear(__gen_e_acsl__10);
}
int t[4] = {1, 2, 3, 4};
/*@ assert \let u = &t[1]; 1 ≡ 1; */
{
int * /*[4]*/ __gen_e_acsl_u_15;
- __e_acsl_mpz_t __gen_e_acsl__11;
- int __gen_e_acsl_eq_5;
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ int __gen_e_acsl_eq_4;
__gen_e_acsl_u_15 = & t[1];
- __gmpz_init_set_si(__gen_e_acsl__11,1L);
- __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__11),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
- __e_acsl_assert(__gen_e_acsl_eq_5 == 0,(char *)"Assertion",
+ __gmpz_init_set_si(__gen_e_acsl__10,1L);
+ __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+ __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
(char *)"main",(char *)"\\let u = &t[1]; 1 == 1",30);
- __gmpz_clear(__gen_e_acsl__11);
+ __gmpz_clear(__gen_e_acsl__10);
}
/*@ assert (\let u = &t[1]; 1) ≡ 1; */
{
int * /*[4]*/ __gen_e_acsl_u_16;
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ int __gen_e_acsl_eq_5;
__gen_e_acsl_u_16 = & t[1];
- __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
- (char *)"(\\let u = &t[1]; 1) == 1",32);
+ __gmpz_init_set_si(__gen_e_acsl__11,1L);
+ __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__11),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ __e_acsl_assert(__gen_e_acsl_eq_5 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"(\\let u = &t[1]; 1) == 1",32);
+ __gmpz_clear(__gen_e_acsl__11);
}
struct __anonstruct_r_1 r = {.x = 1, .y = 2};
__e_acsl_store_block((void *)(& r),(size_t)8);
@@ -273,9 +270,18 @@ int main(void)
/*@ assert (\let u = s; u.x) > 0; */
{
union __anonunion_s_2 __gen_e_acsl_u_18;
+ __e_acsl_mpz_t __gen_e_acsl__15;
+ __e_acsl_mpz_t __gen_e_acsl__16;
+ int __gen_e_acsl_gt_3;
__gen_e_acsl_u_18 = s;
- __e_acsl_assert(__gen_e_acsl_u_18.x > 0,(char *)"Assertion",
- (char *)"main",(char *)"(\\let u = s; u.x) > 0",39);
+ __gmpz_init_set_si(__gen_e_acsl__15,(long)__gen_e_acsl_u_18.x);
+ __gmpz_init_set_si(__gen_e_acsl__16,0L);
+ __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__15),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
+ __e_acsl_assert(__gen_e_acsl_gt_3 > 0,(char *)"Assertion",(char *)"main",
+ (char *)"(\\let u = s; u.x) > 0",39);
+ __gmpz_clear(__gen_e_acsl__15);
+ __gmpz_clear(__gen_e_acsl__16);
}
__retres = 0;
__e_acsl_delete_block((void *)(& r));
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_reals.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_reals.c
index 7627bd75e465e994363437329d9248bf68129f77..3033a792d26c9d50af66c5fa15d517a101cb1fbe 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_reals.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_reals.c
@@ -28,7 +28,7 @@ int main(void)
__gmpq_init(__gen_e_acsl_);
__gmpq_set_str(__gen_e_acsl_,"3",10);
__gmpq_init(__gen_e_acsl__2);
- __gmpq_set_str(__gen_e_acsl__2,"15/10",10);
+ __gmpq_set_d(__gen_e_acsl__2,1.5);
__gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__2));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
@@ -40,151 +40,144 @@ int main(void)
{
__e_acsl_mpq_t __gen_e_acsl__3;
__e_acsl_mpq_t __gen_e_acsl__4;
+ __e_acsl_mpq_t __gen_e_acsl__5;
__e_acsl_mpq_t __gen_e_acsl_add;
int __gen_e_acsl_eq;
__gmpq_init(__gen_e_acsl__3);
__gmpq_set_str(__gen_e_acsl__3,"3",10);
__gmpq_init(__gen_e_acsl__4);
- __gmpq_set_str(__gen_e_acsl__4,"15/10",10);
+ __gmpq_set_d(__gen_e_acsl__4,1.5);
+ __gmpq_init(__gen_e_acsl__5);
+ __gmpq_set_d(__gen_e_acsl__5,1.5);
__gmpq_init(__gen_e_acsl_add);
__gmpq_add(__gen_e_acsl_add,
(__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__4));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
__gen_e_acsl_eq = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__3),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
(char *)"3 == 1.5 + 1.5",15);
__gmpq_clear(__gen_e_acsl__3);
__gmpq_clear(__gen_e_acsl__4);
+ __gmpq_clear(__gen_e_acsl__5);
__gmpq_clear(__gen_e_acsl_add);
}
/*@ assert 0.1 ≡ 0.1; */
{
- __e_acsl_mpq_t __gen_e_acsl__5;
+ __e_acsl_mpq_t __gen_e_acsl__6;
int __gen_e_acsl_eq_2;
- __gmpq_init(__gen_e_acsl__5);
- __gmpq_set_str(__gen_e_acsl__5,"01/10",10);
- __gen_e_acsl_eq_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__5),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
+ __gmpq_init(__gen_e_acsl__6);
+ __gmpq_set_str(__gen_e_acsl__6,"01/10",10);
+ __gen_e_acsl_eq_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__6),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__6));
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
(char *)"main",(char *)"0.1 == 0.1",16);
- __gmpq_clear(__gen_e_acsl__5);
+ __gmpq_clear(__gen_e_acsl__6);
}
/*@ assert (double)0.1 ≢ 0.1; */
{
- __e_acsl_mpq_t __gen_e_acsl__6;
- double __gen_e_acsl_cast;
__e_acsl_mpq_t __gen_e_acsl__7;
+ double __gen_e_acsl__8;
+ __e_acsl_mpq_t __gen_e_acsl__9;
int __gen_e_acsl_ne_2;
- __gmpq_init(__gen_e_acsl__6);
- __gmpq_set_str(__gen_e_acsl__6,"01/10",10);
- __gen_e_acsl_cast = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__6));
__gmpq_init(__gen_e_acsl__7);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast); */
- __gmpq_set_d(__gen_e_acsl__7,__gen_e_acsl_cast);
- __gen_e_acsl_ne_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__7),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__6));
+ __gmpq_set_str(__gen_e_acsl__7,"01/10",10);
+ __gen_e_acsl__8 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__7));
+ __gmpq_init(__gen_e_acsl__9);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__8); */
+ __gmpq_set_d(__gen_e_acsl__9,__gen_e_acsl__8);
+ __gen_e_acsl_ne_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__9),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__7));
__e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion",
(char *)"main",(char *)"(double)0.1 != 0.1",17);
- __gmpq_clear(__gen_e_acsl__6);
__gmpq_clear(__gen_e_acsl__7);
+ __gmpq_clear(__gen_e_acsl__9);
}
/*@ assert (float)0.1 ≢ (double)0.1; */
{
- __e_acsl_mpq_t __gen_e_acsl__8;
- double __gen_e_acsl_cast_2;
- double __gen_e_acsl_cast_3;
- __e_acsl_mpq_t __gen_e_acsl__9;
__e_acsl_mpq_t __gen_e_acsl__10;
- int __gen_e_acsl_ne_3;
- __gmpq_init(__gen_e_acsl__8);
- __gmpq_set_str(__gen_e_acsl__8,"01/10",10);
- __gen_e_acsl_cast_2 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
- __gen_e_acsl_cast_3 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
- __gmpq_init(__gen_e_acsl__9);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast_2); */
- /*@ assert
- Eva: is_nan_or_infinite: \is_finite((float)__gen_e_acsl_cast_2);
- */
- __gmpq_set_d(__gen_e_acsl__9,(double)((float)__gen_e_acsl_cast_2));
+ double __gen_e_acsl__11;
+ double __gen_e_acsl__12;
__gmpq_init(__gen_e_acsl__10);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast_3); */
- __gmpq_set_d(__gen_e_acsl__10,__gen_e_acsl_cast_3);
- __gen_e_acsl_ne_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__9),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__10));
- __e_acsl_assert(__gen_e_acsl_ne_3 != 0,(char *)"Assertion",
- (char *)"main",(char *)"(float)0.1 != (double)0.1",18);
- __gmpq_clear(__gen_e_acsl__8);
- __gmpq_clear(__gen_e_acsl__9);
+ __gmpq_set_str(__gen_e_acsl__10,"01/10",10);
+ __gen_e_acsl__11 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__10));
+ __gen_e_acsl__12 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__10));
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__11); */
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__12); */
+ /*@ assert Eva: is_nan_or_infinite: \is_finite((float)__gen_e_acsl__11);
+ */
+ __e_acsl_assert((double)((float)__gen_e_acsl__11) != __gen_e_acsl__12,
+ (char *)"Assertion",(char *)"main",
+ (char *)"(float)0.1 != (double)0.1",18);
__gmpq_clear(__gen_e_acsl__10);
}
/*@ assert (double)1.1 ≢ 1 + 0.1; */
{
- __e_acsl_mpq_t __gen_e_acsl__11;
- double __gen_e_acsl_cast_4;
- __e_acsl_mpq_t __gen_e_acsl__12;
__e_acsl_mpq_t __gen_e_acsl__13;
+ double __gen_e_acsl__14;
+ __e_acsl_mpq_t __gen_e_acsl__15;
+ __e_acsl_mpq_t __gen_e_acsl__16;
__e_acsl_mpq_t __gen_e_acsl_add_2;
- __e_acsl_mpq_t __gen_e_acsl__14;
- int __gen_e_acsl_ne_4;
- __gmpq_init(__gen_e_acsl__11);
- __gmpq_set_str(__gen_e_acsl__11,"11/10",10);
- __gen_e_acsl_cast_4 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__11));
- __gmpq_init(__gen_e_acsl__12);
- __gmpq_set_str(__gen_e_acsl__12,"1",10);
+ __e_acsl_mpq_t __gen_e_acsl__17;
+ int __gen_e_acsl_ne_3;
__gmpq_init(__gen_e_acsl__13);
- __gmpq_set_str(__gen_e_acsl__13,"01/10",10);
+ __gmpq_set_str(__gen_e_acsl__13,"11/10",10);
+ __gen_e_acsl__14 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__13));
+ __gmpq_init(__gen_e_acsl__15);
+ __gmpq_set_str(__gen_e_acsl__15,"1",10);
+ __gmpq_init(__gen_e_acsl__16);
+ __gmpq_set_str(__gen_e_acsl__16,"01/10",10);
__gmpq_init(__gen_e_acsl_add_2);
__gmpq_add(__gen_e_acsl_add_2,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__12),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__13));
- __gmpq_init(__gen_e_acsl__14);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast_4); */
- __gmpq_set_d(__gen_e_acsl__14,__gen_e_acsl_cast_4);
- __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__14),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__15),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__16));
+ __gmpq_init(__gen_e_acsl__17);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__14); */
+ __gmpq_set_d(__gen_e_acsl__17,__gen_e_acsl__14);
+ __gen_e_acsl_ne_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__17),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2));
- __e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_ne_3 != 0,(char *)"Assertion",
(char *)"main",(char *)"(double)1.1 != 1 + 0.1",19);
- __gmpq_clear(__gen_e_acsl__11);
- __gmpq_clear(__gen_e_acsl__12);
__gmpq_clear(__gen_e_acsl__13);
+ __gmpq_clear(__gen_e_acsl__15);
+ __gmpq_clear(__gen_e_acsl__16);
__gmpq_clear(__gen_e_acsl_add_2);
- __gmpq_clear(__gen_e_acsl__14);
+ __gmpq_clear(__gen_e_acsl__17);
}
/*@ assert 1 + 0.1 ≡ 2 - 0.9; */
{
- __e_acsl_mpq_t __gen_e_acsl__15;
- __e_acsl_mpq_t __gen_e_acsl__16;
- __e_acsl_mpq_t __gen_e_acsl_add_3;
- __e_acsl_mpq_t __gen_e_acsl__17;
__e_acsl_mpq_t __gen_e_acsl__18;
+ __e_acsl_mpq_t __gen_e_acsl__19;
+ __e_acsl_mpq_t __gen_e_acsl_add_3;
+ __e_acsl_mpq_t __gen_e_acsl__20;
+ __e_acsl_mpq_t __gen_e_acsl__21;
__e_acsl_mpq_t __gen_e_acsl_sub;
int __gen_e_acsl_eq_3;
- __gmpq_init(__gen_e_acsl__15);
- __gmpq_set_str(__gen_e_acsl__15,"1",10);
- __gmpq_init(__gen_e_acsl__16);
- __gmpq_set_str(__gen_e_acsl__16,"01/10",10);
+ __gmpq_init(__gen_e_acsl__18);
+ __gmpq_set_str(__gen_e_acsl__18,"1",10);
+ __gmpq_init(__gen_e_acsl__19);
+ __gmpq_set_str(__gen_e_acsl__19,"01/10",10);
__gmpq_init(__gen_e_acsl_add_3);
__gmpq_add(__gen_e_acsl_add_3,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__15),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__16));
- __gmpq_init(__gen_e_acsl__17);
- __gmpq_set_str(__gen_e_acsl__17,"2",10);
- __gmpq_init(__gen_e_acsl__18);
- __gmpq_set_str(__gen_e_acsl__18,"09/10",10);
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__18),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__19));
+ __gmpq_init(__gen_e_acsl__20);
+ __gmpq_set_str(__gen_e_acsl__20,"2",10);
+ __gmpq_init(__gen_e_acsl__21);
+ __gmpq_set_str(__gen_e_acsl__21,"09/10",10);
__gmpq_init(__gen_e_acsl_sub);
__gmpq_sub(__gen_e_acsl_sub,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__17),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__18));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__20),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__21));
__gen_e_acsl_eq_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_add_3),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_sub));
__e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
(char *)"main",(char *)"1 + 0.1 == 2 - 0.9",20);
- __gmpq_clear(__gen_e_acsl__15);
- __gmpq_clear(__gen_e_acsl__16);
- __gmpq_clear(__gen_e_acsl_add_3);
- __gmpq_clear(__gen_e_acsl__17);
__gmpq_clear(__gen_e_acsl__18);
+ __gmpq_clear(__gen_e_acsl__19);
+ __gmpq_clear(__gen_e_acsl_add_3);
+ __gmpq_clear(__gen_e_acsl__20);
+ __gmpq_clear(__gen_e_acsl__21);
__gmpq_clear(__gen_e_acsl_sub);
}
float x = 0.2f;
@@ -193,84 +186,84 @@ int main(void)
/*@ assert sum ≢ x * y; */
{
__e_acsl_mpq_t __gen_e_acsl_y;
- __e_acsl_mpq_t __gen_e_acsl__19;
+ __e_acsl_mpq_t __gen_e_acsl__22;
__e_acsl_mpq_t __gen_e_acsl_mul;
- __e_acsl_mpq_t __gen_e_acsl__20;
- int __gen_e_acsl_ne_5;
+ __e_acsl_mpq_t __gen_e_acsl__23;
+ int __gen_e_acsl_ne_4;
__gmpq_init(__gen_e_acsl_y);
__gmpq_set_d(__gen_e_acsl_y,(double)y);
- __gmpq_init(__gen_e_acsl__19);
- __gmpq_set_d(__gen_e_acsl__19,(double)x);
+ __gmpq_init(__gen_e_acsl__22);
+ __gmpq_set_d(__gen_e_acsl__22,(double)x);
__gmpq_init(__gen_e_acsl_mul);
__gmpq_mul(__gen_e_acsl_mul,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__19),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__22),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_y));
- __gmpq_init(__gen_e_acsl__20);
- __gmpq_set_d(__gen_e_acsl__20,(double)sum);
- __gen_e_acsl_ne_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__20),
+ __gmpq_init(__gen_e_acsl__23);
+ __gmpq_set_d(__gen_e_acsl__23,(double)sum);
+ __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__23),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_mul));
- __e_acsl_assert(__gen_e_acsl_ne_5 != 0,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion",
(char *)"main",(char *)"sum != x * y",24);
__gmpq_clear(__gen_e_acsl_y);
- __gmpq_clear(__gen_e_acsl__19);
+ __gmpq_clear(__gen_e_acsl__22);
__gmpq_clear(__gen_e_acsl_mul);
- __gmpq_clear(__gen_e_acsl__20);
+ __gmpq_clear(__gen_e_acsl__23);
}
/*@ assert \let n = 1; 4 ≡ n + 3.0; */
{
int __gen_e_acsl_n;
- __e_acsl_mpq_t __gen_e_acsl__21;
- __e_acsl_mpq_t __gen_e_acsl__22;
- __e_acsl_mpq_t __gen_e_acsl__23;
+ __e_acsl_mpq_t __gen_e_acsl__24;
+ __e_acsl_mpq_t __gen_e_acsl__25;
+ __e_acsl_mpq_t __gen_e_acsl__26;
__e_acsl_mpq_t __gen_e_acsl_add_4;
int __gen_e_acsl_eq_4;
__gen_e_acsl_n = 1;
- __gmpq_init(__gen_e_acsl__21);
- __gmpq_set_str(__gen_e_acsl__21,"4",10);
- __gmpq_init(__gen_e_acsl__22);
- __gmpq_set_str(__gen_e_acsl__22,"30/10",10);
- __gmpq_init(__gen_e_acsl__23);
- __gmpq_set_si(__gen_e_acsl__23,(long)__gen_e_acsl_n);
+ __gmpq_init(__gen_e_acsl__24);
+ __gmpq_set_str(__gen_e_acsl__24,"4",10);
+ __gmpq_init(__gen_e_acsl__25);
+ __gmpq_set_d(__gen_e_acsl__25,3.);
+ __gmpq_init(__gen_e_acsl__26);
+ __gmpq_set_si(__gen_e_acsl__26,(long)__gen_e_acsl_n);
__gmpq_init(__gen_e_acsl_add_4);
__gmpq_add(__gen_e_acsl_add_4,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__23),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__22));
- __gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__21),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__26),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__25));
+ __gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_4));
__e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
(char *)"main",(char *)"\\let n = 1; 4 == n + 3.0",25);
- __gmpq_clear(__gen_e_acsl__21);
- __gmpq_clear(__gen_e_acsl__22);
- __gmpq_clear(__gen_e_acsl__23);
+ __gmpq_clear(__gen_e_acsl__24);
+ __gmpq_clear(__gen_e_acsl__25);
+ __gmpq_clear(__gen_e_acsl__26);
__gmpq_clear(__gen_e_acsl_add_4);
}
double d = 0.1;
__gen_e_acsl_avg(4.3,11.7);
/*@ assert 1.1d ≢ 1 + 0.1; */
{
- __e_acsl_mpq_t __gen_e_acsl__24;
- __e_acsl_mpq_t __gen_e_acsl__25;
- __e_acsl_mpq_t __gen_e_acsl__26;
+ __e_acsl_mpq_t __gen_e_acsl__27;
+ __e_acsl_mpq_t __gen_e_acsl__28;
__e_acsl_mpq_t __gen_e_acsl_add_5;
- int __gen_e_acsl_ne_6;
- __gmpq_init(__gen_e_acsl__24);
- __gmpq_set_str(__gen_e_acsl__24,"1.1d",10);
- __gmpq_init(__gen_e_acsl__25);
- __gmpq_set_str(__gen_e_acsl__25,"1",10);
- __gmpq_init(__gen_e_acsl__26);
- __gmpq_set_str(__gen_e_acsl__26,"01/10",10);
+ __e_acsl_mpq_t __gen_e_acsl__29;
+ int __gen_e_acsl_ne_5;
+ __gmpq_init(__gen_e_acsl__27);
+ __gmpq_set_str(__gen_e_acsl__27,"1",10);
+ __gmpq_init(__gen_e_acsl__28);
+ __gmpq_set_str(__gen_e_acsl__28,"01/10",10);
__gmpq_init(__gen_e_acsl_add_5);
__gmpq_add(__gen_e_acsl_add_5,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__25),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__26));
- __gen_e_acsl_ne_6 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__27),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__28));
+ __gmpq_init(__gen_e_acsl__29);
+ __gmpq_set_d(__gen_e_acsl__29,1.1);
+ __gen_e_acsl_ne_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__29),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_5));
- __e_acsl_assert(__gen_e_acsl_ne_6 != 0,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_ne_5 != 0,(char *)"Assertion",
(char *)"main",(char *)"1.1d != 1 + 0.1",31);
- __gmpq_clear(__gen_e_acsl__24);
- __gmpq_clear(__gen_e_acsl__25);
- __gmpq_clear(__gen_e_acsl__26);
+ __gmpq_clear(__gen_e_acsl__27);
+ __gmpq_clear(__gen_e_acsl__28);
__gmpq_clear(__gen_e_acsl_add_5);
+ __gmpq_clear(__gen_e_acsl__29);
}
__retres = 0;
return __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_reals2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_reals2.c
index 7627bd75e465e994363437329d9248bf68129f77..3033a792d26c9d50af66c5fa15d517a101cb1fbe 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_reals2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_reals2.c
@@ -28,7 +28,7 @@ int main(void)
__gmpq_init(__gen_e_acsl_);
__gmpq_set_str(__gen_e_acsl_,"3",10);
__gmpq_init(__gen_e_acsl__2);
- __gmpq_set_str(__gen_e_acsl__2,"15/10",10);
+ __gmpq_set_d(__gen_e_acsl__2,1.5);
__gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__2));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
@@ -40,151 +40,144 @@ int main(void)
{
__e_acsl_mpq_t __gen_e_acsl__3;
__e_acsl_mpq_t __gen_e_acsl__4;
+ __e_acsl_mpq_t __gen_e_acsl__5;
__e_acsl_mpq_t __gen_e_acsl_add;
int __gen_e_acsl_eq;
__gmpq_init(__gen_e_acsl__3);
__gmpq_set_str(__gen_e_acsl__3,"3",10);
__gmpq_init(__gen_e_acsl__4);
- __gmpq_set_str(__gen_e_acsl__4,"15/10",10);
+ __gmpq_set_d(__gen_e_acsl__4,1.5);
+ __gmpq_init(__gen_e_acsl__5);
+ __gmpq_set_d(__gen_e_acsl__5,1.5);
__gmpq_init(__gen_e_acsl_add);
__gmpq_add(__gen_e_acsl_add,
(__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__4));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
__gen_e_acsl_eq = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__3),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
(char *)"3 == 1.5 + 1.5",15);
__gmpq_clear(__gen_e_acsl__3);
__gmpq_clear(__gen_e_acsl__4);
+ __gmpq_clear(__gen_e_acsl__5);
__gmpq_clear(__gen_e_acsl_add);
}
/*@ assert 0.1 ≡ 0.1; */
{
- __e_acsl_mpq_t __gen_e_acsl__5;
+ __e_acsl_mpq_t __gen_e_acsl__6;
int __gen_e_acsl_eq_2;
- __gmpq_init(__gen_e_acsl__5);
- __gmpq_set_str(__gen_e_acsl__5,"01/10",10);
- __gen_e_acsl_eq_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__5),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
+ __gmpq_init(__gen_e_acsl__6);
+ __gmpq_set_str(__gen_e_acsl__6,"01/10",10);
+ __gen_e_acsl_eq_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__6),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__6));
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
(char *)"main",(char *)"0.1 == 0.1",16);
- __gmpq_clear(__gen_e_acsl__5);
+ __gmpq_clear(__gen_e_acsl__6);
}
/*@ assert (double)0.1 ≢ 0.1; */
{
- __e_acsl_mpq_t __gen_e_acsl__6;
- double __gen_e_acsl_cast;
__e_acsl_mpq_t __gen_e_acsl__7;
+ double __gen_e_acsl__8;
+ __e_acsl_mpq_t __gen_e_acsl__9;
int __gen_e_acsl_ne_2;
- __gmpq_init(__gen_e_acsl__6);
- __gmpq_set_str(__gen_e_acsl__6,"01/10",10);
- __gen_e_acsl_cast = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__6));
__gmpq_init(__gen_e_acsl__7);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast); */
- __gmpq_set_d(__gen_e_acsl__7,__gen_e_acsl_cast);
- __gen_e_acsl_ne_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__7),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__6));
+ __gmpq_set_str(__gen_e_acsl__7,"01/10",10);
+ __gen_e_acsl__8 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__7));
+ __gmpq_init(__gen_e_acsl__9);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__8); */
+ __gmpq_set_d(__gen_e_acsl__9,__gen_e_acsl__8);
+ __gen_e_acsl_ne_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__9),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__7));
__e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion",
(char *)"main",(char *)"(double)0.1 != 0.1",17);
- __gmpq_clear(__gen_e_acsl__6);
__gmpq_clear(__gen_e_acsl__7);
+ __gmpq_clear(__gen_e_acsl__9);
}
/*@ assert (float)0.1 ≢ (double)0.1; */
{
- __e_acsl_mpq_t __gen_e_acsl__8;
- double __gen_e_acsl_cast_2;
- double __gen_e_acsl_cast_3;
- __e_acsl_mpq_t __gen_e_acsl__9;
__e_acsl_mpq_t __gen_e_acsl__10;
- int __gen_e_acsl_ne_3;
- __gmpq_init(__gen_e_acsl__8);
- __gmpq_set_str(__gen_e_acsl__8,"01/10",10);
- __gen_e_acsl_cast_2 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
- __gen_e_acsl_cast_3 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
- __gmpq_init(__gen_e_acsl__9);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast_2); */
- /*@ assert
- Eva: is_nan_or_infinite: \is_finite((float)__gen_e_acsl_cast_2);
- */
- __gmpq_set_d(__gen_e_acsl__9,(double)((float)__gen_e_acsl_cast_2));
+ double __gen_e_acsl__11;
+ double __gen_e_acsl__12;
__gmpq_init(__gen_e_acsl__10);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast_3); */
- __gmpq_set_d(__gen_e_acsl__10,__gen_e_acsl_cast_3);
- __gen_e_acsl_ne_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__9),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__10));
- __e_acsl_assert(__gen_e_acsl_ne_3 != 0,(char *)"Assertion",
- (char *)"main",(char *)"(float)0.1 != (double)0.1",18);
- __gmpq_clear(__gen_e_acsl__8);
- __gmpq_clear(__gen_e_acsl__9);
+ __gmpq_set_str(__gen_e_acsl__10,"01/10",10);
+ __gen_e_acsl__11 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__10));
+ __gen_e_acsl__12 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__10));
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__11); */
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__12); */
+ /*@ assert Eva: is_nan_or_infinite: \is_finite((float)__gen_e_acsl__11);
+ */
+ __e_acsl_assert((double)((float)__gen_e_acsl__11) != __gen_e_acsl__12,
+ (char *)"Assertion",(char *)"main",
+ (char *)"(float)0.1 != (double)0.1",18);
__gmpq_clear(__gen_e_acsl__10);
}
/*@ assert (double)1.1 ≢ 1 + 0.1; */
{
- __e_acsl_mpq_t __gen_e_acsl__11;
- double __gen_e_acsl_cast_4;
- __e_acsl_mpq_t __gen_e_acsl__12;
__e_acsl_mpq_t __gen_e_acsl__13;
+ double __gen_e_acsl__14;
+ __e_acsl_mpq_t __gen_e_acsl__15;
+ __e_acsl_mpq_t __gen_e_acsl__16;
__e_acsl_mpq_t __gen_e_acsl_add_2;
- __e_acsl_mpq_t __gen_e_acsl__14;
- int __gen_e_acsl_ne_4;
- __gmpq_init(__gen_e_acsl__11);
- __gmpq_set_str(__gen_e_acsl__11,"11/10",10);
- __gen_e_acsl_cast_4 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__11));
- __gmpq_init(__gen_e_acsl__12);
- __gmpq_set_str(__gen_e_acsl__12,"1",10);
+ __e_acsl_mpq_t __gen_e_acsl__17;
+ int __gen_e_acsl_ne_3;
__gmpq_init(__gen_e_acsl__13);
- __gmpq_set_str(__gen_e_acsl__13,"01/10",10);
+ __gmpq_set_str(__gen_e_acsl__13,"11/10",10);
+ __gen_e_acsl__14 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__13));
+ __gmpq_init(__gen_e_acsl__15);
+ __gmpq_set_str(__gen_e_acsl__15,"1",10);
+ __gmpq_init(__gen_e_acsl__16);
+ __gmpq_set_str(__gen_e_acsl__16,"01/10",10);
__gmpq_init(__gen_e_acsl_add_2);
__gmpq_add(__gen_e_acsl_add_2,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__12),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__13));
- __gmpq_init(__gen_e_acsl__14);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast_4); */
- __gmpq_set_d(__gen_e_acsl__14,__gen_e_acsl_cast_4);
- __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__14),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__15),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__16));
+ __gmpq_init(__gen_e_acsl__17);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__14); */
+ __gmpq_set_d(__gen_e_acsl__17,__gen_e_acsl__14);
+ __gen_e_acsl_ne_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__17),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2));
- __e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_ne_3 != 0,(char *)"Assertion",
(char *)"main",(char *)"(double)1.1 != 1 + 0.1",19);
- __gmpq_clear(__gen_e_acsl__11);
- __gmpq_clear(__gen_e_acsl__12);
__gmpq_clear(__gen_e_acsl__13);
+ __gmpq_clear(__gen_e_acsl__15);
+ __gmpq_clear(__gen_e_acsl__16);
__gmpq_clear(__gen_e_acsl_add_2);
- __gmpq_clear(__gen_e_acsl__14);
+ __gmpq_clear(__gen_e_acsl__17);
}
/*@ assert 1 + 0.1 ≡ 2 - 0.9; */
{
- __e_acsl_mpq_t __gen_e_acsl__15;
- __e_acsl_mpq_t __gen_e_acsl__16;
- __e_acsl_mpq_t __gen_e_acsl_add_3;
- __e_acsl_mpq_t __gen_e_acsl__17;
__e_acsl_mpq_t __gen_e_acsl__18;
+ __e_acsl_mpq_t __gen_e_acsl__19;
+ __e_acsl_mpq_t __gen_e_acsl_add_3;
+ __e_acsl_mpq_t __gen_e_acsl__20;
+ __e_acsl_mpq_t __gen_e_acsl__21;
__e_acsl_mpq_t __gen_e_acsl_sub;
int __gen_e_acsl_eq_3;
- __gmpq_init(__gen_e_acsl__15);
- __gmpq_set_str(__gen_e_acsl__15,"1",10);
- __gmpq_init(__gen_e_acsl__16);
- __gmpq_set_str(__gen_e_acsl__16,"01/10",10);
+ __gmpq_init(__gen_e_acsl__18);
+ __gmpq_set_str(__gen_e_acsl__18,"1",10);
+ __gmpq_init(__gen_e_acsl__19);
+ __gmpq_set_str(__gen_e_acsl__19,"01/10",10);
__gmpq_init(__gen_e_acsl_add_3);
__gmpq_add(__gen_e_acsl_add_3,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__15),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__16));
- __gmpq_init(__gen_e_acsl__17);
- __gmpq_set_str(__gen_e_acsl__17,"2",10);
- __gmpq_init(__gen_e_acsl__18);
- __gmpq_set_str(__gen_e_acsl__18,"09/10",10);
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__18),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__19));
+ __gmpq_init(__gen_e_acsl__20);
+ __gmpq_set_str(__gen_e_acsl__20,"2",10);
+ __gmpq_init(__gen_e_acsl__21);
+ __gmpq_set_str(__gen_e_acsl__21,"09/10",10);
__gmpq_init(__gen_e_acsl_sub);
__gmpq_sub(__gen_e_acsl_sub,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__17),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__18));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__20),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__21));
__gen_e_acsl_eq_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_add_3),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_sub));
__e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
(char *)"main",(char *)"1 + 0.1 == 2 - 0.9",20);
- __gmpq_clear(__gen_e_acsl__15);
- __gmpq_clear(__gen_e_acsl__16);
- __gmpq_clear(__gen_e_acsl_add_3);
- __gmpq_clear(__gen_e_acsl__17);
__gmpq_clear(__gen_e_acsl__18);
+ __gmpq_clear(__gen_e_acsl__19);
+ __gmpq_clear(__gen_e_acsl_add_3);
+ __gmpq_clear(__gen_e_acsl__20);
+ __gmpq_clear(__gen_e_acsl__21);
__gmpq_clear(__gen_e_acsl_sub);
}
float x = 0.2f;
@@ -193,84 +186,84 @@ int main(void)
/*@ assert sum ≢ x * y; */
{
__e_acsl_mpq_t __gen_e_acsl_y;
- __e_acsl_mpq_t __gen_e_acsl__19;
+ __e_acsl_mpq_t __gen_e_acsl__22;
__e_acsl_mpq_t __gen_e_acsl_mul;
- __e_acsl_mpq_t __gen_e_acsl__20;
- int __gen_e_acsl_ne_5;
+ __e_acsl_mpq_t __gen_e_acsl__23;
+ int __gen_e_acsl_ne_4;
__gmpq_init(__gen_e_acsl_y);
__gmpq_set_d(__gen_e_acsl_y,(double)y);
- __gmpq_init(__gen_e_acsl__19);
- __gmpq_set_d(__gen_e_acsl__19,(double)x);
+ __gmpq_init(__gen_e_acsl__22);
+ __gmpq_set_d(__gen_e_acsl__22,(double)x);
__gmpq_init(__gen_e_acsl_mul);
__gmpq_mul(__gen_e_acsl_mul,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__19),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__22),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_y));
- __gmpq_init(__gen_e_acsl__20);
- __gmpq_set_d(__gen_e_acsl__20,(double)sum);
- __gen_e_acsl_ne_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__20),
+ __gmpq_init(__gen_e_acsl__23);
+ __gmpq_set_d(__gen_e_acsl__23,(double)sum);
+ __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__23),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_mul));
- __e_acsl_assert(__gen_e_acsl_ne_5 != 0,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion",
(char *)"main",(char *)"sum != x * y",24);
__gmpq_clear(__gen_e_acsl_y);
- __gmpq_clear(__gen_e_acsl__19);
+ __gmpq_clear(__gen_e_acsl__22);
__gmpq_clear(__gen_e_acsl_mul);
- __gmpq_clear(__gen_e_acsl__20);
+ __gmpq_clear(__gen_e_acsl__23);
}
/*@ assert \let n = 1; 4 ≡ n + 3.0; */
{
int __gen_e_acsl_n;
- __e_acsl_mpq_t __gen_e_acsl__21;
- __e_acsl_mpq_t __gen_e_acsl__22;
- __e_acsl_mpq_t __gen_e_acsl__23;
+ __e_acsl_mpq_t __gen_e_acsl__24;
+ __e_acsl_mpq_t __gen_e_acsl__25;
+ __e_acsl_mpq_t __gen_e_acsl__26;
__e_acsl_mpq_t __gen_e_acsl_add_4;
int __gen_e_acsl_eq_4;
__gen_e_acsl_n = 1;
- __gmpq_init(__gen_e_acsl__21);
- __gmpq_set_str(__gen_e_acsl__21,"4",10);
- __gmpq_init(__gen_e_acsl__22);
- __gmpq_set_str(__gen_e_acsl__22,"30/10",10);
- __gmpq_init(__gen_e_acsl__23);
- __gmpq_set_si(__gen_e_acsl__23,(long)__gen_e_acsl_n);
+ __gmpq_init(__gen_e_acsl__24);
+ __gmpq_set_str(__gen_e_acsl__24,"4",10);
+ __gmpq_init(__gen_e_acsl__25);
+ __gmpq_set_d(__gen_e_acsl__25,3.);
+ __gmpq_init(__gen_e_acsl__26);
+ __gmpq_set_si(__gen_e_acsl__26,(long)__gen_e_acsl_n);
__gmpq_init(__gen_e_acsl_add_4);
__gmpq_add(__gen_e_acsl_add_4,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__23),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__22));
- __gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__21),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__26),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__25));
+ __gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_4));
__e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
(char *)"main",(char *)"\\let n = 1; 4 == n + 3.0",25);
- __gmpq_clear(__gen_e_acsl__21);
- __gmpq_clear(__gen_e_acsl__22);
- __gmpq_clear(__gen_e_acsl__23);
+ __gmpq_clear(__gen_e_acsl__24);
+ __gmpq_clear(__gen_e_acsl__25);
+ __gmpq_clear(__gen_e_acsl__26);
__gmpq_clear(__gen_e_acsl_add_4);
}
double d = 0.1;
__gen_e_acsl_avg(4.3,11.7);
/*@ assert 1.1d ≢ 1 + 0.1; */
{
- __e_acsl_mpq_t __gen_e_acsl__24;
- __e_acsl_mpq_t __gen_e_acsl__25;
- __e_acsl_mpq_t __gen_e_acsl__26;
+ __e_acsl_mpq_t __gen_e_acsl__27;
+ __e_acsl_mpq_t __gen_e_acsl__28;
__e_acsl_mpq_t __gen_e_acsl_add_5;
- int __gen_e_acsl_ne_6;
- __gmpq_init(__gen_e_acsl__24);
- __gmpq_set_str(__gen_e_acsl__24,"1.1d",10);
- __gmpq_init(__gen_e_acsl__25);
- __gmpq_set_str(__gen_e_acsl__25,"1",10);
- __gmpq_init(__gen_e_acsl__26);
- __gmpq_set_str(__gen_e_acsl__26,"01/10",10);
+ __e_acsl_mpq_t __gen_e_acsl__29;
+ int __gen_e_acsl_ne_5;
+ __gmpq_init(__gen_e_acsl__27);
+ __gmpq_set_str(__gen_e_acsl__27,"1",10);
+ __gmpq_init(__gen_e_acsl__28);
+ __gmpq_set_str(__gen_e_acsl__28,"01/10",10);
__gmpq_init(__gen_e_acsl_add_5);
__gmpq_add(__gen_e_acsl_add_5,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__25),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__26));
- __gen_e_acsl_ne_6 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__27),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__28));
+ __gmpq_init(__gen_e_acsl__29);
+ __gmpq_set_d(__gen_e_acsl__29,1.1);
+ __gen_e_acsl_ne_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__29),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_5));
- __e_acsl_assert(__gen_e_acsl_ne_6 != 0,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_ne_5 != 0,(char *)"Assertion",
(char *)"main",(char *)"1.1d != 1 + 0.1",31);
- __gmpq_clear(__gen_e_acsl__24);
- __gmpq_clear(__gen_e_acsl__25);
- __gmpq_clear(__gen_e_acsl__26);
+ __gmpq_clear(__gen_e_acsl__27);
+ __gmpq_clear(__gen_e_acsl__28);
__gmpq_clear(__gen_e_acsl_add_5);
+ __gmpq_clear(__gen_e_acsl__29);
}
__retres = 0;
return __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/let.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/let.0.res.oracle
index 2d54fe6c596c255b651eaa4138f31aaf691f0b6d..eb489ce6c2576da5bebb4949ba0e066c54997a77 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/let.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/let.0.res.oracle
@@ -35,12 +35,6 @@
[eva] using specification for function __e_acsl_store_block
[eva] using specification for function __e_acsl_full_init
[eva:alarm] tests/gmp/let.c:27: Warning: assertion got status unknown.
-[eva] using specification for function __gmpq_init
-[eva] using specification for function __gmpq_set_d
-[eva] using specification for function __gmpq_cmp
-[eva:alarm] tests/gmp/let.c:27: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpq_clear
[eva:alarm] tests/gmp/let.c:30: Warning: assertion got status unknown.
[eva] tests/gmp/let.c:32:
cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/let.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/let.1.res.oracle
index bbae66240bf44940b5afced7bde61c5c56967fd0..4ef2a9f67a28af8af5599e60d8657f9d7bc338a3 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/let.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/let.1.res.oracle
@@ -49,24 +49,22 @@
[eva] using specification for function __e_acsl_store_block
[eva] using specification for function __e_acsl_full_init
[eva:alarm] tests/gmp/let.c:27: Warning: assertion got status unknown.
-[eva] using specification for function __gmpq_init
-[eva] using specification for function __gmpq_set_d
-[eva] using specification for function __gmpq_cmp
-[eva:alarm] tests/gmp/let.c:27: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpq_clear
[eva:alarm] tests/gmp/let.c:30: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/let.c:30: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] tests/gmp/let.c:32:
cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
[eva:alarm] tests/gmp/let.c:32: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/let.c:32: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/let.c:35: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/let.c:35: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] tests/gmp/let.c:39:
cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
[eva:alarm] tests/gmp/let.c:39: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/let.c:39: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __e_acsl_delete_block
[eva] using specification for function __e_acsl_memory_clean
[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/reals.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/reals.0.res.oracle
index a1a5dd8416dc57984e6502155398de1c462b9a77..c17cb20a38b2b1165d3aab40dc144b871549f964 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/reals.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/reals.0.res.oracle
@@ -3,6 +3,10 @@
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[e-acsl] beginning translation.
[e-acsl] Warning: R to float: double rounding might cause unsoundness
+[e-acsl] tests/gmp/reals.c:18: Warning:
+ E-ACSL construct `predicate with no definition nor reads clause'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -17,6 +21,7 @@
[eva] using specification for function __e_acsl_memory_init
[eva] using specification for function __gmpq_init
[eva] using specification for function __gmpq_set_str
+[eva] using specification for function __gmpq_set_d
[eva] using specification for function __gmpq_cmp
[eva] using specification for function __e_acsl_assert
[eva:alarm] tests/gmp/reals.c:14: Warning:
@@ -31,21 +36,20 @@
[eva:alarm] tests/gmp/reals.c:17: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_get_d
[eva:alarm] tests/gmp/reals.c:17: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl_cast);
-[eva] using specification for function __gmpq_set_d
+ non-finite double value. assert \is_finite(__gen_e_acsl__8);
[eva:alarm] tests/gmp/reals.c:17: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:18: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl_cast_2);
+ non-finite double value. assert \is_finite(__gen_e_acsl__11);
[eva:alarm] tests/gmp/reals.c:18: Warning:
- non-finite float value. assert \is_finite((float)__gen_e_acsl_cast_2);
+ non-finite double value. assert \is_finite(__gen_e_acsl__12);
[eva:alarm] tests/gmp/reals.c:18: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl_cast_3);
+ non-finite float value. assert \is_finite((float)__gen_e_acsl__11);
[eva:alarm] tests/gmp/reals.c:18: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:19: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:19: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl_cast_4);
+ non-finite double value. assert \is_finite(__gen_e_acsl__14);
[eva:alarm] tests/gmp/reals.c:19: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:20: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/reals.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/reals.1.res.oracle
index a1a5dd8416dc57984e6502155398de1c462b9a77..c17cb20a38b2b1165d3aab40dc144b871549f964 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/reals.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/reals.1.res.oracle
@@ -3,6 +3,10 @@
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[e-acsl] beginning translation.
[e-acsl] Warning: R to float: double rounding might cause unsoundness
+[e-acsl] tests/gmp/reals.c:18: Warning:
+ E-ACSL construct `predicate with no definition nor reads clause'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -17,6 +21,7 @@
[eva] using specification for function __e_acsl_memory_init
[eva] using specification for function __gmpq_init
[eva] using specification for function __gmpq_set_str
+[eva] using specification for function __gmpq_set_d
[eva] using specification for function __gmpq_cmp
[eva] using specification for function __e_acsl_assert
[eva:alarm] tests/gmp/reals.c:14: Warning:
@@ -31,21 +36,20 @@
[eva:alarm] tests/gmp/reals.c:17: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_get_d
[eva:alarm] tests/gmp/reals.c:17: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl_cast);
-[eva] using specification for function __gmpq_set_d
+ non-finite double value. assert \is_finite(__gen_e_acsl__8);
[eva:alarm] tests/gmp/reals.c:17: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:18: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl_cast_2);
+ non-finite double value. assert \is_finite(__gen_e_acsl__11);
[eva:alarm] tests/gmp/reals.c:18: Warning:
- non-finite float value. assert \is_finite((float)__gen_e_acsl_cast_2);
+ non-finite double value. assert \is_finite(__gen_e_acsl__12);
[eva:alarm] tests/gmp/reals.c:18: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl_cast_3);
+ non-finite float value. assert \is_finite((float)__gen_e_acsl__11);
[eva:alarm] tests/gmp/reals.c:18: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:19: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:19: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl_cast_4);
+ non-finite double value. assert \is_finite(__gen_e_acsl__14);
[eva:alarm] tests/gmp/reals.c:19: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:20: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 1aaf8e0276f7d273c2a2696e2fa0a3e96668c5bd..82de0f17f9facdd1fe5605919343de6e351ddab6 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -83,7 +83,6 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
e, env
in
let e, env = match strnum with
- (* TODO RATIONAL: make this matching consistent *)
| Str_Z -> mk_mpz e
| Str_R -> Real.mk_real ~loc ?name e env t_opt
| C_number -> e, env
@@ -149,42 +148,38 @@ let constant_to_exp ~loc t c =
in
match c with
| Integer(n, _repr) ->
- (try
- let ity = Typing.get_number_ty t in
- match ity with
- | Typing.Nan ->
- assert false
- | Typing.Real ->
- (* TODO RATIONAL:
- - is it possible?
- - why converting the integer to a string? *)
+ let ity = Typing.get_number_ty t in
+ (match ity with
+ | Typing.Nan -> assert false
+ | Typing.Real -> Error.not_yet "real number constant"
+ | Typing.Rational -> mk_real (Integer.to_string n)
+ | Typing.Gmpz ->
+ (* too large integer *)
+ Cil.mkString ~loc (Integer.to_string n), Str_Z
+ | Typing.C_float _fkind -> assert false (* TODO RATIONAL *)
+ | Typing.C_integer kind ->
+ let cast = Typing.get_cast t in
+ match cast, kind with
+ | Some ty, (ILongLong | IULongLong) when Gmp.Z.is_t ty ->
+ (* too large integer *)
+ Cil.mkString ~loc (Integer.to_string n), Str_Z
+ | Some ty, _ when Real.is_t ty ->
mk_real (Integer.to_string n)
- | Typing.Gmpz ->
- raise Cil.Not_representable
- | Typing.C_type kind ->
- let cast = Typing.get_cast t in
- match cast, kind with
- (* TODO RATIONAL: why are the two first cases not the same?
- (exception vs builder) *)
- | Some ty, (ILongLong | IULongLong) when Gmp.Z.is_t ty ->
- raise Cil.Not_representable
- | Some ty, (ILongLong | IULongLong) when Real.is_t ty ->
- mk_real (Integer.to_string n)
- | (None | Some _), _ ->
- (* do not keep the initial string representation because the
- generated constant must reflect its type computed by the type
- system. For instance, when translating [INT_MAX+1], we must
- generate a [long long] addition and so [1LL]. If we keep the
- initial string representation, the kind would be ignored in the
- generated code and so [1] would be generated. *)
- Cil.kinteger64 ~loc ~kind n, C_number
- with Cil.Not_representable ->
- (* too big integer *)
- Cil.mkString ~loc (Integer.to_string n), Str_Z)
+ | (None | Some _), _ ->
+ (* do not keep the initial string representation because the generated
+ constant must reflect its type computed by the type system. For
+ instance, when translating [INT_MAX+1], we must generate a [long
+ long] addition and so [1LL]. If we keep the initial string
+ representation, the kind would be ignored in the generated code and
+ so [1] would be generated. *)
+ Cil.kinteger64 ~loc ~kind n, C_number)
| LStr s -> Cil.new_exp ~loc (Const (CStr s)), C_number
| LWStr s -> Cil.new_exp ~loc (Const (CWStr s)), C_number
| LChr c -> Cil.new_exp ~loc (Const (CChr c)), C_number
- | LReal {r_literal=s; r_nearest=_; r_lower=_; r_upper=_} -> mk_real s
+ | LReal lr ->
+ if lr.r_lower = lr.r_upper
+ then Cil.kfloat ~loc FDouble lr.r_nearest, C_number
+ else mk_real lr.r_literal
| LEnum e -> Cil.new_exp ~loc (Const (CEnum e)), C_number
let conditional_to_exp ?(name="if") loc t_opt e1 (e2, env2) (e3, env3) =
@@ -436,14 +431,14 @@ and context_insensitive_term_to_exp kf env t =
Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, C_number, ""
| TBinOp(MinusPP, t1, t2) ->
begin match Typing.get_number_ty t with
- | Typing.C_type _ ->
+ | Typing.C_integer _ ->
let e1, env = term_to_exp kf env t1 in
let e2, env = term_to_exp kf env t2 in
let ty = Typing.get_typ t in
Cil.new_exp ~loc (BinOp(MinusPP, e1, e2, ty)), env, C_number, ""
| Typing.Gmpz ->
not_yet env "pointer subtraction resulting in gmp"
- | Typing.Real | Typing.Nan ->
+ | Typing.(C_float _ | Rational | Real | Nan) ->
assert false
end
| TCastE(ty, t') ->
@@ -497,7 +492,6 @@ and context_insensitive_term_to_exp kf env t =
let e, env =
try
let ty = Typing.typ_of_number_ty param_ty in
- (* TODO RATIONAL: check [Not_a_strnum] *)
add_cast loc env (Some ty) C_number (Some targ) e
with Typing.Not_a_number ->
e, env
@@ -604,7 +598,7 @@ and comparison_to_exp
in
let e2, env = term_to_exp kf env t2 in
match ity with
- | Typing.C_type _ | Typing.Nan ->
+ | Typing.C_integer _ | Typing.C_float _ | Typing.Nan ->
Cil.mkBinOp ~loc bop e1 e2, env
| Typing.Gmpz ->
let _, e, env = Env.new_var
@@ -617,8 +611,10 @@ and comparison_to_exp
[ Misc.mk_call ~loc ~result:(Cil.var v) "__gmpz_cmp" [ e1; e2 ] ])
in
Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
- | Typing.Real ->
+ | Typing.Rational ->
Real.cmp ~loc bop e1 e2 env t_opt
+ | Typing.Real ->
+ Error.not_yet "comparison involving real numbers"
and at_to_exp_no_lscope env t_opt label e =
let stmt = E_acsl_label.get_stmt (Env.get_visitor env) label in
@@ -672,12 +668,14 @@ and env_of_li li kf env loc =
let vi, vi_e, env = Env.Logic_binding.add ~ty env li.l_var_info in
let e, env = term_to_exp kf env t in
let stmt = match Typing.get_number_ty t with
- | Typing.C_type _ | Typing.Nan ->
+ | Typing.(C_integer _ | C_float _ | Nan) ->
Cil.mkStmtOneInstr (Set (Cil.var vi, e, loc))
| Typing.Gmpz ->
Gmp.init_set ~loc (Cil.var vi) vi_e e
- | Typing.Real ->
+ | Typing.Rational ->
Real.init_set ~loc (Cil.var vi) vi_e e
+ | Typing.Real ->
+ Error.not_yet "real number"
in
Env.add_stmt env stmt
@@ -739,8 +737,8 @@ and named_predicate_content_to_exp ?name kf env p =
kf
env
(Logic_const.pand ~loc
- (Logic_const.pimplies ~loc (p1, p2),
- Logic_const.pimplies ~loc (p2, p1)))
+ (Logic_const.pimplies ~loc (p1, p2),
+ Logic_const.pimplies ~loc (p2, p1)))
| Pnot p ->
let e, env = named_predicate_to_exp kf env p in
Cil.new_exp ~loc (UnOp(LNot, e, Cil.intType)), env
@@ -919,11 +917,11 @@ let term_to_exp typ t =
(* infer a context from the given [typ] whenever possible *)
let ctx_of_typ ty =
if Gmp.Z.is_t ty then Typing.gmpz
- else if Real.is_t ty then Typing.real
+ else if Real.is_t ty then Typing.rational
else
match ty with
| TInt(ik, _) -> Typing.ikind ik
- | TFloat _ -> Typing.real
+ | TFloat(fk, _) -> Typing.fkind fk
| _ -> Typing.nan
in
let ctx = Extlib.opt_map ctx_of_typ typ in
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 31e9eb057f2c8dc55ddf1fff1bef64f4ce85fe74..774e0c22d3fe329912e6327df742b28cd3f09f5d 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -37,15 +37,18 @@ let compute_quantif_guards_ref
(******************************************************************************)
type number_ty =
- | C_type of ikind
+ | C_integer of ikind
+ | C_float of fkind
| Gmpz
+ | Rational
| Real
| Nan
-let c_int = C_type IInt
-let ikind ik = C_type ik
+let ikind ik = C_integer ik
+let c_int = ikind IInt
let gmpz = Gmpz
-let real = Real
+let fkind fk = C_float fk
+let rational = Rational
let nan = Nan
module D =
@@ -60,30 +63,44 @@ module D =
if ty1 == ty2 then 0
else
match ty1, ty2 with
- | C_type i1, C_type i2 ->
+ | C_integer i1, C_integer i2 ->
if i1 = i2 then 0
else if Cil.intTypeIncluded i1 i2 then -1 else 1
- | (C_type _ | Gmpz | Real), Nan
- | (C_type _ | Gmpz), Real
- | C_type _, Gmpz ->
+ | C_float f1, C_float f2 ->
+ Stdlib.compare f1 f2
+ | (C_integer _ | C_float _ | Gmpz | Rational | Real), Nan
+ | (C_integer _ | C_float _ | Gmpz | Rational ), Real
+ | (C_integer _ | C_float _ | Gmpz), Rational
+ | (C_integer _ | C_float _), Gmpz
+ | C_integer _, C_float _ ->
-1
- | (Gmpz | Real | Nan), C_type _
- | (Real | Nan), Gmpz
+ | (C_float _ | Gmpz | Rational | Real | Nan), C_integer _
+ | (Gmpz | Rational | Real | Nan), C_float _
+ | (Rational | Real | Nan), Gmpz
+ | (Real | Nan), Rational
| Nan, Real ->
1
- | Gmpz, Gmpz | Real, Real | Nan, Nan -> assert false
+ | Gmpz, Gmpz
+ | Rational, Rational
+ | Real, Real
+ | Nan, Nan ->
+ assert false
let equal = Datatype.from_compare
let hash = function
- | C_type ik -> 7 * Hashtbl.hash ik
+ | C_integer ik -> 7 * Hashtbl.hash ik
+ | C_float fk -> 97 * Hashtbl.hash fk
| Gmpz -> 787
+ | Rational -> 907
| Real -> 1011
| Nan -> 1277
let pretty fmt = function
- | C_type k -> Printer.pp_ikind fmt k
+ | C_integer k -> Printer.pp_ikind fmt k
+ | C_float k -> Printer.pp_fkind fmt k
| Gmpz -> Format.pp_print_string fmt "Gmpz"
+ | Rational -> Format.pp_print_string fmt "Rational"
| Real -> Format.pp_print_string fmt "Real"
| Nan -> Format.pp_print_string fmt "Nan"
end)
@@ -92,40 +109,58 @@ module D =
(** Basic operations *)
(******************************************************************************)
-let join ty1 ty2 = match ty1, ty2 with
- | Nan, Nan ->
- Nan
- | Nan, Real | Real, Nan ->
- Options.fatal "[typing] join failure: real and nan"
- | Real, Real -> Real
- | Real, (Gmpz | C_type _) | (Gmpz | C_type _), Real ->
- Real
- | Nan, (Gmpz | C_type _) | (Gmpz | C_type _), Nan ->
- Options.fatal "[typing] join failure: integer and nan"
- | Gmpz, _ | _, Gmpz -> Gmpz
- | C_type i1, C_type i2 ->
- if Options.Gmp_only.get () then Gmpz
- else
- let ty = Cil.arithmeticConversion (TInt(i1, [])) (TInt(i2, [])) in
- match ty with
- | TInt(i, _) -> C_type i
- | _ ->
- Options.fatal "[typing] join failure: unexpected result %a"
- Printer.pp_typ ty
+let join_cty ty1 ty2 =
+ let ty = Cil.arithmeticConversion ty1 ty2 in
+ match ty with
+ | TInt(i, _) -> C_integer i
+ | TFloat(f, _) -> C_float f
+ | _ ->
+ Options.fatal "[typing] join failure: unexpected result %a"
+ Printer.pp_typ ty
+
+let join ty1 ty2 =
+ if ty1 == ty2 then ty1
+ else
+ match ty1, ty2 with
+ | Nan, Nan | Real, Real | Rational, Rational | Gmpz, Gmpz ->
+ assert false
+ | Nan, (C_integer _ | C_float _ | Gmpz | Rational | Real as ty)
+ | (C_integer _ | C_float _ | Gmpz | Rational | Real as ty), Nan ->
+ Options.fatal "[typing] join failure: number %a and nan" D.pretty ty
+ | Real, (C_integer _ | C_float _ | Gmpz | Rational)
+ | (C_integer _ | C_float _ | Rational | Gmpz), Real ->
+ Real
+ | Rational, (C_integer _ | C_float _ | Gmpz)
+ | (C_integer _ | C_float _ | Gmpz), Rational
+ | C_float _, Gmpz
+ | Gmpz, C_float _ ->
+ Rational
+ | Gmpz, C_integer _
+ | C_integer _, Gmpz ->
+ Gmpz
+ | C_float f1, C_float f2 ->
+ join_cty (TFloat(f1, [])) (TFloat(f2, []))
+ | C_float f, C_integer n
+ | C_integer n, C_float f ->
+ join_cty (TFloat(f, [])) (TInt(n, []))
+ | C_integer i1, C_integer i2 ->
+ if Options.Gmp_only.get () then Gmpz
+ else join_cty (TInt(i1, [])) (TInt(i2, []))
exception Not_a_number
let typ_of_number_ty = function
- | C_type ik -> TInt(ik, [])
+ | C_integer ik -> TInt(ik, [])
+ | C_float fk -> TFloat(fk, [])
| Gmpz -> Gmp.Z.t ()
- | Real -> Real.t ()
+ (* for the time being, no reals but rationals instead *)
+ | Rational -> Real.t ()
+ | Real -> Error.not_yet "real number type"
| Nan -> raise Not_a_number
let typ_of_lty = function
| Ctype cty -> cty
| Linteger -> Gmp.Z.t ()
- | Lreal ->
- (* TODO RATIONAL: implement this case *)
- assert false
+ | Lreal -> Error.not_yet "real type"
| Ltype _ | Lvar _ | Larrow _ -> Options.fatal "unexpected logic type"
(******************************************************************************)
@@ -192,20 +227,31 @@ end
(* Compute the smallest type (bigger than [int]) which can contain the whole
interval. It is the \theta operator of the JFLA's paper. *)
-let ty_of_interv ?ctx i =
- try
- let kind = Interval.ikind_of_interv i in
- (match ctx with
- | None | Some (Gmpz | Nan) -> C_type kind
- | Some (C_type ik as ctx) ->
- (* return [ctx] type for types smaller than int to prevent superfluous
- casts in the generated code *)
- if Cil.intTypeIncluded kind ik then ctx else C_type kind
- | Some Real -> Real)
- with Cil.Not_representable ->
- match ctx with
- | Some Real -> Real
- | None | Some _ -> Gmpz
+let ty_of_interv ?ctx = function
+ | Interval.Float(fk, _) -> C_float fk
+ | Interval.Rational -> Rational
+ | Interval.Real -> Real
+ | Interval.Nan -> Nan
+ | Interval.Ival iv ->
+ try
+ let kind = Interval.ikind_of_ival iv in
+ (match ctx with
+ | None
+ | Some (Gmpz | Nan) ->
+ C_integer kind
+ | Some (C_integer ik as ctx) ->
+ (* return [ctx] type for types smaller than int to prevent superfluous
+ casts in the generated code *)
+ if Cil.intTypeIncluded kind ik then ctx else C_integer kind
+ | Some (C_float _ | Rational) ->
+ Rational
+ | Some Real ->
+ Real)
+ with Cil.Not_representable ->
+ match ctx with
+ | None | Some(C_integer _ | Gmpz | Nan) -> Gmpz
+ | Some (C_float _ | Rational) -> Rational
+ | Some Real -> Real
(* compute a new {!computed_info} by coercing the given type [ty] to the given
context [ctx]. [op] is the type for the operator. *)
@@ -224,8 +270,8 @@ let coerce ~arith_operand ~ctx ~op ty =
else { ty; op; cast = None }
let number_ty_of_typ ty = match Cil.unrollType ty with
- | TInt(ik, _) | TEnum({ ekind = ik }, _) -> C_type ik
- | TFloat _ -> Real
+ | TInt(ik, _) | TEnum({ ekind = ik }, _) -> C_integer ik
+ | TFloat(fk, _) -> C_float fk
| TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ -> Nan
| TNamed _ -> assert false
@@ -243,12 +289,8 @@ let ty_of_logic_ty ?term lty =
| Some t ->
if Options.Gmp_only.get () && lty = Linteger then Gmpz
else
- try
- let i = Interval.infer t in
- ty_of_interv i
- with
- | Interval.Not_a_number -> nan
- | Interval.Is_a_real -> real
+ let i = Interval.infer t in
+ ty_of_interv i
(******************************************************************************)
(** {2 Type system} *)
@@ -257,33 +299,23 @@ let ty_of_logic_ty ?term lty =
(* generate a context [c]. Take --e-acsl-gmp-only into account iff [use_gmp_opt]
is true. *)
let mk_ctx ~use_gmp_opt = function
- | C_type _ as c -> if use_gmp_opt && Options.Gmp_only.get () then Gmpz else c
- | Gmpz | Real | Nan as c -> c
+ | C_integer _ as c ->
+ if use_gmp_opt && Options.Gmp_only.get () then Gmpz
+ else c
+ | C_float _ | Gmpz | Rational | Real | Nan as c -> c
(* the number_ty corresponding to [t] whenever use as an offset.
In that case, it cannot be a GMP, so it must be coerced to an integral type
in that case *)
let type_offset t =
- try
- let i = Interval.infer t in
- match ty_of_interv i with
- | Gmpz -> C_type ILongLong (* largest possible type *)
- | ty -> ty
- with
- | Interval.Is_a_real ->
- (* TODO RATIONAL: shouldn't it be 'assert false' because of typing? *)
- C_type ILongLong
- | Interval.Not_a_number ->
- Options.fatal "expected an integral type for %a" Printer.pp_term t
-
-let type_letin li =
- let li_t = Misc.term_of_li li in
- match ty_of_logic_ty li_t.term_type with
- | C_type _ | Gmpz ->
- let i = Interval.infer li_t in
- Interval.Env.add li.l_var_info i
- | Real | Nan ->
- ()
+ let i = Interval.infer t in
+ match ty_of_interv i with
+ | Gmpz -> C_integer ILongLong (* largest possible type *)
+ | ty -> ty
+
+let type_letin li li_t =
+ let i = Interval.infer li_t in
+ Interval.Env.add li.l_var_info i
(* type the term [t] in a context [ctx] by taking --e-acsl-gmp-only into account
iff [use_gmp_opt] is true. *)
@@ -308,31 +340,17 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
(and of course also covers the missing cases). Also enforce the invariant
that every subterm is typed, even if it is not an integer. *)
match t.term_node with
- | TConst (LReal _) ->
- (* TODO RATIONAL: real: irrationals raise not_yet *)
- dup real
- | TConst (Integer _ | LChr _ | LEnum _)
+ | TConst (Integer _ | LChr _ | LEnum _ | LReal _)
| TSizeOf _
| TSizeOfStr _
| TAlignOf _ ->
- let ty =
- try
- let i = Interval.infer t in
- ty_of_interv ?ctx i
- with
- | Interval.Not_a_number -> nan
- | Interval.Is_a_real -> assert false
- in
+ let i = Interval.infer t in
+ let ty = ty_of_interv ?ctx i in
dup ty
+
| TLval tlv ->
- let ty =
- try
- let i = Interval.infer t in
- ty_of_interv ?ctx i
- with
- | Interval.Not_a_number -> nan
- | Interval.Is_a_real -> real
- in
+ let i = Interval.infer t in
+ let ty = ty_of_interv ?ctx i in
type_term_lval tlv;
dup ty
@@ -340,42 +358,24 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| Tblock_length(_, t')
| TSizeOfE t'
| TAlignOfE t' ->
- let ty =
- try
- let i = Interval.infer t in
- (* [t'] must be typed, but it is a pointer *)
- ignore (type_term ~use_gmp_opt:true ~ctx:nan t');
- ty_of_interv ?ctx i
- with (* this term is an integer *)
- | Interval.Is_a_real
- | Interval.Not_a_number -> assert false
- in
+ let i = Interval.infer t in
+ (* [t'] must be typed, but it is a pointer *)
+ ignore (type_term ~use_gmp_opt:true ~ctx:Nan t');
+ let ty = ty_of_interv ?ctx i in
dup ty
| TBinOp (MinusPP, t1, t2) ->
- let ty =
- try
- let i = Interval.infer t in
- (* [t1] and [t2] must be typed, but they are pointers *)
- ignore (type_term ~use_gmp_opt:true ~ctx:nan t1);
- ignore (type_term ~use_gmp_opt:true ~ctx:nan t2);
- ty_of_interv ?ctx i
- with (* this term is an integer *)
- | Interval.Is_a_real
- | Interval.Not_a_number -> assert false
- in
+ let i = Interval.infer t in
+ (* [t1] and [t2] must be typed, but they are pointers *)
+ ignore (type_term ~use_gmp_opt:true ~ctx:Nan t1);
+ ignore (type_term ~use_gmp_opt:true ~ctx:Nan t2);
+ let ty = ty_of_interv ?ctx i in
dup ty
| TUnOp (unop, t') ->
- let ctx_res, ctx =
- try
- let i = Interval.infer t in
- let i' = Interval.infer t' in
- compute_ctx ?ctx (Ival.join i i')
- with
- | Interval.Is_a_real -> real, real
- | Interval.Not_a_number -> assert false
- in
+ let i = Interval.infer t in
+ let i' = Interval.infer t' in
+ let ctx_res, ctx = compute_ctx ?ctx (Interval.join i i') in
ignore (type_term ~use_gmp_opt:true ~arith_operand:true ~ctx t');
(match unop with
| LNot -> c_int, ctx_res (* converted into [t == 0] in case of GMP *)
@@ -383,15 +383,11 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| TBinOp ((PlusA | MinusA | Mult | Div | Mod | Shiftlt | Shiftrt), t1, t2)
->
+ let i = Interval.infer t in
+ let i1 = Interval.infer t1 in
+ let i2 = Interval.infer t2 in
let ctx_res, ctx =
- try
- let i = Interval.infer t in
- let i1 = Interval.infer t1 in
- let i2 = Interval.infer t2 in
- compute_ctx ?ctx (Ival.join i (Ival.join i1 i2))
- with
- | Interval.Is_a_real -> dup real
- | Interval.Not_a_number -> assert false
+ compute_ctx ?ctx (Interval.join i (Interval.join i1 i2))
in
(* it is enough to explicitly coerce when required one operand to [ctx]
(through [arith_operand]) in order to force the type of the
@@ -410,33 +406,23 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
assert (match ctx with None -> true | Some c -> D.compare c c_int >= 0);
+ let i1 = Interval.infer t1 in
+ let i2 = Interval.infer t2 in
let ctx =
- try
- let i1 = Interval.infer t1 in
- let i2 = Interval.infer t2 in
- mk_ctx ~use_gmp_opt:true (ty_of_interv ?ctx (Ival.join i1 i2))
- with
- | Interval.Is_a_real -> real
- | Interval.Not_a_number -> nan
+ mk_ctx ~use_gmp_opt:true (ty_of_interv ?ctx (Interval.join i1 i2))
in
ignore (type_term ~use_gmp_opt:true ~ctx t1);
ignore (type_term ~use_gmp_opt:true ~ctx t2);
let ty = match ctx with
| Nan -> c_int
- | Real | Gmpz | C_type _ -> ctx
+ | Real | Rational | Gmpz | C_float _ | C_integer _ -> ctx
in
c_int, ty
| TBinOp ((LAnd | LOr), t1, t2) ->
- let ty =
- try
- let i1 = Interval.infer t1 in
- let i2 = Interval.infer t2 in
- ty_of_interv ?ctx (Ival.join i1 i2)
- with (* this term is an integer *)
- | Interval.Is_a_real
- | Interval.Not_a_number -> assert false
- in
+ let i1 = Interval.infer t1 in
+ let i2 = Interval.infer t2 in
+ let ty = ty_of_interv ?ctx (Interval.join i1 i2) in
(* both operands fit in an int. *)
ignore (type_term ~use_gmp_opt:true ~ctx:c_int t1);
ignore (type_term ~use_gmp_opt:true ~ctx:c_int t2);
@@ -447,17 +433,11 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| TBinOp (BOr, _, _) -> Error.not_yet "bitwise or"
| TCastE(_, t') ->
- let ctx =
- try
- (* compute the smallest interval from the whole term [t] *)
- let i = Interval.infer t in
- (* nothing more to do: [i] is already more precise than what we
- could infer from the arguments of the cast. *)
- ty_of_interv ?ctx i
- with
- | Interval.Not_a_number -> nan
- | Interval.Is_a_real -> real
- in
+ (* compute the smallest interval from the whole term [t] *)
+ let i = Interval.infer t in
+ (* nothing more to do: [i] is already more precise than what we could
+ infer from the arguments of the cast. *)
+ let ctx = ty_of_interv ?ctx i in
ignore (type_term ~use_gmp_opt:true ~ctx t');
dup ctx
@@ -467,16 +447,10 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
in
ignore (type_term ~use_gmp_opt:false ~ctx:ctx1 t1);
let i = Interval.infer t in
- let ctx =
- try
- let i2 = Interval.infer t2 in
- let i3 = Interval.infer t3 in
- let ctx = ty_of_interv ?ctx (Ival.join i (Ival.join i2 i3)) in
- mk_ctx ~use_gmp_opt:true ctx
- with
- | Interval.Is_a_real -> real
- | Interval.Not_a_number -> nan
- in
+ let i2 = Interval.infer t2 in
+ let i3 = Interval.infer t3 in
+ let ctx = ty_of_interv ?ctx (Interval.join i (Interval.join i2 i3)) in
+ let ctx = mk_ctx ~use_gmp_opt:true ctx in
ignore (type_term ~use_gmp_opt:true ~ctx t2);
ignore (type_term ~use_gmp_opt:true ~ctx t3);
dup ctx
@@ -489,19 +463,19 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| TStartOf tlv ->
(* it is a pointer, but subterms must be typed. *)
type_term_lval tlv;
- dup nan
+ dup Nan
| Tbase_addr (_, t) ->
(* it is a pointer, but subterms must be typed. *)
- ignore (type_term ~use_gmp_opt:true ~ctx:nan t);
- dup nan
+ ignore (type_term ~use_gmp_opt:true ~ctx:Nan t);
+ dup Nan
| TBinOp ((PlusPI | IndexPI | MinusPI), t1, t2) ->
(* both [t1] and [t2] must be typed. *)
- ignore (type_term ~use_gmp_opt:true ~ctx:nan t1);
+ ignore (type_term ~use_gmp_opt:true ~ctx:Nan t1);
let ctx = type_offset t2 in
ignore (type_term ~use_gmp_opt:false ~ctx t2);
- dup nan
+ dup Nan
| Tapp(li, _, args) ->
if Builtins.mem li.l_var_info.lv_name then
@@ -531,6 +505,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| None ->
assert false
| Some lty ->
+ (* TODO: what if the function returns a real? *)
let ty = ty_of_logic_ty ~term:t lty in
dup ty
end
@@ -545,24 +520,22 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| Tunion _ -> Error.not_yet "tset union"
| Tinter _ -> Error.not_yet "tset intersection"
| Tcomprehension (_,_,_) -> Error.not_yet "tset comprehension"
+
+ | Trange(None, _) | Trange(_, None) ->
+ Options.abort "unbounded ranges are not part of E-ACSl"
| Trange(Some n1, Some n2) ->
ignore (type_term ~use_gmp_opt n1);
ignore (type_term ~use_gmp_opt n2);
- (try
- let i = Interval.infer t in
- let ty = ty_of_interv ?ctx i in
- dup ty
- with
- | Interval.Is_a_real -> dup real
- | Interval.Not_a_number -> dup nan)
+ let i = Interval.infer t in
+ let ty = ty_of_interv ?ctx i in
+ dup ty
- | Trange(None, _) | Trange(_, None) ->
- Options.abort "unbounded ranges are not part of E-ACSl"
| Tlet(li, t) ->
- type_letin li;
let li_t = Misc.term_of_li li in
+ type_letin li li_t;
ignore (type_term ~use_gmp_opt:true li_t);
dup (type_term ~use_gmp_opt:true ?ctx t).ty
+
| Tlambda (_,_) -> Error.not_yet "lambda"
| TDataCons (_,_) -> Error.not_yet "datacons"
| TUpdate (_,_,_) -> Error.not_yet "update"
@@ -571,7 +544,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| TConst (LStr _ | LWStr _)
| Ttypeof _
| Ttype _
- | Tempty_set -> dup nan
+ | Tempty_set -> dup Nan
in
Memo.memo
(fun t ->
@@ -588,7 +561,7 @@ and type_term_lval (host, offset) =
and type_term_lhost = function
| TVar _
| TResult _ -> ()
- | TMem t -> ignore (type_term ~use_gmp_opt:false ~ctx:nan t)
+ | TMem t -> ignore (type_term ~use_gmp_opt:false ~ctx:Nan t)
and type_term_offset = function
| TNoOffset -> ()
@@ -613,28 +586,22 @@ let rec type_predicate p =
a retyping is done there *)
c_int
| LBnone -> (* Eg: \is_finite *)
- Error.not_yet "logic functions with no definition nor reads clause"
+ Error.not_yet "predicate with no definition nor reads clause"
| LBreads _ | LBterm _ | LBinductive _ ->
Options.fatal "unexpected logic definition"
end
| Pseparated _ -> Error.not_yet "\\separated"
| Pdangling _ -> Error.not_yet "\\dangling"
| Prel(_, t1, t2) ->
- let ctx =
- try
- let i1 = Interval.infer t1 in
- let i2 = Interval.infer t2 in
- let i = Ival.join i1 i2 in
- mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:c_int i)
- with
- | Interval.Not_a_number -> nan
- | Interval.Is_a_real -> real
- in
+ let i1 = Interval.infer t1 in
+ let i2 = Interval.infer t2 in
+ let i = Interval.join i1 i2 in
+ let ctx = mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:c_int i) in
ignore (type_term ~use_gmp_opt:true ~ctx t1);
ignore (type_term ~use_gmp_opt:true ~ctx t2);
(match ctx with
| Nan -> c_int
- | Real | Gmpz | C_type _ -> ctx)
+ | Real | Rational | Gmpz | C_float _ | C_integer _ -> ctx)
| Pand(p1, p2)
| Por(p1, p2)
| Pxor(p1, p2)
@@ -653,64 +620,63 @@ let rec type_predicate p =
ignore (type_predicate p2);
c_int
| Plet(li, p) ->
- type_letin li;
let li_t = Misc.term_of_li li in
+ type_letin li li_t;
ignore (type_term ~use_gmp_opt:true li_t);
(type_predicate p).ty
| Pforall(bounded_vars, { pred_content = Pimplies(hyps, goal) })
| Pexists(bounded_vars, { pred_content = Pand(hyps, goal) }) ->
let guards = !compute_quantif_guards_ref p bounded_vars hyps in
- (try
- List.iter
- (fun (t1, r1, x, r2, t2) ->
- let i1 = Interval.infer t1 in
- let i1 = match r1 with
- | Rlt -> Ival.add_singleton_int Integer.one i1
- | Rle -> i1
- | _ -> assert false
- in
- let i2 = Interval.infer t2 in
- (* add one to [i2], since we increment the loop counter one more
- time before going outside the loop. *)
- let i2 = match r2 with
- | Rlt -> i2
- | Rle -> Ival.add_singleton_int Integer.one i2
- | _ -> assert false
- in
- let i = Ival.join i1 i2 in
- let ctx = match x.lv_type with
- | Linteger -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmpz i)
- | Ctype ty ->
- (match Cil.unrollType ty with
- | TInt(ik, _) -> mk_ctx ~use_gmp_opt:true (C_type ik)
- | ty ->
- Options.fatal "unexpected type %a for quantified variable %a"
- Printer.pp_typ ty
- Printer.pp_logic_var x)
- | lty ->
+ let iv_plus_one iv =
+ Interval.Ival (Ival.add_singleton_int Integer.one iv)
+ in
+ List.iter
+ (fun (t1, r1, x, r2, t2) ->
+ let i1 = Interval.infer t1 in
+ let i1 = match r1, i1 with
+ | Rlt, Interval.Ival iv -> iv_plus_one iv
+ | Rle, _ -> i1
+ | _ -> assert false
+ in
+ let i2 = Interval.infer t2 in
+ (* add one to [i2], since we increment the loop counter one more
+ time before going outside the loop. *)
+ let i2 = match r2, i2 with
+ | Rlt, _ -> i2
+ | Rle, Interval.Ival iv -> iv_plus_one iv
+ | _ -> assert false
+ in
+ let i = Interval.join i1 i2 in
+ let ctx = match x.lv_type with
+ | Linteger -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmpz i)
+ | Ctype ty ->
+ (match Cil.unrollType ty with
+ | TInt(ik, _) -> mk_ctx ~use_gmp_opt:true (C_integer ik)
+ | ty ->
Options.fatal "unexpected type %a for quantified variable %a"
- Printer.pp_logic_type lty
- Printer.pp_logic_var x
- in
- (* forcing when typing bounds prevents to generate an extra useless
- GMP variable when --e-acsl-gmp-only *)
- ignore (type_term ~use_gmp_opt:false ~ctx t1);
- ignore (type_term ~use_gmp_opt:false ~ctx t2);
- (* if we must generate GMP code, degrade the interval in order to
- guarantee that [x] will be a GMP when typing the goal *)
- let i = match ctx with
- | C_type _ -> i
- | Gmpz -> Ival.inject_range None None (* [ -\infty; +\infty ] *)
- | Nan -> assert false
- | Real -> Error.not_yet "reals: quantification"
- in
- Interval.Env.add x i)
- guards;
- (type_predicate goal).ty
- with
- | Interval.Not_a_number -> assert false
- | Interval.Is_a_real -> Error.not_yet "quantification over real numbers")
+ Printer.pp_typ ty
+ Printer.pp_logic_var x)
+ | lty ->
+ Options.fatal "unexpected type %a for quantified variable %a"
+ Printer.pp_logic_type lty
+ Printer.pp_logic_var x
+ in
+ (* forcing when typing bounds prevents to generate an extra useless
+ GMP variable when --e-acsl-gmp-only *)
+ ignore (type_term ~use_gmp_opt:false ~ctx t1);
+ ignore (type_term ~use_gmp_opt:false ~ctx t2);
+ (* if we must generate GMP code, degrade the interval in order to
+ guarantee that [x] will be a GMP when typing the goal *)
+ let i = match ctx with
+ | C_integer _ -> i
+ | Gmpz -> Interval.top_ival (* [ -\infty; +\infty ] *)
+ | C_float _ | Rational | Real | Nan ->
+ Options.fatal "unexpected quantification over %a" D.pretty ctx
+ in
+ Interval.Env.add x i)
+ guards;
+ (type_predicate goal).ty
| Pinitialized(_, t)
| Pfreeable(_, t)
@@ -718,7 +684,7 @@ let rec type_predicate p =
| Pvalid(_, t)
| Pvalid_read(_, t)
| Pvalid_function t ->
- ignore (type_term ~use_gmp_opt:false ~ctx:nan t);
+ ignore (type_term ~use_gmp_opt:false ~ctx:Nan t);
c_int
| Pforall _ -> Error.not_yet "unguarded \\forall quantification"
@@ -761,7 +727,8 @@ let extract_typ t ty =
with Not_a_number ->
match t.term_type with
| Ctype _ as lty -> Logic_utils.logicCType lty
- | Linteger | Lreal -> assert false
+ | Linteger | Lreal ->
+ Options.fatal "unexpected context NaN for term %a" Printer.pp_term t
| Ltype _ -> Error.not_yet "unsupported logic type: user-defined type"
| Lvar _ -> Error.not_yet "unsupported logic type: type variable"
| Larrow _ -> Error.not_yet "unsupported logic type: type arrow"
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 7674d4519ed19a145d9adb8eb6f0fe404a6cdd48..29be0fa5d4e072b353af0a821f314178166d5cd1 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -53,8 +53,10 @@ open Cil_types
(** Possible types infered by the system. *)
type number_ty = private
- | C_type of ikind
+ | C_integer of ikind
+ | C_float of fkind
| Gmpz
+ | Rational
| Real
| Nan
@@ -64,8 +66,9 @@ module Datatype: Datatype.S_with_collections with type t = number_ty
val c_int: number_ty
val ikind: ikind -> number_ty
+val fkind: fkind -> number_ty
val gmpz: number_ty
-val real: number_ty
+val rational: number_ty
val nan: number_ty
(** {3 Useful operations over {!number_ty}} *)
@@ -139,7 +142,7 @@ val unsafe_set: term -> ?ctx:number_ty -> number_ty -> unit
(** {2 Typing/types-related utils} *)
(*****************************************************************************)
-val ty_of_interv: ?ctx:number_ty -> Ival.t -> number_ty
+val ty_of_interv: ?ctx:number_ty -> Interval.t -> number_ty
(* Compute the smallest type (bigger than [int]) which can contain the whole
interval. It is the \theta operator of the JFLA's paper. *)