diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 7b213fa5830e2d23285b1355104a7945e19c1ce3..26e2eec5466422874246fdf59d6117dd6a789cb5 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,12 +25,14 @@
Plugin E-ACSL <next-release>
############################
+-* E-ACSL [2022-17-06] Fix wrong cast from pointer to integer (frama-c/frama-c#1119)
##############################
Plugin E-ACSL 25.0 (Manganese)
##############################
-* E-ACSL [2022-23-05] Fix crash for quantifications over enum types (frama-c/e-acsl#199)
+-* E-ACSL [2022-06-09] Fix wrong cast of pointer to integer (frama-c/frama-c#1119)
- E-ACSL [2022-03-04] Improve translation of `\at()` terms and
predicates (frama-c/e-acsl#108).
-* E-ACSL [2022-03-01] Fix normalization of global annotations that
diff --git a/src/plugins/e-acsl/src/analyses/analyses.ml b/src/plugins/e-acsl/src/analyses/analyses.ml
index 181ceceaf62a23ff199dcecfc03d2790e4b23374..41266a7b2b3ae557a33c08196edaa350aa621833 100644
--- a/src/plugins/e-acsl/src/analyses/analyses.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses.ml
@@ -29,6 +29,8 @@ let preprocess () =
Logic_normalizer.preprocess ast;
analyses_feedback "normalizing quantifiers";
Bound_variables.preprocess ast;
+ analyses_feedback "infering interval of annotations";
+ Interval.infer_program ast;
analyses_feedback "typing annotations";
Typing.type_program ast;
analyses_feedback
@@ -40,6 +42,6 @@ let reset () =
Literal_strings.reset ();
Bound_variables.clear_guards ();
Logic_normalizer.clear ();
- Interval.Env.clear();
+ Interval.clear ();
Typing.clear ();
Labels.reset ()
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
index e405d452408ba13afe41a1a12c42089059605491..473ce5547af126a357533a79d850e3fe18e452d3 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
@@ -248,3 +248,240 @@ module At_data = struct
Ext_logic_label.pretty elabel
end)
end
+
+module Ival_datatype =
+ 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)
+
+(* Profiles of functions are the interval ranges of their arguments. For
+ memoization purposes, we need need them as keys of hashtables, even though
+ they are implemented as maps. Functions typically do not have many arguments
+ so it is acceptable to do so.*)
+module Profile =
+struct
+ let rec make args ival =
+ match args,ival with
+ | [],[] -> Logic_var.Map.empty
+ | x::args, i::ival -> Logic_var.Map.add x i (make args ival)
+ | [], _::_ | _::_, [] -> assert false
+
+ include
+ Datatype.Make_with_collections
+ (struct
+ include Datatype.Undefined
+
+ type t = ival Logic_var.Map.t
+
+ let equal = Logic_var.Map.equal Ival_datatype.equal
+ let compare = Logic_var.Map.compare Ival_datatype.compare
+
+ let mem_project = Datatype.never_any_project
+ let copy m = Logic_var.Map.fold Logic_var.Map.add m Logic_var.Map.empty
+ let hash m =
+ Logic_var.Map.fold
+ (fun v i h -> h + Logic_var.hash v + Ival_datatype.hash i)
+ m
+ 0
+ let reprs =
+ let v = List.hd Logic_var.reprs in
+ let i = List.hd Ival_datatype.reprs in
+ [ Logic_var.Map.add v i Logic_var.Map.empty ]
+ let structural_descr = Structural_descr.t_abstract
+ let rehash = Datatype.identity
+ let name = "E-ACSL.Profile"
+ end)
+
+ let is_empty = Logic_var.Map.is_empty
+
+ let empty = Logic_var.Map.empty
+end
+
+module Id_term_in_profile =
+ Datatype.Pair_with_collections
+ (Misc.Id_term)
+ (Profile)
+ (struct let module_name = "E_ACSL.Analyse.Id_term_in_profile" end)
+
+(* Environment to handle recursive functions: this environment stores the logic
+ functions that we have already started inferring along with their
+ profiles. This is necessary for the fixpoint algorithm. *)
+module LFProf =
+ Datatype.Pair_with_collections (Cil_datatype.Logic_info) (Profile)
+ (struct
+ let module_name = "E_ACSL.Interval.LFProf"
+ end)
+
+module Logic_env
+= struct
+ type t = { profile : Profile.t;
+ let_quantif_bind : Profile.t}
+
+ let add env x i =
+ { env with let_quantif_bind = Logic_var.Map.add x i env.let_quantif_bind}
+
+ let empty =
+ {profile = Logic_var.Map.empty;
+ let_quantif_bind = Logic_var.Map.empty}
+
+ let make profile =
+ { profile = profile;
+ let_quantif_bind = Logic_var.Map.empty }
+
+ let find env x =
+ try Logic_var.Map.find x env.let_quantif_bind
+ with Not_found ->
+ Logic_var.Map.find x env.profile
+
+ let get_profile env = env.profile
+
+end
+
+(* Imperative environment to perform fixpoint algorithm for recursive
+ functions *)
+module LF_env
+= struct
+
+ let tbl = LFProf.Hashtbl.create 17
+
+ let clear () = LFProf.Hashtbl.clear tbl
+
+ let find li profile = LFProf.Hashtbl.find tbl (li,profile)
+
+ let add li profile ival = LFProf.Hashtbl.add tbl (li,profile) ival
+
+ exception Recursive
+
+ let contain li = object
+ inherit Visitor.frama_c_inplace
+
+ method! vpredicate p =
+ match p.pred_content with
+ | Papp (li_app,_,_) when Cil_datatype.Logic_info.equal li li_app ->
+ raise Recursive;
+ | _ -> Cil.DoChildren
+
+ method! vterm t =
+ match t.term_node with
+ | Tapp(li_app,_,_) when Cil_datatype.Logic_info.equal li li_app ->
+ raise Recursive
+ | _ -> Cil.DoChildren
+
+ method! vlogic_type _ = Cil.SkipChildren
+ end
+
+ let is_rec li =
+ match li.l_body with
+ | LBpred p ->
+ (try ignore (Visitor.visitFramacPredicate (contain li) p); false
+ with Recursive -> true)
+ | LBterm t ->
+ (try ignore (Visitor.visitFramacTerm (contain li) t); false
+ with Recursive -> true)
+ | LBreads _ | LBnone -> false
+ | LBinductive _ -> Error.not_yet "Inductive"
+
+ let replace li args_ival ival = LFProf.Hashtbl.replace tbl (li, args_ival) ival
+
+end
+
+module Number_ty =
+ Datatype.Make_with_collections
+ (struct
+ type t = number_ty
+ let name = "E_ACSL.Typing.t"
+ let reprs = [ Gmpz; Real; Nan; C_integer IInt ]
+ include Datatype.Undefined
+
+ let compare ty1 ty2 =
+ if ty1 == ty2 then 0
+ else
+ match ty1, ty2 with
+ | C_integer i1, C_integer i2 ->
+ if i1 = i2 then 0
+ else if Cil.intTypeIncluded i1 i2 then -1 else 1
+ | 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
+ | (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
+ | Rational, Rational
+ | Real, Real
+ | Nan, Nan ->
+ assert false
+
+ let equal = Datatype.from_compare
+
+ let hash = function
+ | 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_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)
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
index 7b19f984097738c2225a969ed1dc507f9b84ca35..008856976aa48dc11e4b8ac6c5459ca3c8e5870d 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
@@ -43,3 +43,66 @@ module At_data: sig
(** [create ?error kf kinstr lscope pot label] creates an [at_data] from the
given arguments. *)
end
+
+module Ival_datatype: Datatype.S_with_collections with type t = ival
+
+(** profile that maps logic variables that are function parameters to their
+ interval depending on the arguments at the callsite of the function *)
+module Profile: sig
+ include
+ Datatype.S_with_collections
+ with type t = ival Cil_datatype.Logic_var.Map.t
+
+ val make: logic_var list -> ival list -> t
+ val is_empty: t -> bool
+ val empty: t
+
+end
+
+(** term with a profile: a term inside a logic function or predicate may
+ contain free variables. The profile indicates the interval for those
+ free variables. *)
+module Id_term_in_profile: Datatype.S_with_collections
+ with type t = term * Profile.t
+
+(** profile of logic function or predicate: a logic info representing a logic
+ function or a predicate together with a profile for its arguments. *)
+module LFProf: Datatype.S_with_collections
+ with type t = logic_info * Profile.t
+
+(** logic environment: interval of all bound variables. It consists in two
+ components
+ - a profile for variables bound through function arguments
+ - an association list for variables bound by a let or a quantification *)
+module Logic_env : sig
+ type t
+ (* add a new binding for a let or a quantification binder only *)
+ val add : t -> logic_var -> ival -> t
+ (* the empty environment *)
+ val empty : t
+ (* create a new environment from a profile, for function calls *)
+ val make : Profile.t -> t
+ (* find a logic variable in the environment *)
+ val find : t -> logic_var -> ival
+ (* get the profile of the logic environment, i.e. bindings through function
+ arguments *)
+ val get_profile : t -> Profile.t
+end
+
+
+(** Imperative environment to perform the fixpoint algorithm for recursive
+ functions *)
+module LF_env : sig
+ val find : logic_info -> Profile.t -> ival
+
+ val clear : unit -> unit
+
+ val add : logic_info -> Profile.t -> ival -> unit
+
+ val is_rec : logic_info -> bool
+
+ val replace : logic_info -> Profile.t -> ival -> unit
+end
+
+module Number_ty: Datatype.S_with_collections
+ with type t = number_ty
diff --git a/src/plugins/e-acsl/src/analyses/analyses_types.mli b/src/plugins/e-acsl/src/analyses/analyses_types.mli
index 06f9eddb5a09fb4cbe80497516bef543e1ee6cdc..ea2ec78290d21a627390b476e49ef34f36767070 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_types.mli
+++ b/src/plugins/e-acsl/src/analyses/analyses_types.mli
@@ -67,3 +67,21 @@ type annotation_kind =
| Invariant
| Variant
| RTE
+
+(** Type of intervals inferred by the interval inference *)
+type ival =
+ | Ival of Ival.t
+ | Float of fkind * float option (* a float constant, if any *)
+ | Rational
+ | Real
+ | Nan
+
+(** Type of types inferred by the type inference for types representing
+ numbers *)
+type number_ty =
+ | C_integer of ikind
+ | C_float of fkind
+ | Gmpz
+ | Rational
+ | Real
+ | Nan
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 5199e4e66877841833130e726765a884a73618c8..83f51025ce22159bd623830357532d32a9c7874f 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -664,7 +664,6 @@ let normalize_guard ~loc (t1, rel1, lv, rel2, t2) =
in
t1, lv, t2
-
let compute_guards loc ~is_forall p bounded_vars hyps =
try
let guards,goal = compute_quantif_guards p ~is_forall bounded_vars hyps in
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 86bcf2fb9a0eeb50b2baca1349ac9b18d3739451..f68cae7dcf7b99d17e06792c8fc7208ba865af0c 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -21,76 +21,19 @@
(**************************************************************************)
open Cil_types
+open Analyses_types
+open Analyses_datatype
(* Implements Figure 3 of J. Signoles' JFLA'15 paper "Rester statique pour
devenir plus rapide, plus précis et plus mince".
Also implements a support for real numbers. *)
-
-module Error = Error.Make(struct let phase = Options.Dkey.interval end)
+let dkey = Options.Dkey.interval
+module Error = Error.Make(struct let phase = dkey end)
(* ********************************************************************* *)
(* Basic datatypes and operations *)
(* ********************************************************************* *)
-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) ->
@@ -393,144 +336,156 @@ let ikind_of_ival iv =
(* TODO: do not raise an exception, but returns a value instead *)
raise Cil.Not_representable (* GMP *)
-(* function call profiles (intervals for their formal parameters) *)
-module Profile = struct
- include Datatype.List_with_collections
- (D)
- (struct
- let module_name = "E_ACSL.Interval.Logic_function_env.Profile"
- end)
- let is_included p1 p2 = List.for_all2 is_included p1 p2
-end
-(* Imperative environments *)
-module rec Env: sig
+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 widen_profile =
+ Cil_datatype.Logic_var.Map.map interv_of_typ_containing_interv
+
+let rec fixpoint ~(infer : force:bool ->
+ logic_env:Logic_env.t ->
+ term ->
+ ival Error.result)
+ li args_ival t' ival =
+ let get_res = Error.map (fun x -> x) in
+ let logic_env = Logic_env.make args_ival in
+ (* If the logic function has a given C type, we use this type to infer the
+ interval. Otherwise we compute this interval as a fixpoint *)
+ match li.l_type with
+ | Some (Ctype typ) ->
+ let ival = interv_of_typ typ in
+ LF_env.add li args_ival ival;
+ ignore (infer ~force:true ~logic_env t');
+ ival
+ | None | Some (Linteger | Lreal | Ltype _ | Lvar _ | Larrow _) ->
+ LF_env.replace li args_ival ival;
+ let inferred_ival = get_res (infer ~force:true ~logic_env t') in
+ if is_included inferred_ival ival
+ then
+ ival
+ else
+ fixpoint ~infer li args_ival t' inferred_ival
+
+
+(* Memoization module which retrieves the computed info of some terms *)
+module Memo: sig
+ val memo:
+ force_infer:bool -> Profile.t -> (term -> ival) -> term -> ival Error.result
+ val get: Profile.t -> term -> ival Error.result
val clear: unit -> unit
- val add: Cil_types.logic_var -> ival -> unit
- val find: Cil_types.logic_var -> ival
- val remove: Cil_types.logic_var -> unit
end = struct
+ (* The comparison over terms is the physical equality. It cannot be the
+ structural one (given by [Cil_datatype.Term.equal]) for efficiency.
+
+ By construction (see prepare_ast.ml), there are no physically equal terms
+ in the E-ACSL's generated AST, but
+ - type info of many terms are accessed several times
+ - the translation of E-ACSL guarded quantifications generates
+ new terms (see module {!Quantif}) which must be typed. The term
+ corresponding to the bound variable [x] is actually used twice: once in
+ the guard and once for encoding [x+1] when incrementing it. *)
+ let nondep_tbl : ival Error.result Misc.Id_term.Hashtbl.t =
+ Misc.Id_term.Hashtbl.create 97
+
+ (* The interval of the logic function
+ //@ logic integer f (integer x) = x + 1;
+ depends on the interval of [x]. The same term [x+1] can be infered to be
+ in different intervals if the function [f] is applied several times with
+ different arguments. In this case, we add the interval of [x] as a key
+ to retrieve the type of [x+1].
+ There are two other kinds of binders for logical variables: [TLet] and
+ the quantifiers, however in those cases, a term is only ever translated
+ once. *)
+
+ let dep_tbl : ival Error.result Id_term_in_profile.Hashtbl.t
+ = Id_term_in_profile.Hashtbl.create 97
+
+ (* Small functor to access the result of a memoized inference *)
+ module Accesses (X : Datatype.S_with_collections)
+ (Tbl: sig val tbl : ival Error.result X.Hashtbl.t end)
+ : sig
+ val get : X.Hashtbl.key -> ival Error.result
+ val memo : force_infer:bool -> (term -> ival) -> term -> X.Hashtbl.key ->
+ (ival, exn) Result.t
+ end = struct
+ let get k =
+ try X.Hashtbl.find Tbl.tbl k
+ with Not_found -> Error.not_memoized ()
+
+ let memo ~force_infer f t k =
+ if force_infer then
+ let x =
+ try Result.Ok (f t);
+ with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Error exn
+ in
+ X.Hashtbl.replace Tbl.tbl k x;
+ x
+ else
+ try X.Hashtbl.find Tbl.tbl k
+ with Not_found ->
+ let x =
+ try Result.Ok (f t);
+ with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Error exn
+ in
+ X.Hashtbl.add Tbl.tbl k x;
+ x
+ end
- open Cil_datatype
- let tbl: ival Logic_var.Hashtbl.t = Logic_var.Hashtbl.create 7
+ module Nondep = Accesses (Misc.Id_term) (struct let tbl = nondep_tbl end)
+ module Dep = Accesses (Id_term_in_profile) (struct let tbl = dep_tbl end)
- (* 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
- \let body depends on one formal) *)
- let add = Logic_var.Hashtbl.add tbl
- let remove = Logic_var.Hashtbl.remove tbl
- let find = Logic_var.Hashtbl.find tbl
+ let get profile t =
+ if Profile.is_empty profile
+ then Nondep.get t
+ else Dep.get (t,profile)
- let clear () =
- Logic_var.Hashtbl.clear tbl;
- Logic_function_env.clear ()
+ let memo ~force_infer profile f t =
+ if Profile.is_empty profile
+ then Nondep.memo ~force_infer f t t
+ else Dep.memo ~force_infer f t (t,profile)
+ let clear () =
+ Options.feedback ~level:4 "clearing the typing tables";
+ Misc.Id_term.Hashtbl.clear nondep_tbl;
+ Id_term_in_profile.Hashtbl.clear dep_tbl
end
-(* Environment for handling logic functions *)
-and Logic_function_env: sig
- val widen: infer:(term -> ival) -> term -> ival -> bool * ival
+(* For recursive functions, it is necessary to use a widened profile to query
+ the table (because of the fixpoint algorithm). This module associates to a
+ term in a profile, the profile that should be used to query the table *)
+module Widened_profile: sig
+ val get: Profile.t -> logic_info -> Profile.t
+ val add: Profile.t -> logic_info -> Profile.t -> unit
val clear: unit -> unit
end = struct
- (* The environment associates to each term (denoting a logic function
- application) a profile, i.e. the list of intervals for its formal
- parameters. It helps to type these applications.
-
- For each pair of function name and profile, an interval containing the
- result is also stored. It helps to generate the function definitions for
- each logic function (for each function, one definition per profile) . *)
-
- module Terms = Hashtbl.Make
- (struct
- type t = term
- let equal = (==)
- let hash = Cil_datatype.Term.hash
- end)
+ let widened_profile_tbl : Profile.t LFProf.Hashtbl.t
+ = LFProf.Hashtbl.create 97
- module LF =
- Datatype.Pair_with_collections
- (Datatype.String)
- (Profile)
- (struct
- let module_name = "E_ACSL.Interval.Logic_function_env.LF"
- end)
+ let get profile li =
+ LFProf.Hashtbl.find_def widened_profile_tbl (li, profile) profile
- let terms: Profile.t Terms.t = Terms.create 7
- let named_profiles = LF.Hashtbl.create 7
+ let add profile i args_ival =
+ LFProf.Hashtbl.add widened_profile_tbl (i, profile) args_ival
let clear () =
- Terms.clear terms;
- LF.Hashtbl.clear named_profiles
-
- 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
- | [], [], [] -> []
- | x1 :: l1, x2 :: l2, x3 :: l3 -> f x1 x2 x3 :: map3 f l1 l2 l3
- | _, _, _ -> invalid_arg "E_ACSL.Interval.map3"
-
- 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 _ -> bottom) li.l_profile
- | Some p -> p
- in
- li.l_var_info.lv_name,
- map3
- (fun param old_i arg ->
- 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
- | _ ->
- assert false
+ Options.feedback ~level:4 "clearing the typing tables";
+ LFProf.Hashtbl.clear widened_profile_tbl
- let widen_one_callsite ~infer old_profile t i =
- 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 is_included i old_i then true, p, old_i (* fixpoint reached *)
- else begin
- let j = join i old_i in
- LF.Hashtbl.replace named_profiles named_p j;
- false, p, j
- end
- with Not_found ->
- LF.Hashtbl.add named_profiles named_p i;
- false, p, i
-
- let widen ~infer t i =
- try
- let old_p = Terms.find terms t in
- let is_included, new_p, i = widen_one_callsite ~infer (Some old_p) t i in
- if Profile.is_included new_p old_p then is_included, i
- else begin
- Terms.replace terms t new_p;
- false, i
- end
- with Not_found ->
- let is_included, p, i = widen_one_callsite ~infer None t i in
- Terms.add terms t p;
- is_included, i
end
+let plus_one i =
+ lift_arith_binop Ival.add_int i (singleton Integer.one)
+
(* ********************************************************************* *)
(* Main functions *)
(* ********************************************************************* *)
@@ -639,238 +594,266 @@ let infer_sum_product oper lambda min max = match lambda, min, max with
| Z.Overflow (* if the exponent of \product is too high *) -> top_ival)
| _ -> Error.not_yet "extended quantifiers with non-integer parameters"
-let rec infer t =
+let rec infer ~force ~logic_env t =
let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in
- match t.term_node with
- | TConst (Integer (n, _)) -> singleton n
- | TConst (LChr c) ->
- let n = Cil.charConstToInt c in
- 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
- singleton n
- | TLval lv -> infer_term_lval lv
- | TSizeOf ty -> infer_sizeof ty
- | TSizeOfE t -> infer_sizeof (get_cty t)
- | TSizeOfStr str -> singleton_of_int (String.length str + 1 (* '\0' *))
- | TAlignOf ty -> infer_alignof ty
- | TAlignOfE t -> infer_alignof (get_cty t)
-
- | TUnOp (Neg, t) ->
- let i = infer t in
- lift_unop Ival.neg_int i
- | TUnOp (BNot, t) ->
- let i = infer t in
- lift_unop Ival.bitwise_signed_not i
- | TUnOp (LNot, _)
- | TBinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _) ->
- Ival Ival.zero_or_one
-
- | TBinOp (PlusA, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.add_int i1 i2
- | TBinOp (MinusA, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.sub_int i1 i2
- | TBinOp (Mult, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.mul i1 i2
- | TBinOp (Div, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.div i1 i2
- | TBinOp (Mod, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.c_rem i1 i2
- | TBinOp (Shiftlt, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.shift_left i1 i2
- | TBinOp (Shiftrt, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.shift_right i1 i2
- | TBinOp (BAnd, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.bitwise_and i1 i2
- | TBinOp (BXor, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.bitwise_xor i1 i2
- | TBinOp (BOr, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.bitwise_or i1 i2
- | TCastE (ty, t) ->
- 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
- join i2 i3
- | Tat (t, _) ->
- infer t
- | TBinOp (MinusPP, t, _) ->
- (match Cil.unrollType (get_cty t) with
- | TArray(_, _, _) as ta ->
- begin
- try
- let n = Cil.bitsSizeOf ta in
- (* 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
- ival Integer.zero (Integer.of_int nb_bytes)
- with Cil.SizeOfError _ ->
- Lazy.force interv_of_unknown_block
- end
- | TPtr _ ->
- Lazy.force interv_of_unknown_block
- | _ -> assert false)
- | Tblock_length (_, t)
- | Toffset(_, t) ->
- (match Cil.unrollType (get_cty t) with
- | TArray(_, _, _) as ta ->
- begin
- try
- let n = Cil.bitsSizeOf ta in
- let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
- singleton_of_int nb_bytes
- with Cil.SizeOfError _ ->
- Lazy.force interv_of_unknown_block
- end
- | TPtr _ -> Lazy.force interv_of_unknown_block
- | _ -> assert false)
- | Tnull -> singleton_of_int 0
- | TLogic_coerce (_, t) -> infer t
- | Tapp (li, lst, args) ->
- (match li.l_body with
- | LBpred _ ->
- Ival Ival.zero_or_one
- | LBterm t' ->
- let rec fixpoint i =
- let is_included, new_i =
- Logic_function_env.widen ~infer t i
+ let get_res = Error.map (fun x -> x) in
+ let t = Logic_normalizer.get_term t in
+ let compute t =
+ match t.term_node with
+ | TConst (Integer (n, _)) -> singleton n
+ | TConst (LChr c) ->
+ let n = Cil.charConstToInt c in
+ 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
+ singleton n
+ | TLval lv -> infer_term_lval ~force ~logic_env lv
+ | TSizeOf ty -> infer_sizeof ty
+ | TSizeOfE t ->
+ ignore (infer ~force ~logic_env t);
+ infer_sizeof (get_cty t)
+ | TSizeOfStr str -> singleton_of_int (String.length str + 1 (* '\0' *))
+ | TAlignOf ty -> infer_alignof ty
+ | TAlignOfE t ->
+ ignore (infer ~force ~logic_env t);
+ infer_alignof (get_cty t)
+
+ | TUnOp (Neg, t) ->
+ let i = infer ~force ~logic_env t in
+ Error.map (lift_unop Ival.neg_int) i
+ | TUnOp (BNot, t) ->
+ let i = infer ~force ~logic_env t in
+ Error.map (lift_unop Ival.bitwise_signed_not) i
+ | TUnOp (LNot, t) ->
+ ignore (infer ~force ~logic_env t);
+ Ival Ival.zero_or_one
+
+ | TBinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), t1, t2) ->
+ ignore (infer ~force ~logic_env t1);
+ ignore (infer ~force ~logic_env t2);
+ Ival Ival.zero_or_one
+
+ | TBinOp (PlusA, t1, t2) ->
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
+ Error.map2 (lift_arith_binop Ival.add_int) i1 i2
+ | TBinOp (MinusA, t1, t2) ->
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
+ Error.map2 (lift_arith_binop Ival.sub_int) i1 i2
+ | TBinOp (Mult, t1, t2) ->
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
+ Error.map2 (lift_arith_binop Ival.mul) i1 i2
+ | TBinOp (Div, t1, t2) ->
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
+ Error.map2 (lift_arith_binop Ival.div) i1 i2
+ | TBinOp (Mod, t1, t2) ->
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
+ Error.map2 (lift_arith_binop Ival.c_rem) i1 i2
+ | TBinOp (Shiftlt, t1, t2) ->
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
+ Error.map2 (lift_arith_binop Ival.shift_left) i1 i2
+ | TBinOp (Shiftrt, t1, t2) ->
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
+ Error.map2 (lift_arith_binop Ival.shift_right) i1 i2
+ | TBinOp (BAnd, t1, t2) ->
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
+ Error.map2 (lift_arith_binop Ival.bitwise_and) i1 i2
+ | TBinOp (BXor, t1, t2) ->
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
+ Error.map2 (lift_arith_binop Ival.bitwise_xor) i1 i2
+ | TBinOp (BOr, t1, t2) ->
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
+ Error.map2 (lift_arith_binop Ival.bitwise_or) i1 i2
+ | TCastE (ty, t) ->
+ let src = infer ~force ~logic_env t in
+ let dst = interv_of_typ ty in
+ Error.map (fun src -> cast ~src ~dst) src
+ | Tif (t1, t2, t3) ->
+ ignore (infer ~force ~logic_env t1);
+ let i2 = infer ~force ~logic_env t2 in
+ let i3 = infer ~force ~logic_env t3 in
+ Error.map2 join i2 i3
+ | Tat (t, _) ->
+ get_res (infer ~force ~logic_env t)
+ | TBinOp (MinusPP, t1, t2) ->
+ ignore (infer ~force ~logic_env t1);
+ ignore (infer ~force ~logic_env t2);
+ (match Cil.unrollType (get_cty t1) with
+ | TArray(_, _, _) as ta ->
+ begin
+ try
+ let n = Cil.bitsSizeOf ta in
+ (* 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
+ ival Integer.zero (Integer.of_int nb_bytes)
+ with Cil.SizeOfError _ ->
+ Lazy.force interv_of_unknown_block
+ end
+ | TPtr _ -> Lazy.force interv_of_unknown_block
+ | _ -> assert false)
+ | Tblock_length (_, t)
+ | Toffset(_, t) ->
+ ignore (infer ~force ~logic_env t);
+ (match Cil.unrollType (get_cty t) with
+ | TArray(_, _, _) as ta ->
+ begin
+ try
+ let n = Cil.bitsSizeOf ta in
+ let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
+ singleton_of_int nb_bytes
+ with Cil.SizeOfError _ ->
+ Lazy.force interv_of_unknown_block
+ end
+ | TPtr _ -> Lazy.force interv_of_unknown_block
+ | _ -> assert false)
+ | Tnull -> singleton_of_int 0
+ | TLogic_coerce (_, t) -> get_res (infer ~force ~logic_env t)
+ | Tapp (li,_,args) ->
+ (match li.l_body with
+ | LBpred _ | LBterm _ ->
+ let profile =
+ Profile.make
+ li.l_profile
+ (List.map
+ (fun arg -> get_res (infer ~force ~logic_env arg))
+ args)
in
- if is_included then begin
- List.iter (fun lv -> Env.remove lv) li.l_profile;
- new_i
- end else
- let i = infer t' in
- List.iter (fun lv -> Env.remove lv) li.l_profile;
- fixpoint i
- in
- fixpoint bottom
- | LBnone when li.l_var_info.lv_name = "\\sum" ||
- li.l_var_info.lv_name = "\\product" ->
- (match args with
- | [ t1; t2; { term_node = Tlambda([ k ], _) } as lambda ] ->
- let t1_iv = infer t1 in
- let t2_iv = infer t2 in
- let k_iv = join t1_iv t2_iv in
- Env.add k k_iv;
- let lambda_iv = infer lambda in
- Env.remove k;
- let t2incr =
- Logic_const.term (TBinOp(PlusA, t2, Cil.lone ())) Linteger
- in
- (* it is correct and precise to use k_ival to compute lambda_ival, but
- not during the code generation since the type used for k is the
- greatest type between the type of t1 and the type of t2+1, that is
- why the ival associated to k is updated *)
- Env.add k (join t1_iv (infer t2incr));
- (* k is removed during code generation, it is needed for generating
- the code of the lambda term *)
- infer_sum_product li.l_var_info lambda_iv t1_iv t2_iv
- | _ -> Error.not_yet "extended quantifiers without lambda term")
- | LBnone when li.l_var_info.lv_name = "\\numof" ->
- (match args with
- | [ t1; t2; { term_node = Tlambda([ k ], p) } ] ->
- let logic_info = Cil_const.make_logic_info "\\sum" in
- logic_info.l_type <- li.l_type;
- logic_info.l_tparams <- li.l_tparams;
- logic_info.l_labels <- li.l_labels;
- logic_info.l_profile <- li.l_profile;
- logic_info.l_body <- li.l_body;
- let numof_as_sum =
- let conditional_term =
- Logic_const.term
- (Tif(p, Cil.lone (), Cil.lzero ())) Linteger
- in
- let lambda_term =
- Logic_const.term (Tlambda([ k ], conditional_term)) Linteger
+ (match li.l_body with
+ | LBpred p ->
+ let logic_env = Logic_env.make profile in
+ ignore (infer_predicate ~logic_env p);
+ Ival Ival.zero_or_one
+ | LBterm t' when LF_env.is_rec li ->
+ let widened_profile = widen_profile profile in
+ Widened_profile.add profile li widened_profile;
+ (try LF_env.find li widened_profile
+ with Not_found ->
+ fixpoint ~infer li widened_profile t' (Ival Ival.bottom))
+ | LBterm t' ->
+ let logic_env = Logic_env.make profile in
+ (* If the logic function returns a C type, then its application
+ ranges inside this C type *)
+ (match li.l_type with
+ | Some (Ctype typ) ->
+ ignore ((infer ~force ~logic_env t'));
+ interv_of_typ typ;
+ | None | Some (Linteger | Lreal | Ltype _ | Lvar _ | Larrow _) ->
+ get_res (infer ~force ~logic_env t'))
+ | _ -> assert false)
+ | LBnone when li.l_var_info.lv_name = "\\sum" ||
+ li.l_var_info.lv_name = "\\product" ->
+ (match args with
+ | [ t1; t2; { term_node = Tlambda([ k ], _) } as lambda ] ->
+ let t1_iv = infer ~force ~logic_env t1 in
+ let t2_iv = infer ~force ~logic_env t2 in
+ let k_iv = Error.map2 join t1_iv t2_iv in
+ let logic_env_with_k =
+ Logic_env.add logic_env k k_iv
in
- (Logic_const.term
- (Tapp(logic_info, lst, [ t1; t2; lambda_term ])) Linteger)
- in infer numof_as_sum
- | _ ->
- Options.fatal "unexpected input for an extended quantifier \\numof")
- | LBnone
- | LBreads _ ->
- (match li.l_type with
- | None -> assert false
- | Some ret_type -> interv_of_logic_typ ret_type)
- | LBinductive _ ->
- Error.not_yet "logic functions inductively defined")
-
- | Tunion _ -> Error.not_yet "tset union"
- | Tinter _ -> Error.not_yet "tset intersection"
- | Tcomprehension (_,_,_) -> Error.not_yet "tset comprehension"
- | Trange(Some n1, Some n2) ->
- let i1 = infer n1 in
- let i2 = infer n2 in
- join i1 i2
- | Trange(None, _) | Trange(_, None) ->
- Options.abort "unbounded ranges are not part of E-ACSl"
-
- | Tlet (li, t) ->
- let li_t = Misc.term_of_li li in
- let li_v = li.l_var_info in
- let i1 = infer li_t in
- Env.add li_v i1;
- let i2 = infer t in
- Env.remove li_v;
- i2
- | TConst (LReal lr) ->
- if lr.r_lower = lr.r_upper then Float(FDouble, Some lr.r_nearest)
- else Rational
- | Tlambda ([ _ ],lt) ->
- infer lt
- | Tlambda (_,_)
- | TConst (LStr _ | LWStr _)
- | TBinOp (PlusPI,_,_)
- | TBinOp (MinusPI,_,_)
- | TAddrOf _
- | TStartOf _
- | TDataCons (_,_)
- | Tbase_addr (_,_)
- | TUpdate (_,_,_)
- | Ttypeof _
- | Ttype _
- | Tempty_set ->
- Nan
-
-and infer_term_lval (host, offset as tlv) =
+ let lambda_iv = infer ~force ~logic_env:logic_env_with_k lambda in
+ Error.map3 (infer_sum_product li.l_var_info) lambda_iv t1_iv t2_iv
+ | _ -> Error.not_yet "extended quantifiers without lambda term")
+ | LBnone
+ | LBreads _ ->
+ List.iter
+ (fun arg -> ignore (infer ~force ~logic_env arg))
+ args;
+ (match li.l_type with
+ | None -> assert false
+ | Some ret_type -> interv_of_logic_typ ret_type)
+ | LBinductive _ ->
+ Error.not_yet "logic functions inductively defined")
+
+ | Tunion _ -> Error.not_yet "tset union"
+ | Tinter _ -> Error.not_yet "tset intersection"
+ | Tcomprehension (_,_,_) -> Error.not_yet "tset comprehension"
+ | Trange(Some n1, Some n2) ->
+ let i1 = infer ~force ~logic_env n1 in
+ let i2 = infer ~force ~logic_env n2 in
+ Error.map2 join i1 i2
+ | Trange(None, _) | Trange(_, None) ->
+ Options.abort "unbounded ranges are not part of E-ACSl"
+
+ | Tlet (li,t) ->
+ let li_t = Misc.term_of_li li in
+ let li_v = li.l_var_info in
+ let i1 = infer ~force ~logic_env li_t in
+ let logic_env =
+ Error.map (Logic_env.add logic_env li_v) i1
+ in
+ get_res (infer ~force ~logic_env t)
+ | TConst (LReal lr) ->
+ if lr.r_lower = lr.r_upper then Float(FDouble, Some lr.r_nearest)
+ else Rational
+ | Tlambda ([ _ ],lt) ->
+ get_res (infer ~force ~logic_env lt)
+
+ | TStartOf lv
+ | TAddrOf lv ->
+ ignore (infer_term_lval ~force ~logic_env lv);
+ Nan
+
+ | TBinOp (PlusPI, t1 ,t2)
+ | TBinOp (MinusPI, t1, t2) ->
+ ignore (infer ~force ~logic_env t1);
+ ignore (infer ~force ~logic_env t2);
+ Nan
+
+ | Tbase_addr (_,t)
+ | Ttypeof t ->
+ ignore (infer ~force ~logic_env t);
+ Nan
+
+ |TDataCons(_,l) ->
+ List.iter (fun t -> ignore (infer ~force ~logic_env t)) l;
+ Nan
+
+ | TUpdate(t1, toff, t2) ->
+ ignore (infer ~force ~logic_env t1);
+ ignore (infer ~force ~logic_env t2);
+ infer_term_offset ~force ~logic_env toff;
+ Nan
+
+ | Tlambda (_,_)
+ | TConst (LStr _ | LWStr _)
+ | Ttype _
+ | Tempty_set ->
+ Nan
+ in
+ Memo.memo
+ ~force_infer:force
+ (Logic_env.get_profile logic_env)
+ compute
+ t
+
+and infer_term_lval ~force ~logic_env (host, offset as tlv) =
match offset with
- | TNoOffset -> infer_term_host host
+ | TNoOffset -> infer_term_host ~force ~logic_env host
| _ ->
+ ignore (infer_term_host ~force ~logic_env host);
+ infer_term_offset ~force ~logic_env offset;
let ty = Logic_utils.logicCType (Cil.typeOfTermLval tlv) in
interv_of_typ ty
-and infer_term_host thost =
+and infer_term_host ~force ~logic_env thost =
match thost with
| TVar v ->
- (try Env.find v with Not_found ->
+ (try Logic_env.find logic_env v with Not_found ->
match v.lv_type with
| Linteger -> top_ival
| Ctype (TFloat(fk, _)) -> Float(fk, None)
@@ -880,6 +863,7 @@ and infer_term_host thost =
| TResult ty ->
interv_of_typ ty
| TMem t ->
+ ignore (infer ~force ~logic_env t);
let ty = Logic_utils.logicCType t.term_type in
match Cil.unrollType ty with
| TPtr(ty, _) | TArray(ty, _, _) ->
@@ -889,12 +873,213 @@ and infer_term_host thost =
Printer.pp_typ ty
Printer.pp_term t
+
+and infer_term_offset ~force ~logic_env t =
+ match t with
+ | TNoOffset -> ()
+ | TField(_, toff)
+ | TModel(_, toff) -> infer_term_offset ~force ~logic_env toff
+ | TIndex(t, toff) ->
+ ignore (infer ~force ~logic_env t);
+ infer_term_offset ~force ~logic_env toff
+
+(* [type_bound_variables] infers an interval associated with each of
+ the provided bounds of a quantified variable, and provides a term
+ accordingly. It could happen that the bounds provided for a quantifier
+ [lv] are bigger than its type. [type_bound_variables] handles such cases
+ and provides smaller bounds whenever possible.
+ Let B be the inferred interval and R the range of [lv.typ]
+ - Case 1: B \subseteq R
+ Example: [\forall unsigned char c; 4 <= c <= 100 ==> 0 <= c <= 255]
+ Return: B
+ - Case 2: B \not\subseteq R and the bounds of B are inferred exactly
+ Example: [\forall unsigned char c; 4 <= c <= 300 ==> 0 <= c <= 255]
+ Return: B \intersect R
+ - Case 3: B \not\subseteq R and the bounds of B are NOT inferred exactly
+ Example: [\let m = n > 0 ? 4 : 341; \forall char u; 1 < u < m ==> u > 0]
+ Return: R with a guard guaranteeing that [lv] does not overflow *)
+and infer_bound_variable ~loc ~logic_env (t1, lv, t2) =
+ let get_res = Error.map (fun x -> x) in
+ let i1 = get_res (infer ~force:false ~logic_env t1) in
+ let i2 = get_res (infer ~force:false ~logic_env t2) in
+ let i = widen (join i1 i2) in
+ let t1, t2, i =
+ match lv.lv_type with
+ | Ltype _ | Lvar _ | Lreal | Larrow _ ->
+ Error.not_yet "quantification over non-integer type"
+ | Linteger -> t1, t2, i
+ | Ctype ty ->
+ let ity = extended_interv_of_typ ty in
+ if is_included i ity then
+ (* case 1 *)
+ t1, t2, i
+ else if is_singleton_int i1 &&
+ is_singleton_int i2 then
+ begin
+ (* case 2 *)
+ let i = meet i ity in
+ (* We can now update the bounds in the preprocessed form
+ that come from the meet of the two intervals *)
+ let min, max = Misc.finite_min_and_max (extract_ival i) in
+ let t1 = Logic_const.tint ~loc min in
+ let t2 = Logic_const.tint ~loc max in
+ t1, t2, i
+ end else
+ (* case 3 *)
+ let min, max = Misc.finite_min_and_max (extract_ival 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 (Rlt, lv_term, guard_upper) in
+ let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
+ ignore (infer_predicate ~logic_env guard);
+ Bound_variables.add_guard_for_small_type lv guard;
+ t1, t2, i
+ in
+ ignore (infer ~force:false ~logic_env t1);
+ ignore (infer ~force:false ~logic_env t2);
+ Logic_env.add logic_env lv i, (t1, lv, t2)
+
+and infer_predicate ~logic_env p =
+ let get_res = Error.map (fun x -> x) in
+ let p = Logic_normalizer.get_pred p in
+ match p.pred_content with
+ | Pfalse | Ptrue -> ()
+ | Papp(li, _, args) ->
+ (match li.l_body with
+ | LBpred p ->
+ let profile =
+ Profile.make
+ li.l_profile
+ (List.map
+ (fun arg -> get_res (infer ~force:false ~logic_env arg))
+ args)
+ in
+ let logic_env = Logic_env.make profile in
+ ignore (infer_predicate ~logic_env p)
+ | LBnone -> ()
+ | LBreads _ -> ()
+ | LBinductive _ -> ()
+ | LBterm _ ->
+ Options.fatal "unexpected logic definition"
+ Printer.pp_predicate p
+ )
+ | Pdangling _ -> ()
+ | Prel(_, t1, t2) ->
+ ignore (infer ~force:false ~logic_env t1);
+ ignore (infer ~force:false ~logic_env t2)
+ | Pand(p1, p2)
+ | Por(p1, p2)
+ | Pxor(p1, p2)
+ | Pimplies(p1, p2)
+ | Piff(p1, p2) ->
+ infer_predicate ~logic_env p1;
+ infer_predicate ~logic_env p2
+ | Pnot p ->
+ infer_predicate ~logic_env p;
+ | Pif(t, p1, p2) ->
+ ignore (infer ~force:false ~logic_env t);
+ infer_predicate ~logic_env p1;
+ infer_predicate ~logic_env p2
+ | Plet(li, p) ->
+ let li_t = Misc.term_of_li li in
+ let li_v = li.l_var_info in
+ let i = infer ~force:false ~logic_env li_t in
+ let logic_env =
+ Error.map (Logic_env.add logic_env li_v) i
+ in
+ infer_predicate ~logic_env p
+ | Pforall _
+ | Pexists _ ->
+ let guards, goal =
+ Error.retrieve_preprocessing
+ "quantified predicate"
+ Bound_variables.get_preprocessed_quantifier
+ p
+ Printer.pp_predicate
+ in
+ let loc = p.pred_loc in
+ let rec do_analysis guards new_guards logic_env =
+ match guards with
+ | [] -> logic_env, new_guards
+ | guard :: guards ->
+ let logic_env, new_guard =
+ infer_bound_variable ~loc ~logic_env guard
+ in
+ do_analysis guards (new_guard :: new_guards) logic_env
+ in
+ let logic_env, new_guards = do_analysis guards [] logic_env in
+ Bound_variables.replace p new_guards goal;
+ infer_predicate ~logic_env goal
+ | Pseparated tlist ->
+ List.iter
+ (fun t -> ignore (infer ~force:false ~logic_env t))
+ tlist;
+ | Pinitialized(_, t)
+ | Pfreeable(_, t)
+ | Pallocable(_, t)
+ | Pvalid(_, t)
+ | Pvalid_read(_, t)
+ | Pobject_pointer(_,t)
+ | Pvalid_function t ->
+ ignore (infer ~force:false ~logic_env t);
+ | Pat(p, _) -> infer_predicate ~logic_env p
+ | Pfresh _ -> Error.not_yet "\\fresh"
+
let infer t =
let i = infer t in
- Logic_function_env.clear();
i
-include D
+include Ival_datatype
+
+let typer_visitor ~logic_env = object
+ inherit E_acsl_visitor.visitor dkey
+
+ (* global logic functions and predicates are evaluated are callsites *)
+ method !glob_annot _ = Cil.SkipChildren
+
+ method !vpredicate p =
+ (* Do not raise a warning for e-acsl errors at preprocessing time,
+ those errrors are stored in the table and warnings are raised at
+ translation time *)
+ (try infer_predicate ~logic_env p
+ with Error.Not_yet _ | Error.Typing_error _ -> ());
+ Cil.SkipChildren
+end
+
+let infer_program ast =
+ let visitor = typer_visitor ~logic_env:Logic_env.empty in
+ visitor#visit_file ast
+
+let preprocess_predicate ~logic_env p =
+ let visitor = typer_visitor ~logic_env in
+ ignore @@ visitor#visit_predicate p
+
+let preprocess_code_annot ~logic_env annot =
+ let visitor = typer_visitor ~logic_env in
+ ignore @@ visitor#visit_code_annot annot
+
+let preprocess_term ~logic_env t =
+ ignore (infer ~force:false ~logic_env t)
+
+let get_from_profile ~profile t =
+ let t = Logic_normalizer.get_term t in
+ Error.retrieve_preprocessing
+ "Interval inference"
+ (Memo.get profile)
+ t
+ Printer.pp_term
+
+let get ~logic_env =
+ get_from_profile ~profile:(Logic_env.get_profile logic_env)
+
+let get_widened_profile = Widened_profile.get
+
+let clear () =
+ Memo.clear();
+ Widened_profile.clear();
+ LF_env.clear()
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/analyses/interval.mli b/src/plugins/e-acsl/src/analyses/interval.mli
index ce2b899276fde8941cdc505c7f74f87d2d14c284..9e4d32ae02e25db53a27eb7b9bd6aae0110d8b9d 100644
--- a/src/plugins/e-acsl/src/analyses/interval.mli
+++ b/src/plugins/e-acsl/src/analyses/interval.mli
@@ -47,17 +47,12 @@
Note: this is a partial wrapper on top of [Ival.t], to which most
functions are delegated. *)
+open Analyses_types
+open Analyses_datatype
+
(* ************************************************************************** *)
(** {3 Useful operations on intervals} *)
(* ************************************************************************** *)
-
-type ival =
- | Ival of Ival.t
- | Float of Cil_types.fkind * float option
- | Rational
- | Real
- | Nan
-
type t = ival
val is_included: t -> t -> bool
@@ -88,28 +83,50 @@ val extended_interv_of_typ: Cil_types.typ -> t
@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. *)
-
-(* ************************************************************************** *)
-(** {3 Environment for interval computations} *)
-(* ************************************************************************** *)
-
-(** Environment which maps logic variables to intervals. This environment must
- be extended from outside. *)
-module Env: sig
- val clear: unit -> unit
- val add: Cil_types.logic_var -> t -> unit
- val remove: Cil_types.logic_var -> unit
-end
+val plus_one : ival -> ival
+(** @return the result of adding one to an interval. This is because when we
+ have a condition [x<t], we need to generate [t+1] *)
(* ************************************************************************** *)
(** {3 Inference system} *)
(* ************************************************************************** *)
+(* The inference phase infers the smallest possible integer interval which the
+ values of the term can fit in. *)
-val infer: Cil_types.term -> t
-(** [infer t] infers the smallest possible integer interval which the values
- of the term can fit in.
+val get_from_profile: profile:Profile.t -> Cil_types.term -> t
+(** @return the value computed by the interval inference phase
@raise Is_a_real if the term is either a float or a real.
- @raise Not_a_number if the term does not represent any number. *)
+ @raise Not_a_number if the term does not represent any
+ number.*)
+
+val get: logic_env:Logic_env.t -> Cil_types.term -> t
+(** @return the value computed by the interval inference phase, same as
+ [get_from_profile] but with a full-fledged logic environment instead of a
+ function profile *)
+
+
+(*****************************************************************************)
+(** {2 Interval processing} *)
+(*****************************************************************************)
+
+val infer_program : Cil_types.file -> unit
+(** compute and store the type of all the terms that will be translated
+ in a program *)
+
+val preprocess_predicate :
+ logic_env:Logic_env.t -> Cil_types.predicate -> unit
+(** compute and store the type of all the terms in a code annotation *)
+
+val preprocess_code_annot :
+ logic_env:Logic_env.t -> Cil_types.code_annotation -> unit
+(** compute and store the type of all the terms in a code annotation *)
+
+val preprocess_term :
+ logic_env:Logic_env.t -> Cil_types.term -> unit
+
+val get_widened_profile : Profile.t -> Cil_types.logic_info -> Profile.t
+
+val clear : unit -> unit
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index 9567ecc3fe2f94115cbe8823e771c2aacc03a7bb..1b0830126927676e793b79ea589dc27bde37cdb4 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -493,7 +493,8 @@ module rec Transfer
in
if stmt.ghost then
let rtes = Rte.stmt kf stmt in
- List.iter (Typing.preprocess_rte ~lenv:[]) rtes;
+ let logic_env = Analyses_datatype.Logic_env.empty in
+ List.iter (Typing.preprocess_rte ~logic_env) rtes;
List.fold_left
(fun state a -> register_code_annot kf a state) state rtes
else
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index d4022ccc0b1b038eddc2b4324531bbb5bda60532..83e9a80da29b0d96972a8a25e8668cb0ac2ad65e 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -21,6 +21,8 @@
(**************************************************************************)
open Cil_types
+open Analyses_types
+open Analyses_datatype
(* Implement Figure 4 of J. Signoles' JFLA'15 paper "Rester statique pour
devenir plus rapide, plus précis et plus mince". *)
@@ -41,14 +43,6 @@ let pending_typing : (unit -> unit) Stack.t = Stack.create ()
(** Datatype and constructor *)
(******************************************************************************)
-type number_ty =
- | C_integer of ikind
- | C_float of fkind
- | Gmpz
- | Rational
- | Real
- | Nan
-
let ikind ik = C_integer ik
let c_int = ikind IInt
let gmpz = Gmpz
@@ -56,60 +50,6 @@ let fkind fk = C_float fk
let rational = Rational
let nan = Nan
-module D =
- Datatype.Make_with_collections
- (struct
- type t = number_ty
- let name = "E_ACSL.Typing.t"
- let reprs = [ Gmpz; Real; Nan; c_int ]
- include Datatype.Undefined
-
- let compare ty1 ty2 =
- if ty1 == ty2 then 0
- else
- match ty1, ty2 with
- | C_integer i1, C_integer i2 ->
- if i1 = i2 then 0
- else if Cil.intTypeIncluded i1 i2 then -1 else 1
- | 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
- | (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
- | Rational, Rational
- | Real, Real
- | Nan, Nan ->
- assert false
-
- let equal = Datatype.from_compare
-
- let hash = function
- | 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_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)
-
(******************************************************************************)
(** Basic operations *)
(******************************************************************************)
@@ -131,7 +71,9 @@ let join ty1 ty2 =
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
+ Options.fatal "[typing] join failure: number %a and nan"
+ Number_ty.pretty
+ ty
| Real, (C_integer _ | C_float _ | Gmpz | Rational)
| (C_integer _ | C_float _ | Rational | Gmpz), Real ->
Real
@@ -173,34 +115,21 @@ let typ_of_lty = function
(******************************************************************************)
type computed_info =
- { ty: D.t; (* type required for the term *)
- op: D.t; (* type required for the operation *)
- cast: D.t option; (* if not [None], type of the context which the term
- must be casted to. If [None], no cast needed. *)
+ { ty: Number_ty.t; (* type required for the term *)
+ op: Number_ty.t; (* type required for the operation *)
+ cast: Number_ty.t option; (* if not [None], type of the context which the term
+ must be casted to. If [None], no cast needed. *)
}
-(* Local environement = list of typed variables *)
-module Function_params_ty =
- Datatype.List_with_collections
- (D)
- (struct let module_name = "E_ACSL.Typing.Function_params_ty" end)
-
-module Id_term_with_lenv =
- Datatype.Pair_with_collections
- (Misc.Id_term)
- (Function_params_ty)
- (struct let module_name = "E_ACSL.Typing.Id_term_with_lenv" end)
-
(* Memoization module which retrieves the computed info of some terms. If the
info is already computed for a term, it is never recomputed *)
module Memo: sig
val memo:
- lenv:Function_params_ty.t ->
+ profile: Profile.t ->
(term -> computed_info) ->
term ->
computed_info Error.result
- val get: lenv:Function_params_ty.t -> term ->
- computed_info Error.result
+ val get: profile: Profile.t -> term -> computed_info Error.result
val clear: unit -> unit
end = struct
@@ -231,21 +160,21 @@ end = struct
We distinguish the calls to the function by storing the type of the
arguments corresponding to each call, and we weaken the typing so that it
is invariant when the arguments have the same type. *)
- let dep_tbl : computed_info Error.result Id_term_with_lenv.Hashtbl.t
- = Id_term_with_lenv.Hashtbl.create 97
+ let dep_tbl : computed_info Error.result Id_term_in_profile.Hashtbl.t
+ = Id_term_in_profile.Hashtbl.create 97
- let get_dep lenv t =
- try Id_term_with_lenv.Hashtbl.find dep_tbl (t,lenv)
+ let get_dep profile t =
+ try Id_term_in_profile.Hashtbl.find dep_tbl (t,profile)
with Not_found -> Error.not_memoized ()
let get_nondep t =
try Misc.Id_term.Hashtbl.find tbl t
with Not_found -> Error.not_memoized ()
- let get ~lenv t =
- match lenv with
- | [] -> get_nondep t
- | _::_ -> get_dep lenv t
+ let get ~profile t =
+ if Profile.is_empty profile
+ then get_nondep t
+ else get_dep profile t
let memo_nondep f t =
try Misc.Id_term.Hashtbl.find tbl t
@@ -257,26 +186,26 @@ end = struct
Misc.Id_term.Hashtbl.add tbl t x;
x
- let memo_dep f t lenv =
+ let memo_dep f t profile =
try
- Id_term_with_lenv.Hashtbl.find dep_tbl (t, lenv)
+ Id_term_in_profile.Hashtbl.find dep_tbl (t, profile)
with Not_found ->
let x =
try Result.Ok (f t)
with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Error exn
in
- Id_term_with_lenv.Hashtbl.add dep_tbl (t, lenv) x;
+ Id_term_in_profile.Hashtbl.add dep_tbl (t, profile) x;
x
- let memo ~lenv f t =
- match lenv with
- | [] -> memo_nondep f t
- | _::_ -> memo_dep f t lenv
+ let memo ~profile f t =
+ if Profile.is_empty profile
+ then memo_nondep f t
+ else memo_dep f t profile
let clear () =
Options.feedback ~dkey ~level:4 "clearing the typing tables";
Misc.Id_term.Hashtbl.clear tbl;
- Id_term_with_lenv.Hashtbl.clear dep_tbl
+ Id_term_in_profile.Hashtbl.clear dep_tbl
end
@@ -284,14 +213,23 @@ end
(** {2 Coercion rules} *)
(******************************************************************************)
+let assert_nan = function
+ | Nan -> ()
+ | C_integer _
+ | C_float _
+ | Gmpz
+ | Rational
+ | Real -> Options.abort "got a number type where NaN was expected"
+
+
(* 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 ?(use_gmp_opt = false) = function
- | Interval.Float(fk, _) -> C_float fk
- | Interval.Rational -> Rational
- | Interval.Real -> Real
- | Interval.Nan -> Nan
- | Interval.Ival iv ->
+ | Float(fk, _) -> C_float fk
+ | Rational -> Rational
+ | Real -> Real
+ | Nan -> Nan
+ | Ival iv ->
try
let kind = Interval.ikind_of_ival iv in
(match ctx with
@@ -315,7 +253,7 @@ let ty_of_interv ?ctx ?(use_gmp_opt = false) = function
(* compute a new {!computed_info} by coercing the given type [ty] to the given
context [ctx]. [op] is the type for the operator. *)
let coerce ~arith_operand ~ctx ~op ty =
- if D.compare ty ctx = 1 then
+ if Number_ty.compare ty ctx = 1 then
(* type larger than the expected context,
so we must introduce an explicit cast *)
{ ty; op; cast = Some ctx }
@@ -339,7 +277,7 @@ let number_ty_of_typ ~post ty =
| TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ -> Nan
| TNamed _ -> assert false
-let ty_of_logic_ty ?term lty =
+let ty_of_logic_ty ?term ~profile lty =
let get_ty = function
| Linteger -> Gmpz
| Ctype ty -> number_ty_of_typ ~post:false ty
@@ -353,7 +291,7 @@ let ty_of_logic_ty ?term lty =
| Some t ->
if Options.Gmp_only.get () && lty = Linteger then Gmpz
else
- let i = Interval.infer t in
+ let i = Interval.get_from_profile ~profile t in
ty_of_interv i
(******************************************************************************)
@@ -371,19 +309,33 @@ let mk_ctx ~use_gmp_opt = function
else c
| Gmpz | Rational | Real | Nan as c -> c
+(* If a term has a C type, return it when it is smaller than [int] or [int], \
+ return [None] if the term has no C type *)
+let c_type_or_int_in_ival_of t i =
+ let t = Logic_utils.remove_logic_coerce t in
+ match t.term_type with
+ | Ctype typ ->
+ (match Cil.unrollType typ with
+ | TInt (ik, _) | TEnum({ ekind = ik }, _) when
+ Interval.is_included i (Interval.interv_of_typ typ)
+ ->
+ if Cil.intTypeIncluded ik IInt
+ then Some (C_integer IInt)
+ else Some (C_integer ik)
+ | TInt _ | TEnum _ | TFloat _ | TVoid _ | TPtr _ | TArray _ | TFun _
+ | TComp _ | TBuiltin_va_list _ -> None
+ | TNamed _ -> assert false)
+ | _ -> None
+
(* 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 =
- let i = Interval.infer t in
+let type_offset ~profile t =
+ let i = Interval.get_from_profile ~profile 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. *)
let rec type_term
@@ -391,7 +343,7 @@ let rec type_term
?(under_lambda=false)
?(arith_operand=false)
?ctx
- ~lenv
+ ~profile
t =
let ctx = Option.map (mk_ctx ~use_gmp_opt) ctx in
let dup ty = ty, ty in
@@ -417,16 +369,20 @@ let rec type_term
| TSizeOf _
| TSizeOfStr _
| TAlignOf _ ->
- let i = Interval.infer t in
+ let i = Interval.get_from_profile ~profile t in
(* a constant or a left value directly under a lambda should be a gmp
if the infered context for the lambda is gmp *)
let ty = ty_of_interv ?ctx ~use_gmp_opt:under_lambda i in
dup ty
+ | TLval ((TVar {lv_type = Ctype (TInt (ik, _))}, _) as tlv) ->
+ type_term_lval ~profile tlv;
+ dup (C_integer ik)
+
| TLval tlv ->
- let i = Interval.infer t in
- let ty = ty_of_interv ?ctx ~use_gmp_opt:under_lambda i in
- type_term_lval ~lenv tlv;
+ let i = Interval.get_from_profile ~profile t in
+ let ty = ty_of_interv ?ctx ~use_gmp_opt:under_lambda i in
+ type_term_lval ~profile tlv;
(* Options.feedback "Type : %a" D.pretty ty; *)
dup ty
@@ -434,25 +390,25 @@ let rec type_term
| Tblock_length(_, t')
| TSizeOfE t'
| TAlignOfE t' ->
- let i = Interval.infer t in
+ let i = Interval.get_from_profile ~profile t in
(* [t'] must be typed, but it is a pointer *)
- ignore (type_term ~use_gmp_opt:true ~ctx:Nan ~lenv t');
+ ignore (type_term ~use_gmp_opt:true ~ctx:Nan ~profile t');
let ty = ty_of_interv ?ctx i in
dup ty
| TBinOp (MinusPP, t1, t2) ->
- let i = Interval.infer t in
+ let i = Interval.get_from_profile ~profile t in
(* [t1] and [t2] must be typed, but they are pointers *)
- ignore (type_term ~use_gmp_opt:true ~ctx:Nan ~lenv t1);
- ignore (type_term ~use_gmp_opt:true ~ctx:Nan ~lenv t2);
+ ignore (type_term ~use_gmp_opt:true ~ctx:Nan ~profile t1);
+ ignore (type_term ~use_gmp_opt:true ~ctx:Nan ~profile t2);
let ty = ty_of_interv ?ctx i in
dup ty
| TUnOp (unop, t') ->
- let i = Interval.infer t in
- let i' = Interval.infer t' in
+ let i = Interval.get_from_profile ~profile t in
+ let i' = Interval.get_from_profile ~profile 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 ~lenv t');
+ ignore (type_term ~use_gmp_opt:true ~arith_operand:true ~ctx ~profile t');
(match unop with
| LNot -> c_int, ctx_res (* converted into [t == 0] in case of GMP *)
| Neg | BNot -> dup ctx_res)
@@ -460,9 +416,9 @@ let rec type_term
| TBinOp ((PlusA | MinusA | Mult | Div | Mod | Shiftlt | Shiftrt | BAnd
| BOr | BXor), t1, t2)
->
- let i = Interval.infer t in
- let i1 = Interval.infer t1 in
- let i2 = Interval.infer t2 in
+ let i = Interval.get_from_profile ~profile t in
+ let i1 = Interval.get_from_profile ~profile t1 in
+ let i2 = Interval.get_from_profile ~profile t2 in
let ctx_res, ctx =
compute_ctx ?ctx (Interval.join i (Interval.join i1 i2))
in
@@ -476,20 +432,20 @@ let rec type_term
| _ -> true
in
let cast_first = cast_first t1 t2 in
- ignore (type_term ~use_gmp_opt:true ~arith_operand:cast_first ~ctx ~lenv t1);
ignore
- (type_term ~use_gmp_opt:true ~arith_operand:(not cast_first) ~ctx ~lenv t2);
+ (type_term ~use_gmp_opt:true ~arith_operand:cast_first ~ctx ~profile t1);
+ ignore
+ (type_term ~use_gmp_opt:true ~arith_operand:(not cast_first) ~ctx ~profile t2);
dup ctx_res
| 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 =
- mk_ctx ~use_gmp_opt:true (ty_of_interv ?ctx (Interval.join i1 i2))
- in
- ignore (type_term ~use_gmp_opt:true ~ctx ~lenv t1);
- ignore (type_term ~use_gmp_opt:true ~ctx ~lenv t2);
+ assert
+ (match ctx with
+ | None -> true
+ | Some c -> Number_ty.compare c c_int >= 0);
+ let ctx = ctx_relation ~profile t1 t2 in
+ ignore (type_term ~use_gmp_opt:true ~ctx ~profile t1);
+ ignore (type_term ~use_gmp_opt:true ~ctx ~profile t2);
let ty = match ctx with
| Nan -> c_int
| Real | Rational | Gmpz | C_float _ | C_integer _ -> ctx
@@ -497,57 +453,57 @@ let rec type_term
c_int, ty
| TBinOp ((LAnd | LOr), t1, t2) ->
- let i1 = Interval.infer t1 in
- let i2 = Interval.infer t2 in
+ let i1 = Interval.get_from_profile ~profile t1 in
+ let i2 = Interval.get_from_profile ~profile 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 ~lenv t1);
- ignore (type_term ~use_gmp_opt:true ~ctx:c_int ~lenv t2);
+ ignore (type_term ~use_gmp_opt:true ~ctx:c_int ~profile t1);
+ ignore (type_term ~use_gmp_opt:true ~ctx:c_int ~profile t2);
dup ty
| TCastE(_, t') ->
(* compute the smallest interval from the whole term [t] *)
- let i = Interval.infer t in
+ let i = Interval.get_from_profile ~profile 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 ~lenv t');
+ ignore (type_term ~use_gmp_opt:true ~ctx ~profile t');
dup ctx
| Tif (t1, t2, t3) ->
let ctx1 =
mk_ctx ~use_gmp_opt:false c_int (* an int must be generated *)
in
- ignore (type_term ~use_gmp_opt:false ~ctx:ctx1 ~lenv t1);
- let i = Interval.infer t in
- let i2 = Interval.infer t2 in
- let i3 = Interval.infer t3 in
+ ignore (type_term ~use_gmp_opt:false ~ctx:ctx1 ~profile t1);
+ let i = Interval.get_from_profile ~profile t in
+ let i2 = Interval.get_from_profile ~profile t2 in
+ let i3 = Interval.get_from_profile ~profile 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 ~lenv t2);
- ignore (type_term ~use_gmp_opt:true ~ctx ~lenv t3);
+ ignore (type_term ~use_gmp_opt:true ~ctx ~profile t2);
+ ignore (type_term ~use_gmp_opt:true ~ctx ~profile t3);
dup ctx
| Tat (t, _)
| TLogic_coerce (_, t) ->
- dup (type_term ~use_gmp_opt ~arith_operand ?ctx ~lenv t).ty
+ dup (type_term ~use_gmp_opt ~arith_operand ?ctx ~profile t).ty
| TAddrOf tlv
| TStartOf tlv ->
(* it is a pointer, but subterms must be typed. *)
- type_term_lval tlv ~lenv;
+ type_term_lval tlv ~profile;
dup Nan
| Tbase_addr (_, t) ->
(* it is a pointer, but subterms must be typed. *)
- ignore (type_term ~use_gmp_opt:true ~ctx:Nan ~lenv t);
+ ignore (type_term ~use_gmp_opt:true ~ctx:Nan ~profile t);
dup Nan
| TBinOp ((PlusPI | MinusPI), t1, t2) ->
(* both [t1] and [t2] must be typed. *)
- ignore (type_term ~use_gmp_opt:true ~ctx:Nan ~lenv t1);
- let ctx = type_offset t2 in
- ignore (type_term ~use_gmp_opt:false ~ctx ~lenv t2);
+ ignore (type_term ~use_gmp_opt:true ~ctx:Nan ~profile t1);
+ let ctx = type_offset ~profile t2 in
+ ignore (type_term ~use_gmp_opt:false ~ctx ~profile t2);
dup Nan
| Tapp(li, _, args) ->
@@ -555,13 +511,13 @@ let rec type_term
let typ_arg lvi arg =
(* a built-in is a C function, so the context is necessarily a C
type. *)
- let ctx = ty_of_logic_ty lvi.lv_type in
- ignore (type_term ~use_gmp_opt:false ~ctx ~lenv arg)
+ let ctx = ty_of_logic_ty ~profile lvi.lv_type in
+ ignore (type_term ~use_gmp_opt:false ~ctx ~profile arg)
in
List.iter2 typ_arg li.l_profile args;
(* [li.l_type is [None] for predicate only: not possible here.
Thus using [Option.get] is fine *)
- dup (ty_of_logic_ty (Option.get li.l_type))
+ dup (ty_of_logic_ty ~profile (Option.get li.l_type))
else begin
(* TODO: what if the type of the parameter is smaller than the infered
type of the argument? For now, it is silently ignored (both
@@ -571,70 +527,121 @@ let rec type_term
| LBpred p ->
(* possible to have an [LBpred] here because we transformed
[Papp] into [Tapp] *)
+ List.iter
+ (fun x ->
+ let ctx = match x.term_type with
+ | Linteger ->
+ (* If the function parameter is an integer,
+ the kernel introduces a coercion to integer, so we will
+ always see integer here.*)
+ begin match x.term_node with
+ |TLogic_coerce _ -> None
+ |_ -> if Options.Gmp_only.get() then Some Gmpz else None
+ end
+ | Lreal -> Some Real
+ | Ctype _| Ltype _| Larrow _ | Lvar _ -> None
+ in
+ ignore
+ (type_term
+ ~use_gmp_opt:true
+ ~under_lambda:true
+ ~arith_operand
+ ?ctx
+ ~profile x))
+ args;
+ let new_profile =
+ Profile.make
+ li.l_profile
+ (List.map (Interval.get_from_profile ~profile) args)
+ in
Stack.push
(fun () ->
- let typed_args =
- type_args
- ~use_gmp_opt
- ~lenv
- li.l_profile
- args
- li.l_var_info.lv_name
- in
- ignore (type_predicate ~lenv:typed_args p);
- List.iter Interval.Env.remove li.l_profile)
+ ignore (type_predicate ~profile:new_profile p))
pending_typing;
dup c_int
| LBterm t_body ->
- begin match li.l_type with
- | None ->
- assert false
- | Some lty ->
- (* TODO: what if the function returns a real? *)
- let ty = ty_of_logic_ty ~term:t lty in
- let type_args_and_body () =
- let typed_args =
- type_args
- ~use_gmp_opt
- ~lenv
- li.l_profile
- args
- li.l_var_info.lv_name
- in
- (* Since there are no global logic variables, the typing of the
- inner block of the function only depends on the function's
- own arguments, so the [~lenv] parameter gets replaced with
- the type of the parameters in the current function calls *)
- ignore (type_term ~use_gmp_opt ~lenv:typed_args t_body)
- in
- let clear_env () = List.iter Interval.Env.remove li.l_profile in
- Stack.push
- clear_env
- pending_typing;
- Stack.push
- type_args_and_body
- pending_typing;
- dup ty
- end
+ List.iter
+ (fun x ->
+ let ctx = match x.term_type with
+ | Linteger ->
+ (* If the function parameter is an integer,
+ the kernel introduces a coercion to integer, so we will
+ always see integer here.*)
+ begin match x.term_node with
+ | TLogic_coerce _ -> None
+ |_ -> if Options.Gmp_only.get() then Some Gmpz else None
+ end
+ | Lreal -> Some Real
+ | Ctype _| Ltype _| Larrow _ | Lvar _ -> None
+ in
+ ignore
+ (type_term
+ ~use_gmp_opt:true
+ ~under_lambda:true
+ ~arith_operand
+ ?ctx
+ ~profile x))
+ args;
+ let new_profile =
+ Profile.make
+ li.l_profile
+ (List.map (Interval.get_from_profile ~profile) args)
+ in
+ let new_profile = Interval.get_widened_profile new_profile li in
+ let gmp,ctx_body = match li.l_type with
+ | Some (Ctype typ) ->
+ false, Some (number_ty_of_typ ~post:false typ)
+ | _ ->
+ true, if Options.Gmp_only.get() then Some Gmpz else ctx
+ in
+ Stack.push
+ (fun () ->
+ ignore
+ (type_term
+ ~use_gmp_opt:false
+ ~under_lambda:true
+ ~arith_operand
+ ?ctx:ctx_body
+ ~profile:new_profile
+ t_body))
+ pending_typing;
+ (* If the logic function has a given C number type, we generate a
+ function returning this type, otherwise we use the interval
+ inference *)
+ (match li.l_type with
+ | Some (Ctype (TInt (ikind, _))) ->
+ dup (C_integer ikind)
+ | Some (Ctype (TFloat (fkind, _))) ->
+ dup (C_float fkind)
+ | None
+ | Some (Ctype (TVoid _
+ | TPtr _
+ | TEnum _
+ | TArray _
+ | TFun _
+ | TNamed _
+ | TComp _
+ | TBuiltin_va_list _))
+ | Some (Linteger | Lreal | Ltype _ | Lvar _ | Larrow _) ->
+ dup (ty_of_interv
+ ?ctx:ctx_body
+ ~use_gmp_opt:(gmp && use_gmp_opt)
+ (Interval.get_from_profile ~profile t)))
| LBnone ->
(match args with
| [ t1; t2; {term_node = Tlambda([ _ ], _)} as lambda ] ->
- let anonymous =
- Logic_const.term (TBinOp(PlusA, t2, Cil.lone ())) Linteger
- in
- let ty_bound = Interval.infer anonymous in
- let ty_bound =
- ty_of_interv (Interval.join ty_bound (Interval.infer t1))
- in
+ let range = Interval.(plus_one (get_from_profile ~profile t2)) in
+ let range = Interval.(join range (get_from_profile ~profile t1)) in
+ let range = ty_of_interv range in
ignore
(type_term
- ~use_gmp_opt:true ~arith_operand:true ~ctx:ty_bound ~lenv t1);
+ ~use_gmp_opt:true ~arith_operand:true ~ctx:range ~profile t1);
ignore
(type_term
- ~use_gmp_opt:true ~arith_operand:true ~ctx:ty_bound ~lenv t2);
- let ty = ty_of_interv (Interval.infer t) ~use_gmp_opt:true ?ctx in
- (* Options.feedback "type of extended quantifier: %a" D.pretty ty; *)
- ignore (type_term ~use_gmp_opt:true ?ctx ~lenv lambda);
+ ~use_gmp_opt:true ~arith_operand:true ~ctx:range ~profile t2);
+ let ival = Interval.get_from_profile ~profile t in
+ let ty = ty_of_interv ival ~use_gmp_opt:true ?ctx in
+ ignore (type_term ~use_gmp_opt:true ?ctx ~profile lambda);
dup ty
| [ ] | [ _ ] | [ _; _ ] | _ :: _ :: _ :: _ ->
(* TODO : improve error message to distinguish error messages
@@ -656,19 +663,18 @@ let rec type_term
| 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 ~lenv n1);
- ignore (type_term ~use_gmp_opt ~lenv n2);
- let i = Interval.infer t in
+ ignore (type_term ~use_gmp_opt ~profile n1);
+ ignore (type_term ~use_gmp_opt ~profile n2);
+ let i = Interval.get_from_profile ~profile t in
let ty = ty_of_interv ?ctx i in
dup ty
| Tlet(li, t) ->
let li_t = Misc.term_of_li li in
- type_letin li li_t;
- ignore (type_term ~use_gmp_opt:true ~lenv li_t);
- dup (type_term ~use_gmp_opt:true ?ctx ~lenv t).ty
+ ignore (type_term ~use_gmp_opt:true ~profile li_t);
+ dup (type_term ~use_gmp_opt:true ?ctx ~profile t).ty
| Tlambda ([ _ ],lt) ->
- dup (type_term ~use_gmp_opt:true ~under_lambda:true ?ctx ~lenv lt).ty;
+ dup (type_term ~use_gmp_opt:true ~under_lambda:true ?ctx ~profile lt).ty;
| Tlambda (_,_) -> Error.not_yet "lambda"
| TDataCons (_,_) -> Error.not_yet "datacons"
| TUpdate (_,_,_) -> Error.not_yet "update"
@@ -681,7 +687,7 @@ let rec type_term
in
let t = Logic_normalizer.get_term t in
match
- Memo.memo ~lenv
+ Memo.memo ~profile
(fun t ->
let ty, op = infer t in
match ctx with
@@ -692,127 +698,61 @@ let rec type_term
| Result.Ok res -> res
| Result.Error exn -> raise exn
-and type_term_lval ~lenv (host, offset) =
- type_term_lhost ~lenv host;
- type_term_offset ~lenv offset
+and type_term_lval ~profile (host, offset) =
+ type_term_lhost ~profile host;
+ type_term_offset ~profile offset
-and type_term_lhost ~lenv t = match t with
+and type_term_lhost ~profile t = match t with
| TVar _
| TResult _ -> ()
- | TMem t -> ignore (type_term ~use_gmp_opt:false ~ctx:Nan ~lenv t)
+ | TMem t ->
+ let computed_ty = type_term ~use_gmp_opt:false ~ctx:Nan ~profile t
+ in assert_nan computed_ty.ty
-and type_term_offset ~lenv t = match t with
+and type_term_offset ~profile t = match t with
| TNoOffset -> ()
| TField(_, toff)
- | TModel(_, toff) -> type_term_offset ~lenv toff
+ | TModel(_, toff) -> type_term_offset ~profile toff
| TIndex(t, toff) ->
- let ctx = type_offset t in
- ignore (type_term ~use_gmp_opt:false ~ctx ~lenv t);
- type_term_offset ~lenv toff
-
-and type_args params ~use_gmp_opt ~lenv args fname =
- try
- List.fold_right2
- (fun lv t (typed_args : Function_params_ty.t) ->
- let ty_arg = (type_term ~use_gmp_opt ~lenv t).ty in
- begin
- try
- let typ_arg = typ_of_number_ty ty_arg in
- Interval.Env.add lv (Interval.interv_of_typ typ_arg)
- with Not_a_number -> ()
- end;
- ty_arg :: typed_args)
- params
- args
- []
- with Invalid_argument _ ->
- Options.fatal "[Tapp] unexpected number of arguments when calling %s" fname
-
-(* [type_bound_variables] infers an interval associated with each of
- the provided bounds of a quantified variable, and provides a term
- accordingly. It could happen that the bounds provided for a quantifier
- [lv] are bigger than its type. [type_bound_variables] handles such cases
- and provides smaller bounds whenever possible.
- Let B be the inferred interval and R the range of [lv.typ]
- - Case 1: B \subseteq R
- Example: [\forall unsigned char c; 4 <= c <= 100 ==> 0 <= c <= 255]
- Return: B
- - Case 2: B \not\subseteq R and the bounds of B are inferred exactly
- Example: [\forall unsigned char c; 4 <= c <= 300 ==> 0 <= c <= 255]
- Return: B \intersect R
- - Case 3: B \not\subseteq R and the bounds of B are NOT inferred exactly
- Example: [\let m = n > 0 ? 4 : 341; \forall char u; 1 < u < m ==> u > 0]
- Return: R with a guard guaranteeing that [lv] does not overflow *)
-and type_bound_variables ~loc ~lenv (t1, lv, t2) =
- let i1 = Interval.infer t1 in
- let i2 = Interval.infer t2 in
+ let ctx = type_offset ~profile t in
+ ignore (type_term ~use_gmp_opt:false ~ctx ~profile t);
+ type_term_offset ~profile toff
+
+(* assign a number type to a variable bound by a quantifiers. See [ctx_relation]
+ for an explanation of the cases *)
+and number_ty_bound_variable ~profile (t1, lv, t2) =
+ let i1 = Interval.get_from_profile ~profile t1 in
+ let i2 = Interval.get_from_profile ~profile t2 in
let i = Interval.(widen (join i1 i2)) in
- let ctx = match lv.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, _) | TEnum({ ekind = ik }, _) ->
- mk_ctx ~use_gmp_opt:true (C_integer ik)
- | ty ->
- Options.fatal "unexpected C type %a for quantified variable %a"
- Printer.pp_typ ty
- Printer.pp_logic_var lv)
- | lty ->
- Options.fatal "unexpected logic type %a for quantified variable %a"
- Printer.pp_logic_type lty
- Printer.pp_logic_var lv
- in
- let t1, t2, i =
- match lv.lv_type with
- | Ltype _ | Lvar _ | Lreal | Larrow _ ->
- Error.not_yet "quantification over non-integer type"
- | Linteger -> t1, t2, i
- | Ctype ty ->
- let ity = Interval.extended_interv_of_typ ty in
- if Interval.is_included i ity then
- (* case 1 *)
- t1, t2, i
- else if Interval.is_singleton_int i1 &&
- Interval.is_singleton_int i2 then
- begin
- (* case 2 *)
- let i = Interval.meet i ity in
- (* We can now update the bounds in the preprocessed form
- that come from the meet of the two intervals *)
- let min, max = Misc.finite_min_and_max (Interval.extract_ival i) in
- let t1 = Logic_const.tint ~loc min in
- let t2 = Logic_const.tint ~loc max in
- t1, t2, i
- end else
- (* case 3 *)
- let min, max = Misc.finite_min_and_max (Interval.extract_ival 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 (Rlt, lv_term, guard_upper) in
- let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
- ignore (type_predicate ~lenv guard);
- Bound_variables.add_guard_for_small_type lv guard;
- t1, t2, i
- in
+ match lv.lv_type with
+ | Linteger ->
+ let ty =
+ match c_type_or_int_in_ival_of t2 i with
+ | Some ty -> ty
+ | None -> ty_of_interv ~ctx:Gmpz i
+ in mk_ctx ~use_gmp_opt:true ty
+ | Ctype ty ->
+ (match Cil.unrollType ty with
+ | TInt(ik, _) | TEnum({ ekind = ik}, _)-> join
+ (ty_of_interv i)
+ (mk_ctx ~use_gmp_opt:true (C_integer ik))
+ | ty ->
+ Options.fatal "unexpected C type %a for quantified variable %a"
+ Printer.pp_typ ty
+ Printer.pp_logic_var lv)
+ | lty ->
+ Options.fatal "unexpected logic type %a for quantified variable %a"
+ Printer.pp_logic_type lty
+ Printer.pp_logic_var lv
+
+and type_bound_variables ~profile (t1, lv, t2) =
+ let ctx = number_ty_bound_variable ~profile (t1, lv, t2) 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 ~lenv t1);
- ignore (type_term ~use_gmp_opt:false ~ctx ~lenv 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
- (* [ -\infty; +\infty ] *)
- | Gmpz -> Interval.Ival (Ival.inject_range None None)
- | C_float _ | Rational | Real | Nan ->
- Options.fatal "unexpected quantification over %a" D.pretty ctx
- in
- Interval.Env.add lv i;
- (t1, lv, t2)
+ ignore(type_term ~use_gmp_opt:false ~ctx ~profile t1);
+ ignore(type_term ~use_gmp_opt:false ~ctx ~profile t2)
-and type_predicate ~lenv p =
+and type_predicate ~profile p =
let p = Logic_normalizer.get_pred p in
Cil.CurrentLoc.set p.pred_loc;
(* this pattern matching also follows the formal rules of the JFLA's paper *)
@@ -823,16 +763,15 @@ and type_predicate ~lenv p =
begin
match li.l_body with
| LBpred p ->
- let typed_args =
- type_args
- ~use_gmp_opt:true
- ~lenv
+ List.iter
+ (fun x -> ignore (type_term ~use_gmp_opt: true ~profile x))
+ args;
+ let new_profile =
+ Profile.make
li.l_profile
- args
- li.l_var_info.lv_name
+ (List.map (Interval.get_from_profile ~profile) args)
in
- ignore (type_predicate ~lenv:typed_args p);
- List.iter Interval.Env.remove li.l_profile
+ ignore (type_predicate ~profile:new_profile p);
| LBnone -> ()
| LBreads _ -> ()
| LBinductive _ -> ()
@@ -843,12 +782,9 @@ and type_predicate ~lenv p =
c_int
| Pdangling _ -> Error.not_yet "\\dangling"
| Prel(_, t1, t2) ->
- 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 ~lenv t1);
- ignore (type_term ~use_gmp_opt:true ~ctx ~lenv t2);
+ let ctx = ctx_relation ~profile t1 t2 in
+ ignore (type_term ~use_gmp_opt:true ~ctx ~profile t1);
+ ignore (type_term ~use_gmp_opt:true ~ctx ~profile t2);
(match ctx with
| Nan -> c_int
| Real | Rational | Gmpz | C_float _ | C_integer _ -> ctx)
@@ -857,23 +793,22 @@ and type_predicate ~lenv p =
| Pxor(p1, p2)
| Pimplies(p1, p2)
| Piff(p1, p2) ->
- ignore (type_predicate ~lenv p1);
- ignore (type_predicate ~lenv p2);
+ ignore (type_predicate ~profile p1);
+ ignore (type_predicate ~profile p2);
c_int
| Pnot p ->
- ignore (type_predicate ~lenv p);
+ ignore (type_predicate ~profile p);
c_int
| Pif(t, p1, p2) ->
let ctx = mk_ctx ~use_gmp_opt:false c_int in
- ignore (type_term ~use_gmp_opt:false ~ctx ~lenv t);
- ignore (type_predicate ~lenv p1);
- ignore (type_predicate ~lenv p2);
+ ignore (type_term ~use_gmp_opt:false ~ctx ~profile t);
+ ignore (type_predicate ~profile p1);
+ ignore (type_predicate ~profile p2);
c_int
| Plet(li, p) ->
let li_t = Misc.term_of_li li in
- type_letin li li_t;
- ignore (type_term ~use_gmp_opt:true ~lenv li_t);
- (type_predicate ~lenv p).ty
+ ignore (type_term ~use_gmp_opt:true ~profile li_t);
+ (type_predicate ~profile p).ty
| Pforall _
| Pexists _ ->
begin
@@ -884,19 +819,14 @@ and type_predicate ~lenv p =
p
Printer.pp_predicate
in
- let guards =
- List.map
- (fun (t1, x, t2) ->
- type_bound_variables ~loc:p.pred_loc ~lenv (t1, x, t2))
- guards
- in Bound_variables.replace p guards goal;
- (type_predicate ~lenv goal).ty
+ List.iter
+ (fun (t1, x, t2) -> type_bound_variables ~profile (t1, x, t2))
+ guards;
+ (type_predicate ~profile goal).ty
end
| Pseparated tlist ->
List.iter
- (fun t ->
- ignore
- (type_term ~use_gmp_opt:false ~ctx:Nan ~lenv t))
+ (fun t -> ignore (type_term ~use_gmp_opt:false ~ctx:Nan ~profile t))
tlist;
c_int
| Pinitialized(_, t)
@@ -906,43 +836,67 @@ and type_predicate ~lenv p =
| Pvalid_read(_, t)
| Pobject_pointer(_,t)
| Pvalid_function t ->
- ignore (type_term ~use_gmp_opt:false ~ctx:Nan ~lenv t);
+ ignore (type_term ~use_gmp_opt:false ~ctx:Nan ~profile t);
c_int
- | Pat(p, _) -> (type_predicate ~lenv p).ty
+ | Pat(p, _) -> (type_predicate ~profile p).ty
| Pfresh _ -> Error.not_yet "\\fresh"
in
coerce ~arith_operand:false ~ctx:c_int ~op c_int
-let type_term ~use_gmp_opt ?ctx ~lenv t =
+(** When typing a binary relation, generate the context in which the relation
+ should be typed, to avoid spurious casts:
+ - Compute the union of the interval of the two terms
+ - Check if any of the term has a number C type that contains this union,
+ and if so use this C type, or [int] if this type is smaller than [int]
+ - Otherwise use the type corresponding to the union *)
+and ctx_relation ~profile t1 t2 =
+ let i1 = Interval.get_from_profile ~profile t1 in
+ let i2 = Interval.get_from_profile ~profile t2 in
+ let i = Interval.join i1 i2 in
+ let ty =
+ match c_type_or_int_in_ival_of t1 i, c_type_or_int_in_ival_of t2 i with
+ | Some ty, _
+ | None, Some ty -> ty
+ | None, None -> ty_of_interv ~ctx:c_int i
+ in mk_ctx ~use_gmp_opt:true ty
+
+let type_term ~use_gmp_opt ?ctx ~profile t =
Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
- Printer.pp_term t (Pretty_utils.pp_opt D.pretty) ctx;
- ignore (type_term ~use_gmp_opt ?ctx ~lenv t);
+ Printer.pp_term t (Pretty_utils.pp_opt Number_ty.pretty) ctx;
+ ignore (type_term ~use_gmp_opt ?ctx ~profile t);
while not (Stack.is_empty pending_typing) do
Stack.pop pending_typing ()
done
-let type_named_predicate ~lenv p =
+let type_named_predicate ~profile p =
Options.feedback ~dkey ~level:3 "typing predicate '%a'."
Printer.pp_predicate p;
- ignore (type_predicate ~lenv p);
+ ignore (type_predicate ~profile p);
while not (Stack.is_empty pending_typing) do
Stack.pop pending_typing ()
done
-let unsafe_set t ?ctx ~lenv ty =
+let unsafe_set t ?ctx ~logic_env ty =
+ let profile = Logic_env.get_profile logic_env in
let ctx = match ctx with None -> ty | Some ctx -> ctx in
let mk _ = coerce ~arith_operand:false ~ctx ~op:ty ty in
- ignore (Memo.memo mk ~lenv t)
+ ignore (Memo.memo mk ~profile t)
(******************************************************************************)
(** {2 Getters} *)
(******************************************************************************)
-let get_number_ty ~lenv t =
- (Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t Printer.pp_term).ty
-let get_integer_op ~lenv t =
- (Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t Printer.pp_term).op
-let get_integer_op_of_predicate ~lenv p = (type_predicate ~lenv p).op
+let get_number_ty ~logic_env t =
+ let profile = Logic_env.get_profile logic_env in
+ (Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term).ty
+
+let get_integer_op ~logic_env t =
+ let profile = Logic_env.get_profile logic_env in
+ (Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term).op
+
+let get_integer_op_of_predicate ~logic_env p =
+ let profile = Logic_env.get_profile logic_env in
+ (type_predicate ~profile p).op
(* {!typ_of_integer}, but handle the not-integer cases. *)
let extract_typ t ty =
@@ -956,30 +910,34 @@ let extract_typ t ty =
| Lvar _ -> Error.not_yet "unsupported logic type: type variable"
| Larrow _ -> Error.not_yet "unsupported logic type: type arrow"
-let get_typ ~lenv t =
+let get_typ ~logic_env t =
+ let profile = Logic_env.get_profile logic_env in
let info =
- Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t Printer.pp_term in
+ Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term in
extract_typ t info.ty
-let get_op ~lenv t =
+let get_op ~logic_env t =
+ let profile = Logic_env.get_profile logic_env in
let info =
- Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t Printer.pp_term in
+ Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term in
extract_typ t info.op
-let get_cast ~lenv t =
+let get_cast ~logic_env t =
+ let profile = Logic_env.get_profile logic_env in
let info =
- Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t Printer.pp_term in
+ Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term in
try Option.map typ_of_number_ty info.cast
with Not_a_number -> None
-let get_cast_of_predicate ~lenv p =
- let info = type_predicate ~lenv p in
+let get_cast_of_predicate ~logic_env p =
+ let profile = Logic_env.get_profile logic_env in
+ let info = type_predicate ~profile p in
try Option.map typ_of_number_ty info.cast
with Not_a_number -> assert false
let clear = Memo.clear
-let typing_visitor lenv = object
+let typing_visitor profile = object
inherit E_acsl_visitor.visitor dkey
(* global logic functions and predicates are evaluated are callsites *)
@@ -990,29 +948,38 @@ let typing_visitor lenv = object
those errrors are stored in the table and warnings are raised at
translation time *)
ignore
- (try type_named_predicate ~lenv p
+ (try type_named_predicate ~profile p
with Error.Not_yet _ | Error.Typing_error _ -> ());
Cil.SkipChildren
end
let type_program ast =
- let visitor = typing_visitor [] in
+ let visitor = typing_visitor Profile.empty in
visitor#visit_file ast
let type_code_annot lenv annot =
let visitor = typing_visitor lenv in
ignore @@ visitor#visit_code_annot annot
-let preprocess_predicate lenv p =
+let preprocess_predicate ~logic_env p =
Logic_normalizer.preprocess_predicate p;
Bound_variables.preprocess_predicate p;
- let visitor = typing_visitor lenv in
+ Interval.preprocess_predicate ~logic_env p;
+ let profile = Logic_env.get_profile logic_env in
+ let visitor = typing_visitor profile in
ignore @@ visitor#visit_predicate p
-let preprocess_rte ~lenv rte =
+let preprocess_rte ~logic_env rte =
Logic_normalizer.preprocess_annot rte;
Bound_variables.preprocess_annot rte;
- type_code_annot lenv rte
+ ignore (Interval.preprocess_code_annot ~logic_env rte);
+ let profile = Logic_env.get_profile logic_env in
+ type_code_annot profile rte
+
+let preprocess_term ~use_gmp_opt ?ctx ~logic_env t =
+ ignore (Interval.preprocess_term ~logic_env t);
+ let profile = Logic_env.get_profile logic_env in
+ ignore (type_term ~use_gmp_opt ?ctx ~profile t);
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index a54fadfc9bf016997a15aa4ea2f502a4cb4d4f6f..2fbf5e238a556a3b26055fbe8385b861392cd2c4 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -45,24 +45,13 @@
safely be computed in [int]: its result belongs to [[-2;4]]. *)
open Cil_types
+open Analyses_types
+open Analyses_datatype
(******************************************************************************)
(** {2 Datatypes} *)
(******************************************************************************)
-(** Possible types infered by the system. *)
-
-type number_ty = private
- | C_integer of ikind
- | C_float of fkind
- | Gmpz
- | Rational
- | Real
- | Nan
-
-module Function_params_ty:
- Datatype.S_with_collections with type t = number_ty list
-
(** {3 Smart constructors} *)
val c_int: number_ty
@@ -93,23 +82,13 @@ val join: number_ty -> number_ty -> number_ty
semi-lattice. If one of the argument is {!Other}, the function assumes that
the other argument is also {!Other}. In this case, the result is [Other]. *)
+val number_ty_bound_variable:
+ profile:Profile.t -> term * logic_var * term -> number_ty
+(** return the type of a quantified logic variable *)
+
(******************************************************************************)
(** {2 Typing} *)
(******************************************************************************)
-
-val type_term:
- use_gmp_opt:bool ->
- ?ctx:number_ty ->
- lenv:Function_params_ty.t ->
- term ->
- unit
-(** Compute the type of each subterm of the given term in the given context. If
- [use_gmp_opt] is false, then the conversion to the given context is done
- even if -e-acsl-gmp-only is set. *)
-
-val type_named_predicate: lenv:Function_params_ty.t -> predicate -> unit
-(** Compute the type of each term of the given predicate. *)
-
val clear: unit -> unit
(** Remove all the previously computed types. *)
@@ -119,35 +98,36 @@ val clear: unit -> unit
{!type_named_predicate} has been previously computed for the given term or
predicate. *)
-val get_number_ty: lenv:Function_params_ty.t -> term -> number_ty
+val get_number_ty: logic_env:Logic_env.t -> term -> number_ty
(** @return the infered type for the given term. *)
-val get_integer_op: lenv:Function_params_ty.t -> term -> number_ty
+val get_integer_op: logic_env:Logic_env.t -> term -> number_ty
(** @return the infered type for the top operation of the given term.
It is meaningless to call this function over a non-arithmetical/logical
operator. *)
val get_integer_op_of_predicate:
- lenv:Function_params_ty.t -> predicate -> number_ty
+ logic_env:Logic_env.t -> predicate -> number_ty
(** @return the infered type for the top operation of the given predicate. *)
-val get_typ: lenv:Function_params_ty.t -> term -> typ
+val get_typ: logic_env:Logic_env.t -> term -> typ
(** Get the type which the given term must be generated to. *)
-val get_op: lenv:Function_params_ty.t -> term -> typ
+val get_op: logic_env:Logic_env.t -> term -> typ
(** Get the type which the operation on top of the given term must be generated
to. *)
-val get_cast: lenv:Function_params_ty.t -> term -> typ option
+val get_cast: logic_env:Logic_env.t -> term -> typ option
(** Get the type which the given term must be converted to (if any). *)
-val get_cast_of_predicate: lenv:Function_params_ty.t -> predicate -> typ option
+val get_cast_of_predicate:
+ logic_env:Logic_env.t -> predicate -> typ option
(** Like {!get_cast}, but for predicates. *)
val unsafe_set:
term ->
?ctx:number_ty ->
- lenv:Function_params_ty.t ->
+ logic_env:Logic_env.t ->
number_ty ->
unit
(** Register that the given term has the given type in the given context (if
@@ -160,16 +140,36 @@ val unsafe_set:
val typ_of_lty: logic_type -> typ
(** @return the C type that correponds to the given logic type. *)
+(*****************************************************************************)
+(** {2 Typing processing} *)
+(*****************************************************************************)
+
val type_program : file -> unit
(** compute and store the type of all the terms that will be translated
in a program *)
-val preprocess_predicate : Function_params_ty.t -> predicate -> unit
+val preprocess_predicate :
+ logic_env:Logic_env.t ->
+ predicate ->
+ unit
(** compute and store the types of all the terms in a given predicate *)
-val preprocess_rte : lenv:Function_params_ty.t -> code_annotation -> unit
+val preprocess_rte :
+ logic_env:Logic_env.t ->
+ code_annotation ->
+ unit
(** compute and store the type of all the terms in a code annotation *)
+val preprocess_term:
+ use_gmp_opt:bool ->
+ ?ctx:number_ty ->
+ logic_env:Logic_env.t ->
+ term ->
+ unit
+(** Compute the type of each subterm of the given term in the given context. If
+ [use_gmp_opt] is false, then the conversion to the given context is done
+ even if -e-acsl-gmp-only is set. *)
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index e2dafa3717c764407fa9490730e0ef3521f604e4..7db64b30c3a2694fd32bc0d2b057731cabca58fd 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -162,7 +162,7 @@ let assumes_predicate env assumes =
Logic_const.ptrue
assumes
in
- Typing.preprocess_predicate (Env.Local_vars.get env) p;
+ Typing.preprocess_predicate ~logic_env:(Env.Logic_env.get env) p;
p
let create ~loc spec =
@@ -360,7 +360,9 @@ let check_other_requires kf env contract =
let requires =
{ requires with pred_name = b.b_name :: requires.pred_name }
in
- Typing.preprocess_predicate (Env.Local_vars.get env) requires;
+ Typing.preprocess_predicate
+ ~logic_env:(Env.Logic_env.get env)
+ requires;
(* Create runtime check *)
let adata, env = Assert.empty ~loc kf env in
let requires_e, adata, env =
@@ -681,7 +683,7 @@ let check_post_conds kf env contract =
pred_name = b.b_name :: post_cond.pred_name }
in
Typing.preprocess_predicate
- (Env.Local_vars.get env)
+ ~logic_env:(Env.Logic_env.get env)
post_cond;
(* Create runtime check *)
let adata, env = Assert.empty ~loc kf env in
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 1bc2d330c57097e2cae47ad1594952f86c93b988..5189b00ad2c0f04ddc5d00ee608e4f0977bbd274 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -77,7 +77,7 @@ type t = {
(* list of loop environment for each currently visited loops *)
cpt: int;
(* counter used when generating variables *)
- local_vars: Typing.Function_params_ty.t list;
+ logic_env_stack: Analyses_datatype.Logic_env.t list;
(* type of variables used in calls to logic functions and predicates *)
kinstr: kinstr;
(* Current kinstr of the environment *)
@@ -112,7 +112,7 @@ let empty =
var_mapping = Logic_var.Map.empty;
loop_envs = [];
cpt = 0;
- local_vars = [];
+ logic_env_stack = [ Analyses_datatype.Logic_env.empty ];
kinstr = Kglobal }
let top env = match env.env_stack with
@@ -540,21 +540,35 @@ module Context = struct
end
-module Local_vars = struct
+module Logic_env = struct
- let push_new env =
- {env with local_vars = [] :: env.local_vars}
+ let push_new env profile =
+ let logic_env_stack =
+ Analyses_datatype.Logic_env.make profile :: env.logic_env_stack
+ in
+ {env with logic_env_stack = logic_env_stack}
- let add env ty =
- match env.local_vars with
- | curr::stacked -> {env with local_vars = (ty :: curr) :: stacked}
- | [] -> Options.fatal
- "Trying to add local variable in a non-existing environment"
+ let add env x ival =
+ match env.logic_env_stack with
+ | curr::_ as logic_env ->
+ let logic_env_stack =
+ Analyses_datatype.Logic_env.add curr x ival :: logic_env
+ in
+ {env with logic_env_stack = logic_env_stack}
+ | [] -> Options.fatal "logic environment stack is empty"
let get env =
- match env.local_vars with
- | lenv :: _ -> lenv
- | [] -> []
+ match env.logic_env_stack with
+ | curr::_ -> curr
+ | [] -> Options.fatal "logic environment stack is empty"
+
+ let get_profile env =
+ Analyses_datatype.Logic_env.get_profile (get env)
+
+ let pop env =
+ match env.logic_env_stack with
+ | _::stacked -> {env with logic_env_stack = stacked}
+ | [] -> Options.fatal "logic environment stack is empty"
end
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index da9b818bb86dc6843fb89c87c2d47613aa1ec332..a3f7e3c08032f76150163e5bbc542cbf5b0c358f 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -22,6 +22,7 @@
open Cil_types
open Analyses_types
+open Analyses_datatype
open Contract_types
(** Environments.
@@ -176,10 +177,12 @@ val set_rte: t -> bool -> t
val generate_rte: t -> bool
(** Returns the current value of RTE generation for the given environment *)
-module Local_vars: sig
- val push_new: t -> t
- val add: t -> Typing.number_ty -> t
- val get: t -> Typing.Function_params_ty.t
+module Logic_env: sig
+ val push_new: t -> Profile.t -> t
+ val add : t -> logic_var -> ival -> t
+ val get: t -> Logic_env.t
+ val get_profile : t -> Profile.t
+ val pop: t -> t
end
(* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index b2eec285b37913ed2b79b68042213f990aeb22f2..efc72c375b0559a68b2db7706a817f0444aaf640 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+open Analyses_types
module Error = Translation_error
(**************************************************************************)
@@ -70,31 +71,24 @@ let get_set_suffix_and_arg res_ty e =
end
in
match (exp_number_ty, res_number_ty) with
- | Typing.Gmpz, Typing.Gmpz | Typing.Rational, Typing.Rational ->
- "", [ e ]
- | Typing.Gmpz, Typing.Rational ->
- "_z", [ e ]
- | Typing.Rational, Typing.Gmpz ->
- "_q", [ e ]
- | Typing.C_integer IChar, _ ->
+ | Gmpz, Gmpz | Rational, Rational -> "", [ e ]
+ | Gmpz, Rational -> "_z", [ e ]
+ | Rational, Gmpz -> "_q", [ e ]
+ | C_integer IChar, _ ->
(if Cil.theMachine.Cil.theMachine.char_is_unsigned then "_ui"
else "_si"),
args_uisi e
- | Typing.C_integer (IBool | IUChar | IUInt | IUShort | IULong), _ ->
+ | C_integer (IBool | IUChar | IUInt | IUShort | IULong), _ ->
"_ui", args_uisi e
- | Typing.C_integer (ISChar | IShort | IInt | ILong), _ ->
- "_si", args_uisi e
- | Typing.C_integer (ILongLong | IULongLong as ikind), _ ->
- raise (Longlong ikind)
- | Typing.C_float (FDouble | FFloat), _ ->
- (* FFloat is a strict subset of FDouble (modulo exceptional numbers)
- Hence, calling [set_d] for both of them is sound.
- HOWEVER: the machdep MUST NOT be vulnerable to double rounding
- [TODO] check the statement above *)
- "_d", [ e ]
- | Typing.C_float FLongDouble, _ ->
- Error.not_yet "creating gmp from long double"
- | Typing.Gmpz, _ | Typing.Rational, _ | Typing.Real, _ | Typing.Nan, _ -> (
+ | C_integer (ISChar | IShort | IInt | ILong), _ -> "_si", args_uisi e
+ | C_integer (ILongLong | IULongLong as ikind), _ -> raise (Longlong ikind)
+ | C_float (FDouble | FFloat), _ -> "_d", [ e ]
+ (* FFloat is a strict subset of FDouble (modulo exceptional numbers)
+ Hence, calling [set_d] for both of them is sound.
+ HOWEVER: the machdep MUST NOT be vulnerable to double rounding
+ [TODO] check the statement above *)
+ | C_float FLongDouble, _ -> Error.not_yet "creating gmp from long double"
+ | Gmpz, _ | Rational, _ | Real, _ | Nan, _ -> (
match Cil.unrollType ty with
| TPtr(TInt(IChar, _), _) ->
"_str",
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index dacc80aa94a742b7d86f113c406436023369baf2..034f9369c09ea3a2d50ac8425a39cf5477ee5515 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -223,6 +223,7 @@ let inject_in_instr env kf stmt = function
let add_new_block_in_stmt env kf stmt =
(* Add temporal analysis instrumentations *)
let env = Temporal.handle_stmt stmt env kf in
+ let logic_env = Env.Logic_env.get env in
let new_stmt, env =
if Functions.check kf then
let env =
@@ -232,7 +233,7 @@ let add_new_block_in_stmt env kf stmt =
(* translate potential RTEs of ghost code *)
let rtes = Rte.stmt ~warn:false kf stmt in
List.iter
- (Typing.preprocess_rte ~lenv:(Env.Local_vars.get env))
+ (Typing.preprocess_rte ~logic_env)
rtes;
Translate_rtes.rte_annots Printer.pp_stmt stmt kf env rtes
end else
diff --git a/src/plugins/e-acsl/src/code_generator/libc.ml b/src/plugins/e-acsl/src/code_generator/libc.ml
index 6d7a2c1b1eb4a8bc9252902e2c519a056b425fcb..9738f961d1df8798d6aca52c31024f19d848c97f 100644
--- a/src/plugins/e-acsl/src/code_generator/libc.ml
+++ b/src/plugins/e-acsl/src/code_generator/libc.ml
@@ -187,9 +187,10 @@ let check_integer_bounds ~from target =
If [check_lower_bound] is set to false, then the lower bound check is not
performed. *)
let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
- Typing.type_term ~use_gmp_opt:false ~lenv:(Env.Local_vars.get env) t;
- match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t with
- | Typing.Gmpz ->
+ let logic_env = Env.Logic_env.get env in
+ Typing.preprocess_term ~use_gmp_opt:false ~logic_env t;
+ match Typing.get_number_ty ~logic_env t with
+ | Gmpz ->
let e, _, env =
Translate_utils.gmp_to_sizet
~adata:Assert.no_data
@@ -201,7 +202,7 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
t
in
e, env
- | Typing.(C_integer _ | C_float _) as nty ->
+ | C_integer _ | C_float _ as nty ->
(* We know that [t] can be translated to a C type, so we start with that *)
let e, _, env = Translate_terms.to_exp ~adata:Assert.no_data kf env t in
(* Then we can check if the expression will fit in a [size_t] *)
@@ -210,9 +211,8 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
let check_lower_bound, check_upper_bound =
let lower, upper =
match nty with
- | Typing.C_integer t_kind ->
- check_integer_bounds ~from:t_kind sizet_kind
- | Typing.C_float _ -> true, true
+ | C_integer t_kind -> check_integer_bounds ~from:t_kind sizet_kind
+ | C_float _ -> true, true
| _ -> assert false
in
lower && check_lower_bound, upper
@@ -284,9 +284,8 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
List.rev (assigns :: stmts))
in
e, env
- | Typing.(Rational | Real) ->
- Env.not_yet env "cast of rational or real to size_t"
- | Typing.Nan ->
+ | Rational | Real -> Env.not_yet env "cast of rational or real to size_t"
+ | Nan ->
Options.fatal
"Trying to translate a term that is not an integer or a C type: %a"
Printer.pp_term t
diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.ml b/src/plugins/e-acsl/src/code_generator/logic_array.ml
index 56fd4c6518729e0b905b020665da4b68510745eb..cf4122b3e569015a30a783ed1759e97b69ea63f1 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_array.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_array.ml
@@ -240,7 +240,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
(Rle, Logic_utils.expr_to_term len, Logic_utils.expr_to_term len_orig)
in
let p = { p with pred_name = "array_coercion" :: p.pred_name } in
- Typing.preprocess_predicate (Env.Local_vars.get env) p;
+ Typing.preprocess_predicate ~logic_env:(Env.Logic_env.get env) p;
let adata, env = Assert.empty ~loc kf env in
let adata = Assert.register ~loc "destination length" len adata in
let adata = Assert.register ~loc "current length" len_orig adata in
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index 1dd94bb94467bea728e9b455ebbba85fcba59c61..331ec21a4ea44268ed23683105a300ab2c16fb96 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -22,6 +22,8 @@
open Cil_types
open Cil_datatype
+open Analyses_types
+open Analyses_datatype
module Error = Translation_error
(**************************************************************************)
@@ -122,22 +124,22 @@ let generate_body ~loc kf env ret_ty ret_vi = function
| LBnone |LBreads _ | LBinductive _ -> assert false
(* Generate a kernel function from a given logic info [li] *)
-let generate_kf ~loc fname env ret_ty params_ty li =
+let generate_kf ~loc fname env ret_ty params_ty params_ival li =
(* build the formal parameters *)
let params, params_ty_vi =
List.fold_right2
(fun lvi pty (params, params_ty) ->
let ty = match pty with
- | Typing.Gmpz ->
+ | Gmpz ->
(* GMP's integer are arrays: consider them as pointers in function's
parameters *)
Gmp_types.Z.t_as_ptr ()
- | Typing.C_integer ik -> TInt(ik, [])
- | Typing.C_float ik -> TFloat(ik, [])
+ | C_integer ik -> TInt(ik, [])
+ | C_float ik -> TFloat(ik, [])
(* for the time being, no reals but rationals instead *)
- | Typing.Rational -> Gmp_types.Q.t ()
- | Typing.Real -> Error.not_yet "real number"
- | Typing.Nan -> Typing.typ_of_lty lvi.lv_type
+ | Rational -> Gmp_types.Q.t ()
+ | Real -> Error.not_yet "real number"
+ | Nan -> Typing.typ_of_lty lvi.lv_type
in
(* build the formals: cannot use [Cil.makeFormal] since the function
does not exist yet *)
@@ -196,23 +198,9 @@ let generate_kf ~loc fname env ret_ty params_ty li =
let env = Env.push env in
(* fill the typing environment with the function's parameters
before generating the code (code generation invokes typing) *)
- let env = Env.Local_vars.push_new env in
+ let env = Env.Logic_env.push_new env params_ival in
let env =
- let add ty env =
- Env.Local_vars.add env ty
- in
- (* The list of parameters has to respect the order of the parameters to
- keep consistency with the typing. Hence the folding is on the right.
- This is acceptable since in practice functions have few parameters *)
- List.fold_right add params_ty env
- in
- let env =
- let add env lvi vi =
- let i = Interval.interv_of_typ vi.vtype in
- Interval.Env.add lvi i;
- Env.Logic_binding.add_binding env lvi vi
- in
- List.fold_left2 add env li.l_profile params
+ List.fold_left2 (Env.Logic_binding.add_binding) env li.l_profile params
in
let assigns_from =
try Some (Assigns.get_assigns_from ~loc env li.l_profile li.l_var_info)
@@ -270,7 +258,6 @@ let generate_kf ~loc fname env ret_ty params_ty li =
fundec.sbody.blocals <- blocks;
List.iter
(fun lvi ->
- Interval.Env.remove lvi;
ignore (Env.Logic_binding.remove env lvi))
li.l_profile
in
@@ -283,7 +270,7 @@ let generate_kf ~loc fname env ret_ty params_ty li =
(* for each logic_info, associate its possible profiles, i.e. the types of its
parameters + the generated varinfo for the function *)
let memo_tbl:
- kernel_function Typing.Function_params_ty.Hashtbl.t Logic_info.Hashtbl.t
+ kernel_function Profile.Hashtbl.t Logic_info.Hashtbl.t
= Logic_info.Hashtbl.create 7
let reset () = Logic_info.Hashtbl.clear memo_tbl
@@ -303,7 +290,7 @@ let add_generated_functions globals =
:: acc
in
aux
- (Typing.Function_params_ty.Hashtbl.fold_sorted
+ (Profile.Hashtbl.fold_sorted
(fun _ -> add_fundecl)
params
acc)
@@ -324,7 +311,7 @@ let add_generated_functions globals =
in
let rev_globals =
Logic_info.Hashtbl.fold_sorted
- (fun _ -> Typing.Function_params_ty.Hashtbl.fold_sorted
+ (fun _ -> Profile.Hashtbl.fold_sorted
(fun _ -> add_fundec))
memo_tbl
rev_globals
@@ -333,15 +320,18 @@ let add_generated_functions globals =
(* Generate (and memoize) the function body and create the call to the
generated function. *)
-let function_to_exp ~loc ?tapp fname env kf li params_ty args =
+let function_to_exp ~loc ?tapp fname env kf li params_ty profile args =
let ret_ty =
match tapp with
- | Some tapp -> Typing.get_typ ~lenv:(Env.Local_vars.get env) tapp
+ | Some tapp ->
+ let logic_env = Env.Logic_env.get env in
+ Typing.get_typ ~logic_env tapp
| None -> (Cil_types.TInt (IInt, []))
in
let gen tbl =
- let vi, kf, gen_body = generate_kf fname ~loc env ret_ty params_ty li in
- Typing.Function_params_ty.Hashtbl.add tbl params_ty kf;
+ let vi, kf, gen_body =
+ generate_kf fname ~loc env ret_ty params_ty profile li in
+ Profile.Hashtbl.add tbl profile kf;
vi, gen_body
in
(* memoise the function's varinfo *)
@@ -349,12 +339,12 @@ let function_to_exp ~loc ?tapp fname env kf li params_ty args =
try
let h = Logic_info.Hashtbl.find memo_tbl li in
try
- let kf = Typing.Function_params_ty.Hashtbl.find h params_ty in
+ let kf = Profile.Hashtbl.find h profile in
Kernel_function.get_vi kf,
(fun () -> ()) (* body generation already planified *)
with Not_found -> gen h
with Not_found ->
- let h = Typing.Function_params_ty.Hashtbl.create 7 in
+ let h = Profile.Hashtbl.create 7 in
Logic_info.Hashtbl.add memo_tbl li h;
gen h
in
@@ -449,7 +439,7 @@ let app_to_exp ~adata ~loc ?tapp kf env ?eargs li targs =
begin
raise_errors li.l_body;
(* build the arguments and compute the integer_ty of the parameters *)
- let params_ty, args, adata, env =
+ let params_ty, params_ival, args, adata, env =
let eargs, adata, env =
match eargs with
| None ->
@@ -468,12 +458,10 @@ let app_to_exp ~adata ~loc ?tapp kf env ?eargs li targs =
in
try
List.fold_right2
- (fun targ earg (params_ty, args, adata, env) ->
- let param_ty =
- Typing.get_number_ty
- ~lenv:(Env.Local_vars.get env)
- targ
- in
+ (fun targ earg (params_ty, params_ival ,args, adata, env) ->
+ let logic_env = Env.Logic_env.get env in
+ let param_ty = Typing.get_number_ty ~logic_env targ in
+ let param_ival = Interval.get ~logic_env targ in
let e, env =
try
let ty = Typing.typ_of_number_ty param_ty in
@@ -488,9 +476,13 @@ let app_to_exp ~adata ~loc ?tapp kf env ?eargs li targs =
with Typing.Not_a_number ->
earg, env
in
- param_ty :: params_ty, e :: args, adata, env)
+ param_ty :: params_ty,
+ param_ival :: params_ival,
+ e :: args,
+ adata,
+ env)
targs eargs
- ([], [], adata ,env)
+ ([], [], [], adata ,env)
with Invalid_argument _ ->
Options.fatal
"[Tapp] unexpected number of arguments when calling %s"
@@ -499,8 +491,10 @@ let app_to_exp ~adata ~loc ?tapp kf env ?eargs li targs =
let gen_fname =
Varname.get ~scope:Varname.Global (Functions.RTL.mk_gen_name fname)
in
+ let profile = Profile.make li.l_profile params_ival in
+ let profile = Interval.get_widened_profile profile li in
let vi, e, env =
- function_to_exp ~loc ?tapp gen_fname env kf li params_ty args
+ function_to_exp ~loc ?tapp gen_fname env kf li params_ty profile args
in
vi, e, adata, env
end
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index d656f4bd504e46f5a109f37f29746f1f114c741a..0f25543b66d2f833927cb0c93e0cdb97abe0de7a 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -66,10 +66,9 @@ let handle_annotations env kf stmt =
| Some (t, measure_opt) ->
let env = Env.set_annotation_kind env Variant in
let env = Env.push env in
- (* There cannot be bound logical variables since we cannot write
- loops inside logic functions or predicates, hence lenv is []*)
- Typing.type_term ~use_gmp_opt:true ~lenv:[] t;
- let ty = Typing.get_typ ~lenv:[] t in
+ let logic_env = Env.Logic_env.get env in
+ Typing.preprocess_term ~use_gmp_opt:true ~logic_env t;
+ let ty = Typing.get_typ ~logic_env t in
if Gmp_types.is_t ty then Error.not_yet "loop variant using GMP";
let e, _, env = !term_to_exp_ref ~adata:Assert.no_data kf env t in
let vi_old, e_old, env =
@@ -99,7 +98,6 @@ let handle_annotations env kf stmt =
| [] -> begin
(* No statements remaining in the loop: variant check *)
let env = Env.set_annotation_kind env Variant in
- let lenv = Env.Local_vars.get env in
match variant with
| Some (t, e_old, Some measure) ->
let env = Env.push env in
@@ -110,7 +108,8 @@ let handle_annotations env kf stmt =
term_name = [];
term_type = Linteger;}
in
- Typing.type_term ~use_gmp_opt:true ~lenv tapp;
+ let logic_env = Env.Logic_env.get env in
+ Typing.preprocess_term ~use_gmp_opt:true ~logic_env tapp;
let e, _, env = !term_to_exp_ref ~adata:Assert.no_data kf env t in
let e_tapp, _, env =
Logic_functions.app_to_exp
@@ -167,7 +166,8 @@ let handle_annotations env kf stmt =
let variant_pos =
Logic_const.prel ~loc (Rge, t_old, Logic_const.tinteger ~loc 0)
in
- Typing.type_named_predicate ~lenv variant_pos;
+ let logic_env = Env.Logic_env.get env in
+ Typing.preprocess_predicate ~logic_env variant_pos;
let variant_pos_e, _, env =
!predicate_to_exp_ref ~adata:Assert.no_data kf env variant_pos
in
@@ -199,7 +199,7 @@ let handle_annotations env kf stmt =
let variant_dec =
Logic_const.prel ~loc (Rgt, t_old, t)
in
- Typing.type_named_predicate ~lenv variant_dec;
+ Typing.preprocess_predicate ~logic_env variant_dec;
let variant_dec_e, _, env =
!predicate_to_exp_ref ~adata:Assert.no_data kf env variant_dec
in
@@ -280,30 +280,25 @@ let handle_annotations env kf stmt =
(**************************** Nested loops ********************************)
(**************************************************************************)
let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
- let lenv = Env.Local_vars.get env in
let term_to_exp = !term_to_exp_ref ~adata:Assert.no_data in
+ let logic_env = Env.Logic_env.get env in
match lscope_vars with
| [] ->
mk_innermost_block env
| Lvs_quantif(t1, rel1, logic_x, rel2, t2) :: lscope_vars' ->
assert (rel1 == Rle && rel2 == Rlt);
- Typing.type_term ~use_gmp_opt:false ~lenv t1;
- Typing.type_term ~use_gmp_opt:false ~lenv t2;
let ctx =
- let ty1 = Typing.get_number_ty ~lenv t1 in
- let ty2 = Typing.get_number_ty ~lenv t2 in
- Typing.join ty1 ty2
+ Typing.number_ty_bound_variable
+ ~profile:(Env.Logic_env.get_profile env)
+ (t1, logic_x, t2)
in
- let t_plus_one ?ty t =
- (* whenever provided, [ty] is known to be the type of the result *)
+ let t_plus_one ~ty t =
+ (* [ty] is the type of the result *)
let tone = Cil.lone ~loc () in
let res = Logic_const.term ~loc (TBinOp(PlusA, t, tone)) Linteger in
- Option.iter
- (fun ty ->
- Typing.unsafe_set tone ~ctx:ty ~lenv ctx;
- Typing.unsafe_set t ~ctx:ty ~lenv ctx;
- Typing.unsafe_set res ~lenv ty)
- ty;
+ Typing.unsafe_set ~logic_env tone ~ctx:ty ctx;
+ Typing.unsafe_set ~logic_env t ~ctx:ty ctx;
+ Typing.unsafe_set ~logic_env res ty;
res
in
let ty =
@@ -314,9 +309,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 kf logic_x in
let lv_x = var var_x in
let env = match ctx with
- | Typing.C_integer _ -> env
- | Typing.Gmpz -> Env.add_stmt env (Gmp.init ~loc x)
- | Typing.(C_float _ | Rational | Real | Nan) -> assert false
+ | C_integer _ -> env
+ | Gmpz -> Env.add_stmt env (Gmp.init ~loc x)
+ | C_float _ | Rational | Real | Nan -> assert false
in
(* build the inner loops and loop body *)
let body, env =
@@ -337,17 +332,17 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
to avoid the extra addition (relevant when computing with GMP) *)
let guard =
match t2.term_node with
- | TBinOp (PlusA, t2_minus_one, {term_node = TConst(Integer (n, _))}) when Integer.is_one n ->
+ | TBinOp (PlusA, t2_minus_one, {term_node = TConst(Integer (n, _))}) when
+ Integer.is_one n ->
Logic_const.term ~loc
- (TBinOp(Le, tlv, { t2_minus_one with term_node = t2_minus_one.term_node }))
+ (TBinOp(Le, tlv, t2_minus_one))
Linteger
| _ ->
- (* must copy [t2] to force it being typed again *)
Logic_const.term ~loc
- (TBinOp(Lt, tlv, { t2 with term_node = t2.term_node } ))
+ (TBinOp(Lt, tlv, t2))
Linteger
in
- Typing.type_term ~use_gmp_opt:false ~lenv ~ctx:Typing.c_int guard;
+ Typing.preprocess_term ~use_gmp_opt:false ~ctx:Typing.c_int ~logic_env guard;
let guard_exp, _, env = term_to_exp kf (Env.push env) guard in
let break_stmt = Smart_stmt.break ~loc:guard_exp.eloc in
let guard_blk, env = Env.pop_and_get
@@ -413,7 +408,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
Env.Logic_binding.remove env logic_x;
[ start ; stmt ], env
| Lvs_let(lv, t) :: lscope_vars' ->
- let ty = Typing.get_typ ~lenv t in
+ let ty = Typing.get_typ ~logic_env t in
let vi_of_lv, exp_of_lv, env = Env.Logic_binding.add ~ty env kf lv in
let e, _, env = term_to_exp kf env t in
let ty = Cil.typeOf e in
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index 5ce9f723155a78b8090017ff950ea2293eb3fe37..db07104aa2d3fd256750e294661f6c0f27dd443b 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -215,11 +215,8 @@ let range_to_ptr_and_size ~adata ~loc kf env ptr r p =
Logic_const.term ~loc (TBinOp(Mult, s, n1)) Linteger))
(Ctype typ_charptr)
in
- Typing.type_term
- ~use_gmp_opt:false
- ~ctx:Typing.nan
- ~lenv:(Env.Local_vars.get env)
- ptr;
+ let logic_env = Env.Logic_env.get env in
+ Typing.preprocess_term ~use_gmp_opt:false ~ctx:Typing.nan ~logic_env ptr;
let (ptr, adata), env =
Env.with_params_and_result
~rte:true
@@ -269,11 +266,10 @@ let range_to_ptr_and_size ~adata ~loc kf env ptr r p =
in
Logic_const.term ~loc (Tlet (size_term_info, size_term_if)) Linteger
in
- let lenv = Env.Local_vars.get env in
- Typing.type_term ~use_gmp_opt:false ~lenv size_term;
+ Typing.preprocess_term ~use_gmp_opt:false ~logic_env size_term;
let size, adata, env =
- match Typing.get_number_ty size_term ~lenv with
- | Typing.Gmpz ->
+ match Typing.get_number_ty size_term ~logic_env with
+ | Gmpz ->
(* Start by translating [size_term] to an expression so that the full term
with [\let] is not passed around. *)
let size_e, adata, env = !term_to_exp_ref ~adata kf env size_term in
@@ -287,10 +283,8 @@ let range_to_ptr_and_size ~adata ~loc kf env ptr r p =
"translation to GMP code should always return a C variable"
in
gmp_to_sizet ~adata ~loc ~pp:size_term kf env cvar_term p
- | Typing.(C_integer _ | C_float _) ->
- !term_to_exp_ref ~adata kf env size_term
- | Typing.(Rational | Real | Nan) ->
- assert false
+ | C_integer _ | C_float _ -> !term_to_exp_ref ~adata kf env size_term
+ | Rational | Real | Nan -> assert false
in
ptr, size, adata, env
@@ -480,7 +474,7 @@ let call_with_tset
in
(* There's no more quantifiers in the arguments now, we can call back
[predicate_to_exp] to translate the predicate as usual *)
- Typing.preprocess_predicate (Env.Local_vars.get env) p_quantified;
+ Typing.preprocess_predicate ~logic_env:(Env.Logic_env.get env) p_quantified;
!predicate_to_exp_ref ~adata kf env p_quantified
| [] ->
(* No arguments require quantifiers, so we can directly translate the
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index 27a00a7af6bee9a8023f084d874d6797281c1b29..30128ffc1aa2af95e56f231b91c19a9cfa0b7632 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -43,26 +43,31 @@ let predicate_to_exp_ref
[has_empty_quantif_with_false_negative] partially detects such cases:
Case 1: an empty quantification was detected for sure, return true.
Case 2: we don't know, return false. *)
-let rec has_empty_quantif_with_false_negative = function
+let rec has_empty_quantif_with_false_negative ~logic_env = function
| [] ->
(* case 2 *)
false
| (t1, _, t2) :: guards ->
- let iv1 = Interval.(extract_ival (infer t1)) in
- let iv2 = Interval.(extract_ival (infer t2)) in
+ let iv1 = Interval.(extract_ival (get ~logic_env t1)) in
+ let iv2 = Interval.(extract_ival (get ~logic_env t2)) in
let lower_bound, _ = Ival.min_and_max iv1 in
let _, upper_bound = Ival.min_and_max iv2 in
begin
match lower_bound, upper_bound with
| Some lower_bound, Some upper_bound ->
let res = lower_bound >= upper_bound in
- res (* case 1 *) || has_empty_quantif_with_false_negative guards
+ res (* case 1 *) ||
+ has_empty_quantif_with_false_negative guards ~logic_env
| None, _ | _, None ->
- has_empty_quantif_with_false_negative guards
+ has_empty_quantif_with_false_negative guards ~logic_env
end
let () =
- Labels.has_empty_quantif_ref := has_empty_quantif_with_false_negative
+ Labels.has_empty_quantif_ref :=
+ let logic_env = Analyses_datatype.Logic_env.empty in
+ has_empty_quantif_with_false_negative ~logic_env
+(* Since we do not support logic functions with labels, we do not need to
+ pass an actual logic environment *)
module Label_ids =
State_builder.Counter(struct let name = "E_ACSL.Label_ids" end)
@@ -76,7 +81,9 @@ let convert kf env loc ~is_forall quantif =
quantif
Printer.pp_predicate
in
- match has_empty_quantif_with_false_negative bound_vars, is_forall with
+ let logic_env = Env.Logic_env.get env in
+ let empty = has_empty_quantif_with_false_negative ~logic_env bound_vars in
+ match empty, is_forall with
| true, true ->
Cil.one ~loc, env
| true, false ->
@@ -92,14 +99,17 @@ let convert kf env loc ~is_forall quantif =
else z, o, fun e -> Smart_exp.lnot ~loc:e.eloc e
in
(* transform [bound_vars] into [lscope_var list],
- and update logic scope in the process *)
- let lvs_guards, env = List.fold_right
- (fun (t1, lv, t2) (lvs_guards, env) ->
+ and update logic scope and logic environment in the process *)
+ let lvs_guards, env = List.fold_left
+ (fun (lvs_guards, env) (t1, lv, t2) ->
let lvs = Lvs_quantif (t1, Rle, lv, Rlt, t2) in
let env = Env.Logic_scope.extend env lvs in
+ let logic_env = Env.Logic_env.get env in
+ let i = Interval.(join (get ~logic_env t1) (get ~logic_env t2)) in
+ let env = Env.Logic_env.add env lv i in
lvs :: lvs_guards, env)
- bound_vars
([], env)
+ bound_vars
in
let var_res, res, env =
(* variable storing the result of the quantifier *)
@@ -153,6 +163,12 @@ let convert kf env loc ~is_forall quantif =
end_loop.labels <- label :: end_loop.labels;
end_loop_ref := end_loop;
let env = Env.add_stmt env end_loop in
+ let env =
+ List.fold_left
+ (fun env _ -> Env.Logic_env.pop env)
+ env
+ lvs_guards
+ in
res, env
end
diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.ml b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
index aea6fef775426369624525e1ef3e939060bd8e81..cf14ab17aa83a48331f6ebf86548c3b230534d5f 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
@@ -92,7 +92,7 @@ end
where [t_size = tmax - tmin + (-1|0|1)] depending on whether the
inequalities are strict or large
and [t_shifted = lv - tmin + (-1|0)] (so that we start indexing at 0) *)
-let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
+let rec sizes_and_shifts_from_quantifs ~loc ~logic_env kf lscope sizes_and_shifts =
match lscope with
| [] ->
sizes_and_shifts
@@ -117,7 +117,8 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
| _ ->
Options.fatal "Unexpected comparison operator"
in
- let iv = Interval.(extract_ival (infer t_size)) in
+ Interval.(preprocess_term ~logic_env t_size);
+ let iv = Interval.(extract_ival (get ~logic_env 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
@@ -156,12 +157,12 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
in
(* Returning *)
let sizes_and_shifts = (t_size, t_shifted) :: sizes_and_shifts in
- sizes_and_shifts_from_quantifs ~loc kf lscope' sizes_and_shifts
+ sizes_and_shifts_from_quantifs ~loc ~logic_env kf lscope' sizes_and_shifts
| (Lvs_let(_, t) | Lvs_global(_, t)) :: _
when Misc.term_has_lv_from_vi t ->
Error.not_yet "\\at with logic variable linked to C variable"
| Lvs_let _ :: lscope' ->
- sizes_and_shifts_from_quantifs ~loc kf lscope' sizes_and_shifts
+ sizes_and_shifts_from_quantifs ~loc ~logic_env kf lscope' sizes_and_shifts
| Lvs_formal _ :: _ ->
Error.not_yet "\\at using formal variable of a logic function"
| Lvs_global _ :: _ ->
@@ -182,11 +183,8 @@ let size_from_sizes_and_shifts ~loc = function
(* Build the left-value corresponding to [*(at + index)]. *)
let lval_at_index ~loc kf env (e_at, t_index) =
- Typing.type_term
- ~use_gmp_opt:false
- ~ctx:Typing.c_int
- ~lenv:(Env.Local_vars.get env)
- t_index;
+ let logic_env = Env.Logic_env.get env in
+ Typing.preprocess_term ~use_gmp_opt:false ~ctx:Typing.c_int ~logic_env t_index;
let term_to_exp = !term_to_exp_ref in
let e_index, _, env = term_to_exp ~adata:Assert.no_data kf env t_index in
let e_index = Cil.constFold false e_index in
@@ -238,8 +236,9 @@ let index_from_sizes_and_shifts ~loc sizes_and_shifts =
let indexed_exp ~loc kf env e_at =
let lscope_vars = Lscope.get_all (Env.Logic_scope.get env) in
let lscope_vars = List.rev lscope_vars in
+ let logic_env = Env.Logic_env.get env in
let sizes_and_shifts =
- sizes_and_shifts_from_quantifs ~loc kf lscope_vars []
+ sizes_and_shifts_from_quantifs ~loc ~logic_env kf lscope_vars []
in
let t_index = index_from_sizes_and_shifts ~loc sizes_and_shifts in
let lval_at_index, env = lval_at_index ~loc kf env (e_at, t_index) in
@@ -258,9 +257,10 @@ let translations: varinfo Error.result At_data.Hashtbl.t =
[pred_or_term] in the current environment and returns the translated
expression. *)
let pretranslate_to_exp ~loc kf env pot =
- Options.debug ~level:4 "pre-translating %a in local environment '%a'"
+ Options.debug ~level:4 "pre-translating %a in profile '%a'"
Pred_or_term.pretty pot
- Typing.Function_params_ty.pretty (Env.Local_vars.get env);
+ Profile.pretty
+ (Env.Logic_env.get_profile env);
let e, env, t_opt =
let adata = Assert.no_data in
match pot with
@@ -299,26 +299,42 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
Options.debug ~level:4
"pre-translating %a in local environment '%a' with lscope '%a'"
Pred_or_term.pretty pot
- Typing.Function_params_ty.pretty (Env.Local_vars.get env)
+ Profile.pretty
+ (Env.Logic_env.get_profile env)
Lscope.D.pretty lscope;
let term_to_exp = !term_to_exp_ref in
let lscope_vars = Lscope.get_all lscope in
let lscope_vars = List.rev lscope_vars in
+ let rec add_lscope_to_logic_env env = function
+ | [] -> env
+ | Lvs_quantif(t1,_,x,_,t2)::lscope ->
+ let logic_env = Env.Logic_env.get env in
+ let i =
+ Interval.join
+ (Interval.get ~logic_env t1)
+ (Interval.get ~logic_env t2)
+ in
+ add_lscope_to_logic_env
+ (Env.Logic_env.add env x i)
+ lscope
+ | _::_ -> env
+ in
+ let env = add_lscope_to_logic_env env lscope in
+ let logic_env = Env.Logic_env.get env in
let sizes_and_shifts =
- sizes_and_shifts_from_quantifs ~loc kf lscope_vars []
+ sizes_and_shifts_from_quantifs ~loc ~logic_env kf lscope_vars []
in
(* Creating the pointer *)
let ty = match pot with
| PoT_pred _ ->
Cil.intType
| PoT_term t ->
- let lenv = (Env.Local_vars.get env) in
- begin match Typing.get_number_ty ~lenv t with
- | Typing.(C_integer _ | C_float _ | Nan) ->
- Typing.get_typ ~lenv t
- | Typing.(Rational | Real) ->
+ begin match Typing.get_number_ty ~logic_env t with
+ | C_integer _ | C_float _ | Nan ->
+ Typing.get_typ ~logic_env t
+ | Rational | Real ->
Error.not_yet "\\at on purely logic variables and over real type"
- | Typing.Gmpz ->
+ | Gmpz ->
Error.not_yet "\\at on purely logic variables and over gmp type"
end
in
@@ -339,11 +355,9 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
let t_size =
Logic_const.term ~loc (TBinOp(Mult, t_sizeof, t_size)) lty_sizeof
in
- let lenv = Env.Local_vars.get env in
- Typing.type_term ~use_gmp_opt:false ~lenv t_size;
- let malloc_stmt =
- match Typing.get_number_ty ~lenv t_size with
- | Typing.C_integer IInt ->
+ Typing.preprocess_term ~use_gmp_opt:false ~logic_env t_size;
+ let malloc_stmt = match Typing.get_number_ty ~logic_env t_size with
+ | C_integer IInt ->
let e_size, _, _ =
term_to_exp ~adata:Assert.no_data kf env t_size
in
@@ -355,11 +369,11 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
[ e_size ]
in
malloc_stmt
- | Typing.(C_integer _ | C_float _ | Gmpz) ->
+ | 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.(Rational | Real | Nan) ->
+ | Rational | Real | Nan ->
Error.not_yet "quantification over non-integer type"
in
let free_stmt = Smart_stmt.call ~loc "free" [e] in
@@ -396,8 +410,8 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
variable declarations. *)
[ Smart_stmt.block_stmt block ], env
| PoT_term t ->
- begin match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t with
- | Typing.(C_integer _ | C_float _ | Nan) ->
+ begin match Typing.get_number_ty ~logic_env t with
+ | C_integer _ | C_float _ | Nan ->
let env = Env.push env in
let lval, env = lval_at_index ~loc kf env (e_at, t_index) in
let e, _, env = term_to_exp kf env t in
@@ -411,9 +425,9 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
(* We CANNOT return [block.bstmts] because it does NOT contain
variable declarations. *)
[ Smart_stmt.block_stmt block ], env
- | Typing.(Rational | Real) ->
+ | Rational | Real ->
Error.not_yet "\\at on purely logic variables and over real type"
- | Typing.Gmpz ->
+ | Gmpz ->
Error.not_yet "\\at on purely logic variables and over gmp type"
end
in
diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
index f2de0bc87cf9e97d465c29d8748d85033ba52c54..1975623c8f965d0ccec1480f2ec94fad329d22e9 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -72,7 +72,7 @@ let relation_to_binop = function
translation. *)
let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
let loc = p.pred_loc in
- let lenv = Env.Local_vars.get env in
+ let logic_env = Env.Logic_env.get env in
Cil.CurrentLoc.set loc;
match p.pred_content with
| Pfalse -> Cil.zero ~loc, adata, env
@@ -88,7 +88,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
| Pvalid_function _ -> Env.not_yet env "\\valid_function"
| Prel(rel, t1, t2) ->
let ity =
- Typing.get_integer_op_of_predicate ~lenv p
+ Typing.get_integer_op_of_predicate ~logic_env p
in
Translate_utils.comparison_to_exp
~adata
@@ -199,7 +199,6 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
let e, adata, env = to_exp ~adata kf env p in
(* Remove the logic var from the logic scope *)
let env = Env.Logic_scope.remove env lvs in
- Interval.Env.remove li.l_var_info;
e, adata, env
| Pforall _ | Pexists _ ->
let e, env = Quantif.quantif_to_exp kf env p in
@@ -238,7 +237,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
let p = { p with pred_name = name :: p.pred_name } in
let tp = Logic_const.toplevel_predicate ~kind:Assert p in
let annot = Logic_const.new_code_annotation (AAssert ([],tp)) in
- Typing.preprocess_rte ~lenv:(Env.Local_vars.get env) annot;
+ Typing.preprocess_rte ~logic_env:(Env.Logic_env.get env) annot;
!translate_rte_annots_ref
Printer.pp_code_annotation
annot
@@ -324,7 +323,7 @@ and to_exp ~adata ?inplace ?name kf ?rte env p =
let env = if rte then !translate_rte_exp_ref kf env e else env in
let cast =
Typing.get_cast_of_predicate
- ~lenv:(Env.Local_vars.get env)
+ ~logic_env:(Env.Logic_env.get env)
p
in
let env = Assert.do_pending_register_data env in
diff --git a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
index 3a25b9959cdbdf82d1aa10b33aaab97521ae3e79..f421f71dffc21670bfd7f0cfc218af0d3f3f389f 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
@@ -67,7 +67,7 @@ let exp ?filter kf env e =
| Some f -> List.filter f l
| None -> l
in
- List.iter (Typing.preprocess_rte ~lenv:(Env.Local_vars.get env)) l;
+ List.iter (Typing.preprocess_rte ~logic_env:(Env.Logic_env.get env)) l;
let env = rte_annots Printer.pp_exp e kf env l in
Assert.do_pending_register_data env
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index d748d34d5431cb67d9bb5b2d3533fd6034672c2d..12965127c73a69a7c0140e0ccaddfe33b2b57ded 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -24,6 +24,7 @@
open Cil_types
open Analyses_types
+open Analyses_datatype
let dkey = Options.Dkey.translation
(**************************************************************************)
@@ -45,25 +46,24 @@ let translate_rte_exp_ref
(* ************************************************************************** *)
let constant_to_exp ~loc env t c =
- let lenv = Env.Local_vars.get env in
let mk_real s =
let s = Rational.normalize_str s in
Cil.mkString ~loc s, Typed_number.Str_R
in
match c with
| Integer(n, _repr) ->
- let ity = Typing.get_number_ty ~lenv t in
+ let logic_env = Env.Logic_env.get env in
+ let ity = Typing.get_number_ty ~logic_env 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), Typed_number.Str_Z
- | Typing.C_float fkind ->
+ | Nan -> assert false
+ | Real -> Error.not_yet "real number constant"
+ | Rational -> mk_real (Integer.to_string n)
+ | Gmpz -> Cil.mkString ~loc (Integer.to_string n), Typed_number.Str_Z
+ (* too large integer *)
+ | C_float fkind ->
Cil.kfloat ~loc fkind (Int64.to_float (Integer.to_int64_exn n)), C_number
- | Typing.C_integer kind ->
- let cast = Typing.get_cast ~lenv t in
+ | C_integer kind ->
+ let cast = Typing.get_cast ~logic_env t in
match cast, kind with
| Some ty, (ILongLong | IULongLong) when Gmp_types.Z.is_t ty ->
(* too large integer *)
@@ -163,13 +163,13 @@ and tlval_to_lval kf env (host, offset) =
extended quantifier ("\sum" or "\product"). Do not take care of "\numof"
that have already been converted to "\sum". *)
and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
- let lenv = Env.Local_vars.get env in
+ let logic_env = Env.Logic_env.get env in
match lambda.term_node with
| Tlambda([ k ] ,lt)
when name.lv_name = "\\product" || name.lv_name = "\\sum"
->
- let ty_op = Typing.get_typ ~lenv t in
- let ty_k = match Typing.get_cast ~lenv t_min with
+ let ty_op = Typing.get_typ ~logic_env t in
+ let ty_k = match Typing.get_cast ~logic_env t_min with
| Some e -> e
| _ -> Options.fatal "unexpected error in \\sum translation"
in
@@ -199,7 +199,6 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
(* lambda_as_varinfo assignment *)
let env = Env.push env in
let e_lbd, _, env = to_exp ~adata:Assert.no_data kf env lt in
- Interval.Env.remove k;
let lbd_stmt,env =
Env.pop_and_get env
(Gmp.affect ~loc (Cil.var lbd_as_varinfo) lbd_as_exp e_lbd)
@@ -263,7 +262,7 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
let loc = t.term_loc in
- let lenv = Env.Local_vars.get env in
+ let logic_env = Env.Logic_env.get env in
match t.term_node with
| TConst c ->
let c, strnum = constant_to_exp ~loc env t c in
@@ -296,7 +295,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
let adata = Assert.register_term ~loc t e adata in
e, adata, env, Typed_number.C_number, "alignof"
| TUnOp(Neg | BNot as op, t') ->
- let ty = Typing.get_typ ~lenv t in
+ let ty = Typing.get_typ ~logic_env t in
let e, adata, env = to_exp ~adata kf env t' in
if Gmp_types.Z.is_t ty then
let name, vname = match op with
@@ -319,12 +318,12 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
else
Cil.new_exp ~loc (UnOp(op, e, ty)), adata, env, Typed_number.C_number, ""
| TUnOp(LNot, t) ->
- let ty = Typing.get_op ~lenv t in
+ let ty = Typing.get_op ~logic_env t in
if Gmp_types.Z.is_t ty then
(* [!t] is converted into [t == 0] *)
let zero = Logic_const.tinteger 0 in
- let ctx = Typing.get_number_ty ~lenv t in
- Typing.type_term ~use_gmp_opt:true ~ctx ~lenv zero;
+ let ctx = Typing.get_number_ty ~logic_env t in
+ Typing.preprocess_term ~use_gmp_opt:true ~ctx ~logic_env zero;
let e, adata, env =
Translate_utils.comparison_to_exp
~adata
@@ -346,7 +345,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
e, adata, env, Typed_number.C_number, ""
end
| TBinOp(PlusA | MinusA | Mult as bop, t1, t2) ->
- let ty = Typing.get_typ ~lenv t in
+ let ty = Typing.get_typ ~logic_env t in
let e1, adata, env = to_exp ~adata kf env t1 in
let e2, adata, env = to_exp ~adata kf env t2 in
if Gmp_types.Z.is_t ty then
@@ -369,7 +368,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
e, adata, env, Typed_number.C_number, ""
end
| TBinOp(Div | Mod as bop, t1, t2) ->
- let ty = Typing.get_typ ~lenv t in
+ let ty = Typing.get_typ ~logic_env t in
let e1, adata, env = to_exp ~adata kf env t1 in
let t2_to_exp adata env = to_exp ~adata kf env t2 in
if Gmp_types.Z.is_t ty then
@@ -382,14 +381,14 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
let adata, env = Assert.merge_right ~loc env adata2 adata in
(* TODO: preventing division by zero should not be required anymore.
RTE should do this automatically. *)
- let ctx = Typing.get_number_ty ~lenv t in
+ let ctx = Typing.get_number_ty ~logic_env t in
let t = Some t in
let name = Gmp.name_of_mpz_arith_bop bop in
(* [TODO] can now do better since the type system got some info about
possible values of [t2] *)
(* guarding divisions and modulos *)
let zero = Logic_const.tinteger 0 in
- Typing.type_term ~use_gmp_opt:true ~ctx ~lenv zero;
+ Typing.preprocess_term ~use_gmp_opt:true ~ctx ~logic_env zero;
(* do not generate [e2] from [t2] twice *)
let guard, _, env =
let name = Misc.name_of_binop bop ^ "_guard" in
@@ -439,7 +438,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
end
| TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
(* comparison operators *)
- let ity = Typing.get_integer_op ~lenv t in
+ let ity = Typing.get_integer_op ~logic_env t in
let e, adata, env =
Translate_utils.comparison_to_exp
~adata
@@ -455,7 +454,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
e, adata, env, Typed_number.C_number, ""
| TBinOp((Shiftlt | Shiftrt) as bop, t1, t2) ->
(* left/right shift *)
- let ty = Typing.get_typ ~lenv t in
+ let ty = Typing.get_typ ~logic_env t in
let t1_to_exp adata env = to_exp ~adata kf env t1 in
let t2_to_exp adata env = to_exp ~adata kf env t2 in
if Gmp_types.Z.is_t ty then
@@ -480,13 +479,12 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
| TLogic_coerce (_, t) -> term_to_name t
| _ -> ""
in
- let ctx = Typing.get_number_ty ~lenv t in
+ let ctx = Typing.get_number_ty ~logic_env t in
let bop_name = Misc.name_of_binop bop in
let e1_name = term_to_name t1 in
let e2_name = term_to_name t2 in
let zero = Logic_const.tinteger 0 in
- Typing.type_term ~use_gmp_opt:true ~ctx ~lenv zero;
-
+ Typing.preprocess_term ~use_gmp_opt:true ~ctx ~logic_env zero;
(* Check that e2 is representable in mp_bitcnt_t *)
let coerce_guard, env =
let name = e2_name ^ bop_name ^ "_guard" in
@@ -520,7 +518,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
in
let pname = bop_name ^ "_rhs_fits_in_mp_bitcnt_t" in
let pred = { pred with pred_name = pname :: pred.pred_name } in
- Typing.preprocess_predicate (Env.Local_vars.get env) pred;
+ Typing.preprocess_predicate ~logic_env:(Env.Logic_env.get env) pred;
let cond, env =
Assert.runtime_check
~adata:adata2
@@ -600,7 +598,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
in
let e1_guard_cond, env =
let pred = Logic_const.prel ~loc (Rge, t1, zero) in
- Typing.preprocess_predicate (Env.Local_vars.get env) pred;
+ Typing.preprocess_predicate ~logic_env:(Env.Logic_env.get env) pred;
let cond, env =
Assert.runtime_check
~adata:adata1
@@ -681,7 +679,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
e, adata, env, Typed_number.C_number, ""
| TBinOp((BOr | BXor | BAnd) as bop, t1, t2) ->
(* other logic/arith operators *)
- let ty = Typing.get_typ ~lenv t in
+ let ty = Typing.get_typ ~logic_env t in
let e1, adata, env = to_exp ~adata kf env t1 in
let e2, adata, env = to_exp ~adata kf env t2 in
if Gmp_types.Z.is_t ty then
@@ -716,16 +714,16 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
let e = Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)) in
e, adata, env, Typed_number.C_number, ""
| TBinOp(MinusPP, t1, t2) ->
- begin match Typing.get_number_ty ~lenv t with
- | Typing.C_integer _ ->
+ begin match Typing.get_number_ty ~logic_env t with
+ | C_integer _ ->
let e1, adata, env = to_exp ~adata kf env t1 in
let e2, adata, env = to_exp ~adata kf env t2 in
- let ty = Typing.get_typ ~lenv t in
+ let ty = Typing.get_typ ~logic_env t in
let e = Cil.new_exp ~loc (BinOp(MinusPP, e1, e2, ty)) in
e, adata, env, Typed_number.C_number, ""
- | Typing.Gmpz ->
+ | Gmpz ->
Env.not_yet env "pointer subtraction resulting in gmp"
- | Typing.(C_float _ | Rational | Real | Nan) ->
+ | C_float _ | Rational | Real | Nan ->
assert false
end
| TCastE(ty, t') ->
@@ -861,7 +859,6 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
let e, adata, env = to_exp ~adata kf env t in
(* Remove the logic var from the logic scope *)
let env = Env.Logic_scope.remove env lvs in
- Interval.Env.remove li.l_var_info;
e, adata, env, Typed_number.C_number, ""
(* Convert an ACSL term into a corresponding C expression (if any) in the given
@@ -871,8 +868,9 @@ and to_exp ~adata ?inplace kf env t =
let generate_rte = Env.generate_rte env in
Options.feedback ~dkey ~level:4 "translating term %a (rte? %b)in local \
environment '%a'"
- Printer.pp_term t generate_rte Typing.Function_params_ty.pretty
- (Env.Local_vars.get env);
+ Printer.pp_term t generate_rte Profile.pretty
+ (Env.Logic_env.get_profile env);
+ let logic_env = Env.Logic_env.get env in
let t = Logic_normalizer.get_term t in
Extlib.flatten
(Env.with_params_and_result
@@ -884,7 +882,7 @@ and to_exp ~adata ?inplace kf env t =
let env =
if generate_rte then !translate_rte_exp_ref kf env e else env
in
- let cast = Typing.get_cast ~lenv:(Env.Local_vars.get env) t in
+ let cast = Typing.get_cast ~logic_env t in
let name = if name = "" then None else Some name in
Extlib.nest
adata
@@ -924,7 +922,8 @@ let untyped_to_exp typ t =
| _ -> Typing.nan
in
let ctx = Option.map ctx_of_typ typ in
- Typing.type_term ~use_gmp_opt:true ~lenv:[] ?ctx t;
+ let logic_env = Logic_env.empty in
+ Typing.preprocess_term ~use_gmp_opt:true ~logic_env ?ctx t;
let env = Env.push Env.empty in
let env = Env.set_rte env false in
let e, _, env =
diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.ml b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
index 053ccd96994e8114c97f1a7fbeae521077b45c2c..5b6f157fc6c94f5b8c41fc08f5624e2c122cea64 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_utils.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
@@ -23,6 +23,7 @@
(** Utility functions for generating C implementations. *)
open Cil_types
+open Analyses_types
module Error = Translation_error
(**************************************************************************)
@@ -78,7 +79,7 @@ let () =
E_acsl_visitor.must_translate_ppt_opt_ref := must_translate_opt
let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
- let lenv = Env.Local_vars.get env in
+ let logic_env = Env.Logic_env.get env in
let pp = match pp with Some size_pp -> size_pp | None -> t in
let sizet = Cil.(theMachine.typeOfSizeOf) in
let stmts = [] in
@@ -93,7 +94,7 @@ let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
pred_name = pred_name :: lower_guard_pp.pred_name }
in
let lower_guard = Logic_const.prel ~loc (Rge, t, zero_term) in
- Typing.type_named_predicate ~lenv lower_guard;
+ Typing.preprocess_predicate ~logic_env lower_guard;
let adata_lower_guard, env = Assert.empty ~loc kf env in
let lower_guard, adata_lower_guard, env =
!predicate_to_exp_ref ~adata:adata_lower_guard kf env lower_guard
@@ -123,7 +124,7 @@ let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
pred_name = pred_name :: upper_guard_pp.pred_name }
in
let upper_guard = Logic_const.prel ~loc (Rle, t, sizet_max) in
- Typing.type_named_predicate ~lenv upper_guard;
+ Typing.preprocess_predicate ~logic_env upper_guard;
let adata_upper_guard, env = Assert.empty ~loc kf env in
let upper_guard, adata_upper_guard, env =
!predicate_to_exp_ref ~adata:adata_upper_guard kf env upper_guard
@@ -202,9 +203,9 @@ let comparison_to_exp
Env.not_yet env "comparison between two structs or unions"
| Logic_aggr.NotAggregate, Logic_aggr.NotAggregate -> begin
match ity with
- | Typing.C_integer _ | Typing.C_float _ | Typing.Nan ->
+ | C_integer _ | C_float _ | Nan ->
Cil.mkBinOp ~loc bop e1 e2, env
- | Typing.Gmpz ->
+ | Gmpz ->
let _, e, env = Env.new_var
~loc
env
@@ -220,10 +221,8 @@ let comparison_to_exp
[ e1; e2 ] ])
in
Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
- | Typing.Rational ->
- Rational.cmp ~loc bop e1 e2 env kf t_opt
- | Typing.Real ->
- Error.not_yet "comparison involving real numbers"
+ | Rational -> Rational.cmp ~loc bop e1 e2 env kf t_opt
+ | Real -> Error.not_yet "comparison involving real numbers"
end
| _, _ ->
Options.fatal
@@ -244,7 +243,7 @@ let conditional_to_exp ?(name="if") ~loc kf t_opt e1 (e2, env2) (e3, env3) =
| _ ->
let ty = match t_opt with
| None (* predicate *) -> Cil.intType
- | Some t -> Typing.get_typ ~lenv:(Env.Local_vars.get env) t
+ | Some t -> Typing.get_typ ~logic_env:(Env.Logic_env.get env) t
in
let _, e, env =
Env.new_var
@@ -278,19 +277,16 @@ let env_of_li ~adata ~loc kf env li =
match li.l_var_info.lv_type with
| Ctype _ | Linteger | Lreal ->
let t = Misc.term_of_li li in
- let lenv = Env.Local_vars.get env in
- let ty = Typing.get_typ ~lenv t in
+ let logic_env = Env.Logic_env.get env in
+ let ty = Typing.get_typ ~logic_env t in
let vi, vi_e, env = Env.Logic_binding.add ~ty env kf li.l_var_info in
let e, adata, env = !term_to_exp_ref ~adata kf env t in
- let stmt = match Typing.get_number_ty ~lenv t with
- | Typing.(C_integer _ | C_float _ | Nan) ->
+ let stmt = match Typing.get_number_ty ~logic_env t with
+ | C_integer _ | C_float _ | Nan ->
Smart_stmt.assigns ~loc ~result:(Cil.var vi) e
- | Typing.Gmpz ->
- Gmp.init_set ~loc (Cil.var vi) vi_e e
- | Typing.Rational ->
- Rational.init_set ~loc (Cil.var vi) vi_e e
- | Typing.Real ->
- Error.not_yet "real number"
+ | Gmpz -> Gmp.init_set ~loc (Cil.var vi) vi_e e
+ | Rational -> Rational.init_set ~loc (Cil.var vi) vi_e e
+ | Real -> Error.not_yet "real number"
in
adata, Env.add_stmt env stmt
| Ltype _ ->
diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.mli b/src/plugins/e-acsl/src/code_generator/translate_utils.mli
index 2932dd4db854cbab3e1f6b0edf5308a4a28500a3..ba8841aa2f4f3b5dc492319326e267840f7f4a39 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_utils.mli
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.mli
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+open Analyses_types
(** Utility functions for generating C implementations. *)
@@ -55,7 +56,7 @@ val comparison_to_exp:
loc:location ->
kernel_function ->
Env.t ->
- Typing.number_ty ->
+ number_ty ->
?e1:exp ->
binop ->
term ->
diff --git a/src/plugins/e-acsl/src/libraries/error.ml b/src/plugins/e-acsl/src/libraries/error.ml
index 1b32febdce7a0fec8334dbcd7246080599f18543..008b0352355ed5f6b8670889f89d3cf2e3c18a50 100644
--- a/src/plugins/e-acsl/src/libraries/error.ml
+++ b/src/plugins/e-acsl/src/libraries/error.ml
@@ -54,6 +54,9 @@ module type S = sig
Format.formatter ->
'a result ->
unit
+ val map: ('a -> 'b) -> 'a result -> 'b
+ val map2: ('a -> 'b -> 'c) -> 'a result -> 'b result -> 'c
+ val map3 : ('a -> 'b -> 'c -> 'd) -> 'a result -> 'b result -> 'c result -> 'd
end
module Make_with_opt(P: sig val phase:Options.category option end): S = struct
@@ -125,6 +128,24 @@ module Make_with_opt(P: sig val phase:Options.category option end): S = struct
match res with
| Result.Ok a -> Format.fprintf fmt "@[%a@]" pp a
| Result.Error err -> Format.fprintf fmt "@[%s@]" (Printexc.to_string err)
+
+ let map f = function
+ | Result.Ok a -> f a
+ | Result.Error e -> raise e
+
+ let map2 f a b =
+ match a,b with
+ | Result.Ok a, Result.Ok b -> f a b
+ | Result.Ok _, Result.Error e
+ | Result.Error e, _ -> raise e
+
+ let map3 f a b c =
+ match a,b,c with
+ | Result.Ok a, Result.Ok b, Result.Ok c -> f a b c
+ | Result.Ok _, Result.Ok _, Result.Error e
+ | Result.Ok _, Result.Error e, _
+ | Result.Error e, _, _ -> raise e
+
end
module Make(P: sig val phase:Options.category end): S =
diff --git a/src/plugins/e-acsl/src/libraries/error.mli b/src/plugins/e-acsl/src/libraries/error.mli
index 599ec5cd1bb75d6f3c6d4d5c5ce1307d45e9577a..a4a690ab56a1d450b0993c1e4806a9f743056021 100644
--- a/src/plugins/e-acsl/src/libraries/error.mli
+++ b/src/plugins/e-acsl/src/libraries/error.mli
@@ -81,8 +81,14 @@ module type S = sig
Format.formatter ->
'a result ->
unit
- (** [pp_result pp] where [pp] is a formatter for ['a] returns a formatter for
- ['a result]. *)
+ (** [pp_result pp] where [pp] is a formatter for ['a] returns a formatter for
+ ['a result]. *)
+
+ val map : ('a -> 'b) -> 'a result -> 'b
+ val map2 : ('a -> 'b -> 'c) -> 'a result -> 'b result -> 'c
+ val map3 : ('a -> 'b -> 'c -> 'd) -> 'a result -> 'b result -> 'c result -> 'd
+ (** Apply a function to one or several results and propagate the errors *)
+
end
(** Functor to build an [Error] module for a given [phase]. *)
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
index 7310815d56d7fe3e9e947326d43ec61708b8801c..722a30329dc0d8844b5db2c70565c8812edee5a3 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
@@ -20,8 +20,6 @@
[eva:alarm] functions.c:53: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:53: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] functions.c:54: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] functions.c:55: Warning:
@@ -33,14 +31,14 @@
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
[eva:alarm] functions.c:63: Warning:
- function __e_acsl_assert_register_int: precondition data->values == \null ||
- \valid(data->values) got status unknown.
+ function __e_acsl_assert_register_char: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
[eva:alarm] functions.c:63: Warning:
function __e_acsl_assert_register_char: precondition data->values == \null ||
\valid(data->values) got status unknown.
[eva:alarm] functions.c:65: Warning:
- function __e_acsl_assert_register_int: precondition data->values == \null ||
- \valid(data->values) got status unknown.
+ function __e_acsl_assert_register_short: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
[eva:alarm] functions.c:65: Warning:
function __e_acsl_assert_register_short: precondition data->values == \null ||
\valid(data->values) got status unknown.
@@ -54,7 +52,7 @@
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
[eva:alarm] functions.c:75: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__10);
+ non-finite double value. assert \is_finite(__gen_e_acsl__9);
[eva:alarm] functions.c:75: Warning:
function __e_acsl_assert_register_double: precondition data->values == \null ||
\valid(data->values) got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c b/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
index d50114664a1ca05ec58bf00723475d14bbf31219..598514c5351e05f34baf16d146d26c670296530c 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
@@ -436,7 +436,7 @@ int main(void)
else {
{
int __gen_e_acsl_if_2;
- if ((int)(__gen_e_acsl_k_9 % 2UL) == 1) __gen_e_acsl_if_2 = 1;
+ if ((int)(__gen_e_acsl_k_9 % 2U) == 1) __gen_e_acsl_if_2 = 1;
else __gen_e_acsl_if_2 = 0;
__gen_e_acsl_lambda_9 = __gen_e_acsl_if_2;
}
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
index 35d9f436ac7691d26e8b80ccad01a9bea10e72f6..192abded1c01d4e34b486e5e9ec1cb56a80a8f3c 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -22,14 +22,14 @@ int __gen_e_acsl_p1(int x, int y);
*/
int __gen_e_acsl_p2(int x, int y);
-int __gen_e_acsl_p2_5(int x, long y);
-
int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y);
+int __gen_e_acsl_p2_5(int x, int y);
+
/*@ logic integer f1(integer x, integer y) = x + y;
*/
-long __gen_e_acsl_f1(int x, int y);
+int __gen_e_acsl_f1_3(int x, int y);
void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
__e_acsl_mpz_struct * y);
@@ -37,13 +37,15 @@ void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
__e_acsl_mpz_struct * y);
+long __gen_e_acsl_f1(int x, int y);
+
/*@ logic char h_char(char c) = c;
*/
-int __gen_e_acsl_h_char(int c);
+char __gen_e_acsl_h_char(char c);
/*@ logic short h_short(short s) = s;
*/
-int __gen_e_acsl_h_short(int s);
+short __gen_e_acsl_h_short(short s);
/*@ logic int g_hidden(int x) = x;
*/
@@ -88,7 +90,7 @@ double __gen_e_acsl_f2(double x);
/*@ logic integer f_sum(integer x) = \sum(1, x, \lambda integer y; 1);
*/
-unsigned int __gen_e_acsl_f_sum(int x);
+int __gen_e_acsl_f_sum(int x);
int main(void)
{
@@ -174,14 +176,14 @@ int main(void)
}
/*@ assert f1(x, y) == 3; */ ;
{
- long __gen_e_acsl_f1_4;
+ int __gen_e_acsl_f1_4;
int __gen_e_acsl_p2_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
- __gen_e_acsl_f1_4 = __gen_e_acsl_f1(3,4);
+ __gen_e_acsl_f1_4 = __gen_e_acsl_f1_3(3,4);
__gen_e_acsl_p2_6 = __gen_e_acsl_p2_5(x,__gen_e_acsl_f1_4);
- __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_5,"f1(3, 4)",0,
- __gen_e_acsl_f1_4);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_5,"f1(3, 4)",0,
+ __gen_e_acsl_f1_4);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_5,"x",0,x);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_5,
"p2(x, f1(3, 4))",0,__gen_e_acsl_p2_6);
@@ -196,18 +198,18 @@ int main(void)
}
/*@ assert p2(x, f1(3, 4)); */ ;
{
- __e_acsl_mpz_t __gen_e_acsl__4;
+ __e_acsl_mpz_t __gen_e_acsl__3;
__e_acsl_mpz_t __gen_e_acsl_f1_6;
- __e_acsl_mpz_t __gen_e_acsl__5;
- int __gen_e_acsl_gt_3;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_gt_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
- __gmpz_init_set_str(__gen_e_acsl__4,"99999999999999999999999999999",10);
+ __gmpz_init_set_str(__gen_e_acsl__3,"99999999999999999999999999999",10);
__gen_e_acsl_f1_5(& __gen_e_acsl_f1_6,9,
- (__e_acsl_mpz_struct *)__gen_e_acsl__4);
- __gmpz_init_set_si(__gen_e_acsl__5,0L);
- __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ (__e_acsl_mpz_struct *)__gen_e_acsl__3);
+ __gmpz_init_set_si(__gen_e_acsl__4,0L);
+ __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,
"f1(9, 99999999999999999999999999999)",0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6));
@@ -217,27 +219,27 @@ int main(void)
__gen_e_acsl_assert_data_6.file = "functions.c";
__gen_e_acsl_assert_data_6.fct = "main";
__gen_e_acsl_assert_data_6.line = 54;
- __e_acsl_assert(__gen_e_acsl_gt_3 > 0,& __gen_e_acsl_assert_data_6);
+ __e_acsl_assert(__gen_e_acsl_gt_2 > 0,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
- __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl__3);
__gmpz_clear(__gen_e_acsl_f1_6);
- __gmpz_clear(__gen_e_acsl__5);
+ __gmpz_clear(__gen_e_acsl__4);
}
/*@ assert f1(9, 99999999999999999999999999999) > 0; */ ;
{
- __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl__5;
__e_acsl_mpz_t __gen_e_acsl_f1_8;
- __e_acsl_mpz_t __gen_e_acsl__7;
+ __e_acsl_mpz_t __gen_e_acsl__6;
int __gen_e_acsl_eq;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
- __gmpz_init_set_str(__gen_e_acsl__6,"99999999999999999999999999999",10);
+ __gmpz_init_set_str(__gen_e_acsl__5,"99999999999999999999999999999",10);
__gen_e_acsl_f1_7(& __gen_e_acsl_f1_8,
- (__e_acsl_mpz_struct *)__gen_e_acsl__6,
- (__e_acsl_mpz_struct *)__gen_e_acsl__6);
- __gmpz_init_set_str(__gen_e_acsl__7,"199999999999999999999999999998",10);
+ (__e_acsl_mpz_struct *)__gen_e_acsl__5,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__5);
+ __gmpz_init_set_str(__gen_e_acsl__6,"199999999999999999999999999998",10);
__gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_8),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_7,
"f1(99999999999999999999999999999, 99999999999999999999999999999)",
0,
@@ -250,9 +252,9 @@ int main(void)
__gen_e_acsl_assert_data_7.line = 55;
__e_acsl_assert(__gen_e_acsl_eq == 0,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
- __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl__5);
__gmpz_clear(__gen_e_acsl_f1_8);
- __gmpz_clear(__gen_e_acsl__7);
+ __gmpz_clear(__gen_e_acsl__6);
}
/*@
assert
@@ -280,13 +282,13 @@ int main(void)
/*@ assert g(x) == x; */ ;
char c = (char)'c';
{
- int __gen_e_acsl_h_char_2;
+ char __gen_e_acsl_h_char_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_9 =
{.values = (void *)0};
- __gen_e_acsl_h_char_2 = __gen_e_acsl_h_char((int)c);
+ __gen_e_acsl_h_char_2 = __gen_e_acsl_h_char(c);
__e_acsl_assert_register_char(& __gen_e_acsl_assert_data_9,"c",0,c);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_9,"h_char(c)",0,
- __gen_e_acsl_h_char_2);
+ __e_acsl_assert_register_char(& __gen_e_acsl_assert_data_9,"h_char(c)",0,
+ __gen_e_acsl_h_char_2);
__e_acsl_assert_register_char(& __gen_e_acsl_assert_data_9,"c",0,c);
__gen_e_acsl_assert_data_9.blocking = 1;
__gen_e_acsl_assert_data_9.kind = "Assertion";
@@ -294,20 +296,20 @@ int main(void)
__gen_e_acsl_assert_data_9.file = "functions.c";
__gen_e_acsl_assert_data_9.fct = "main";
__gen_e_acsl_assert_data_9.line = 63;
- __e_acsl_assert(__gen_e_acsl_h_char_2 == (int)c,
+ __e_acsl_assert((int)__gen_e_acsl_h_char_2 == (int)c,
& __gen_e_acsl_assert_data_9);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_9);
}
/*@ assert h_char(c) == c; */ ;
short s = (short)1;
{
- int __gen_e_acsl_h_short_2;
+ short __gen_e_acsl_h_short_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_10 =
{.values = (void *)0};
- __gen_e_acsl_h_short_2 = __gen_e_acsl_h_short((int)s);
+ __gen_e_acsl_h_short_2 = __gen_e_acsl_h_short(s);
__e_acsl_assert_register_short(& __gen_e_acsl_assert_data_10,"s",0,s);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_10,"h_short(s)",
- 0,__gen_e_acsl_h_short_2);
+ __e_acsl_assert_register_short(& __gen_e_acsl_assert_data_10,
+ "h_short(s)",0,__gen_e_acsl_h_short_2);
__e_acsl_assert_register_short(& __gen_e_acsl_assert_data_10,"s",0,s);
__gen_e_acsl_assert_data_10.blocking = 1;
__gen_e_acsl_assert_data_10.kind = "Assertion";
@@ -315,7 +317,7 @@ int main(void)
__gen_e_acsl_assert_data_10.file = "functions.c";
__gen_e_acsl_assert_data_10.fct = "main";
__gen_e_acsl_assert_data_10.line = 65;
- __e_acsl_assert(__gen_e_acsl_h_short_2 == (int)s,
+ __e_acsl_assert((int)__gen_e_acsl_h_short_2 == (int)s,
& __gen_e_acsl_assert_data_10);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_10);
}
@@ -364,19 +366,19 @@ int main(void)
}
/*@ assert f2(d) > 0; */ ;
{
- unsigned int __gen_e_acsl_f_sum_2;
+ int __gen_e_acsl_f_sum_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_13 =
{.values = (void *)0};
__gen_e_acsl_f_sum_2 = __gen_e_acsl_f_sum(100);
- __e_acsl_assert_register_uint(& __gen_e_acsl_assert_data_13,"f_sum(100)",
- 0,__gen_e_acsl_f_sum_2);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_13,"f_sum(100)",
+ 0,__gen_e_acsl_f_sum_2);
__gen_e_acsl_assert_data_13.blocking = 1;
__gen_e_acsl_assert_data_13.kind = "Assertion";
__gen_e_acsl_assert_data_13.pred_txt = "f_sum(100) == 100";
__gen_e_acsl_assert_data_13.file = "functions.c";
__gen_e_acsl_assert_data_13.fct = "main";
__gen_e_acsl_assert_data_13.line = 77;
- __e_acsl_assert(__gen_e_acsl_f_sum_2 == 100U,
+ __e_acsl_assert(__gen_e_acsl_f_sum_2 == 100,
& __gen_e_acsl_assert_data_13);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_13);
}
@@ -421,33 +423,7 @@ int __gen_e_acsl_p1(int x, int y)
assigns \result \from x, y; */
int __gen_e_acsl_p2(int x, int y)
{
- int __retres = x + (long)y > 0L;
- return __retres;
-}
-
-/*@ assigns \result;
- assigns \result \from x, y; */
-int __gen_e_acsl_p2_5(int x, long y)
-{
- __e_acsl_mpz_t __gen_e_acsl_x_2;
- __e_acsl_mpz_t __gen_e_acsl_y;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
- __e_acsl_mpz_t __gen_e_acsl__3;
- int __gen_e_acsl_gt_2;
- __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_y,y);
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y));
- __gmpz_init_set_si(__gen_e_acsl__3,0L);
- __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- int __retres = __gen_e_acsl_gt_2 > 0;
- __gmpz_clear(__gen_e_acsl_x_2);
- __gmpz_clear(__gen_e_acsl_y);
- __gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl__3);
+ int __retres = x + y > 0;
return __retres;
}
@@ -475,9 +451,17 @@ int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
/*@ assigns \result;
assigns \result \from x, y; */
-long __gen_e_acsl_f1(int x, int y)
+int __gen_e_acsl_p2_5(int x, int y)
{
- long __retres = x + (long)y;
+ int __retres = x + (long)y > 0L;
+ return __retres;
+}
+
+/*@ assigns \result;
+ assigns \result \from x, y; */
+int __gen_e_acsl_f1_3(int x, int y)
+{
+ int __retres = x + y;
return __retres;
}
@@ -487,17 +471,17 @@ long __gen_e_acsl_f1(int x, int y)
void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
__e_acsl_mpz_struct * y)
{
- __e_acsl_mpz_t __gen_e_acsl_x_3;
- __e_acsl_mpz_t __gen_e_acsl_add_3;
- __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
- __gmpz_init(__gen_e_acsl_add_3);
- __gmpz_add(__gen_e_acsl_add_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
+ __e_acsl_mpz_t __gen_e_acsl_x_2;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
(__e_acsl_mpz_struct const *)(y));
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
- __gmpz_clear(__gen_e_acsl_x_3);
- __gmpz_clear(__gen_e_acsl_add_3);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gmpz_clear(__gen_e_acsl_x_2);
+ __gmpz_clear(__gen_e_acsl_add_2);
return;
}
@@ -508,26 +492,34 @@ void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
__e_acsl_mpz_struct * y)
{
- __e_acsl_mpz_t __gen_e_acsl_add_4;
- __gmpz_init(__gen_e_acsl_add_4);
- __gmpz_add(__gen_e_acsl_add_4,(__e_acsl_mpz_struct const *)(x),
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,(__e_acsl_mpz_struct const *)(x),
(__e_acsl_mpz_struct const *)(y));
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
- __gmpz_clear(__gen_e_acsl_add_4);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
+ __gmpz_clear(__gen_e_acsl_add_3);
return;
}
+/*@ assigns \result;
+ assigns \result \from x, y; */
+long __gen_e_acsl_f1(int x, int y)
+{
+ long __retres = x + (long)y;
+ return __retres;
+}
+
/*@ assigns \result;
assigns \result \from c; */
-int __gen_e_acsl_h_char(int c)
+char __gen_e_acsl_h_char(char c)
{
return c;
}
/*@ assigns \result;
assigns \result \from s; */
-int __gen_e_acsl_h_short(int s)
+short __gen_e_acsl_h_short(short s)
{
return s;
}
@@ -575,46 +567,46 @@ int __gen_e_acsl_k_pred(int x)
assigns \result \from x; */
double __gen_e_acsl_f2(double x)
{
+ __e_acsl_mpq_t __gen_e_acsl__7;
__e_acsl_mpq_t __gen_e_acsl__8;
- __e_acsl_mpq_t __gen_e_acsl__9;
__e_acsl_mpq_t __gen_e_acsl_div;
- double __gen_e_acsl__10;
+ double __gen_e_acsl__9;
+ __gmpq_init(__gen_e_acsl__7);
+ __gmpq_set_str(__gen_e_acsl__7,"1",10);
__gmpq_init(__gen_e_acsl__8);
- __gmpq_set_str(__gen_e_acsl__8,"1",10);
- __gmpq_init(__gen_e_acsl__9);
- __gmpq_set_d(__gen_e_acsl__9,x);
+ __gmpq_set_d(__gen_e_acsl__8,x);
__gmpq_init(__gen_e_acsl_div);
- __gmpq_div(__gen_e_acsl_div,(__e_acsl_mpq_struct const *)(__gen_e_acsl__8),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__9));
- __gen_e_acsl__10 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
+ __gmpq_div(__gen_e_acsl_div,(__e_acsl_mpq_struct const *)(__gen_e_acsl__7),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
+ __gen_e_acsl__9 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
+ __gmpq_clear(__gen_e_acsl__7);
__gmpq_clear(__gen_e_acsl__8);
- __gmpq_clear(__gen_e_acsl__9);
__gmpq_clear(__gen_e_acsl_div);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__10); */
- return __gen_e_acsl__10;
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__9); */
+ return __gen_e_acsl__9;
}
/*@ assigns \result;
assigns \result \from x; */
-unsigned int __gen_e_acsl_f_sum(int x)
+int __gen_e_acsl_f_sum(int x)
{
- long __gen_e_acsl_y_2;
- long __gen_e_acsl_one;
+ int __gen_e_acsl_y;
+ int __gen_e_acsl_one;
int __gen_e_acsl_cond;
- unsigned int __gen_e_acsl_lambda;
- unsigned int __gen_e_acsl_accumulator;
+ int __gen_e_acsl_lambda;
+ int __gen_e_acsl_accumulator;
__gen_e_acsl_one = 1;
__gen_e_acsl_cond = 0;
__gen_e_acsl_lambda = 0;
__gen_e_acsl_accumulator = 0;
- __gen_e_acsl_y_2 = 1L;
+ __gen_e_acsl_y = 1;
while (1) {
- __gen_e_acsl_cond = __gen_e_acsl_y_2 > (long)x;
+ __gen_e_acsl_cond = __gen_e_acsl_y > x;
if (__gen_e_acsl_cond) break;
else {
__gen_e_acsl_lambda = 1;
__gen_e_acsl_accumulator += __gen_e_acsl_lambda;
- __gen_e_acsl_y_2 += __gen_e_acsl_one;
+ __gen_e_acsl_y += __gen_e_acsl_one;
}
}
return __gen_e_acsl_accumulator;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
index b38e3178766ffb17f3fb1c472b78e599e36e0dbb..fb1832ca1932365758dee4c7644baaca1cd4882a 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
@@ -11,38 +11,42 @@ extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
/*@ logic integer f1(integer n) = n <= 0? 0: f1(n - 1) + n;
*/
-void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n);
-
void __gen_e_acsl_f1_2(__e_acsl_mpz_t *__retres_arg, long n);
+void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n);
+
void __gen_e_acsl_f1_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
/*@
logic integer f2(integer n) = n < 0? 1: (f2(n - 1) * f2(n - 2)) / f2(n - 3);
*/
-int __gen_e_acsl_f2(int n);
-
int __gen_e_acsl_f2_2(long n);
+int __gen_e_acsl_f2(int n);
+
int __gen_e_acsl_f2_3(__e_acsl_mpz_struct * n);
/*@ logic integer g(integer n) = 0;
*/
+int __gen_e_acsl_g_3(long n);
+
+int __gen_e_acsl_g_9(__e_acsl_mpz_struct * n);
+
int __gen_e_acsl_g(int n);
-int __gen_e_acsl_g_3(long n);
+int __gen_e_acsl_g_11(long n);
int __gen_e_acsl_g_5(__e_acsl_mpz_struct * n);
/*@ logic integer f3(integer n) = n > 0? g(n) * f3(n - 1) - 5: g(n + 1);
*/
-int __gen_e_acsl_f3(int n);
-
int __gen_e_acsl_f3_2(long n);
+int __gen_e_acsl_f3(int n);
+
int __gen_e_acsl_f3_3(__e_acsl_mpz_struct * n);
/*@
@@ -50,19 +54,19 @@ logic integer f4(integer n) =
n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
*/
-unsigned long __gen_e_acsl_f4(int n);
-
unsigned long __gen_e_acsl_f4_2(long n);
+unsigned long __gen_e_acsl_f4(int n);
+
unsigned long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * n);
/*@ logic integer f5(integer n) = n >= 0? 0: f5(n + 1) + n;
*/
-void __gen_e_acsl_f5(__e_acsl_mpz_t *__retres_arg, int n);
-
void __gen_e_acsl_f5_2(__e_acsl_mpz_t *__retres_arg, long n);
+void __gen_e_acsl_f5(__e_acsl_mpz_t *__retres_arg, int n);
+
void __gen_e_acsl_f5_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
int main(void)
@@ -248,40 +252,6 @@ int main(void)
return __retres;
}
-/*@ assigns (*__retres_arg)[0];
- assigns (*__retres_arg)[0] \from n; */
-void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n)
-{
- __e_acsl_mpz_t __gen_e_acsl_if_3;
- if (n <= 0) {
- __e_acsl_mpz_t __gen_e_acsl_;
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gmpz_init_set(__gen_e_acsl_if_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gmpz_clear(__gen_e_acsl_);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_f1_7;
- __e_acsl_mpz_t __gen_e_acsl_n_2;
- __e_acsl_mpz_t __gen_e_acsl_add_3;
- __gen_e_acsl_f1_2(& __gen_e_acsl_f1_7,n - 1L);
- __gmpz_init_set_si(__gen_e_acsl_n_2,(long)n);
- __gmpz_init(__gen_e_acsl_add_3);
- __gmpz_add(__gen_e_acsl_add_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2));
- __gmpz_init_set(__gen_e_acsl_if_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
- __gmpz_clear(__gen_e_acsl_f1_7);
- __gmpz_clear(__gen_e_acsl_n_2);
- __gmpz_clear(__gen_e_acsl_add_3);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_3));
- __gmpz_clear(__gen_e_acsl_if_3);
- return;
-}
-
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f1_2(__e_acsl_mpz_t *__retres_arg, long n)
@@ -330,6 +300,40 @@ void __gen_e_acsl_f1_2(__e_acsl_mpz_t *__retres_arg, long n)
return;
}
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from n; */
+void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n)
+{
+ __e_acsl_mpz_t __gen_e_acsl_if_3;
+ if (n <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gmpz_init_set(__gen_e_acsl_if_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_clear(__gen_e_acsl_);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_f1_7;
+ __e_acsl_mpz_t __gen_e_acsl_n_2;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __gen_e_acsl_f1_2(& __gen_e_acsl_f1_7,n - 1L);
+ __gmpz_init_set_si(__gen_e_acsl_n_2,(long)n);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2));
+ __gmpz_init_set(__gen_e_acsl_if_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
+ __gmpz_clear(__gen_e_acsl_f1_7);
+ __gmpz_clear(__gen_e_acsl_n_2);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ }
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_3));
+ __gmpz_clear(__gen_e_acsl_if_3);
+ return;
+}
+
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from *((__e_acsl_mpz_struct *)n);
*/
@@ -381,51 +385,6 @@ void __gen_e_acsl_f1_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
return;
}
-/*@ assigns \result;
- assigns \result \from n; */
-int __gen_e_acsl_f2(int n)
-{
- int __gen_e_acsl_if_6;
- if (n < 0) __gen_e_acsl_if_6 = 1;
- else {
- int __gen_e_acsl_f2_15;
- int __gen_e_acsl_f2_17;
- int __gen_e_acsl_f2_19;
- __gen_e_acsl_f2_15 = __gen_e_acsl_f2_2(n - 1L);
- __gen_e_acsl_f2_17 = __gen_e_acsl_f2_2(n - 2L);
- __gen_e_acsl_f2_19 = __gen_e_acsl_f2_2(n - 3L);
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
- {.values = (void *)0};
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,
- "__gen_e_acsl_f2_19",0,__gen_e_acsl_f2_19);
- __gen_e_acsl_assert_data_7.blocking = 1;
- __gen_e_acsl_assert_data_7.kind = "RTE";
- __gen_e_acsl_assert_data_7.pred_txt = "__gen_e_acsl_f2_19 != 0";
- __gen_e_acsl_assert_data_7.file = "functions_rec.c";
- __gen_e_acsl_assert_data_7.fct = "f2";
- __gen_e_acsl_assert_data_7.line = 13;
- __gen_e_acsl_assert_data_7.name = "division_by_zero";
- __e_acsl_assert(__gen_e_acsl_f2_19 != 0,& __gen_e_acsl_assert_data_7);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
- /*@ assert Eva: division_by_zero: __gen_e_acsl_f2_19 != 0; */
- /*@ assert
- Eva: signed_overflow:
- -2147483648 <= __gen_e_acsl_f2_15 * __gen_e_acsl_f2_17;
- */
- /*@ assert
- Eva: signed_overflow:
- __gen_e_acsl_f2_15 * __gen_e_acsl_f2_17 <= 2147483647;
- */
- /*@ assert
- Eva: signed_overflow:
- (int)(__gen_e_acsl_f2_15 * __gen_e_acsl_f2_17) / __gen_e_acsl_f2_19
- <= 2147483647;
- */
- __gen_e_acsl_if_6 = (__gen_e_acsl_f2_15 * __gen_e_acsl_f2_17) / __gen_e_acsl_f2_19;
- }
- return __gen_e_acsl_if_6;
-}
-
/*@ assigns \result;
assigns \result \from n; */
int __gen_e_acsl_f2_2(long n)
@@ -513,6 +472,51 @@ int __gen_e_acsl_f2_2(long n)
return __gen_e_acsl_if_5;
}
+/*@ assigns \result;
+ assigns \result \from n; */
+int __gen_e_acsl_f2(int n)
+{
+ int __gen_e_acsl_if_6;
+ if (n < 0) __gen_e_acsl_if_6 = 1;
+ else {
+ int __gen_e_acsl_f2_15;
+ int __gen_e_acsl_f2_17;
+ int __gen_e_acsl_f2_19;
+ __gen_e_acsl_f2_15 = __gen_e_acsl_f2_2(n - 1L);
+ __gen_e_acsl_f2_17 = __gen_e_acsl_f2_2(n - 2L);
+ __gen_e_acsl_f2_19 = __gen_e_acsl_f2_2(n - 3L);
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
+ {.values = (void *)0};
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,
+ "__gen_e_acsl_f2_19",0,__gen_e_acsl_f2_19);
+ __gen_e_acsl_assert_data_7.blocking = 1;
+ __gen_e_acsl_assert_data_7.kind = "RTE";
+ __gen_e_acsl_assert_data_7.pred_txt = "__gen_e_acsl_f2_19 != 0";
+ __gen_e_acsl_assert_data_7.file = "functions_rec.c";
+ __gen_e_acsl_assert_data_7.fct = "f2";
+ __gen_e_acsl_assert_data_7.line = 13;
+ __gen_e_acsl_assert_data_7.name = "division_by_zero";
+ __e_acsl_assert(__gen_e_acsl_f2_19 != 0,& __gen_e_acsl_assert_data_7);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
+ /*@ assert Eva: division_by_zero: __gen_e_acsl_f2_19 != 0; */
+ /*@ assert
+ Eva: signed_overflow:
+ -2147483648 <= __gen_e_acsl_f2_15 * __gen_e_acsl_f2_17;
+ */
+ /*@ assert
+ Eva: signed_overflow:
+ __gen_e_acsl_f2_15 * __gen_e_acsl_f2_17 <= 2147483647;
+ */
+ /*@ assert
+ Eva: signed_overflow:
+ (int)(__gen_e_acsl_f2_15 * __gen_e_acsl_f2_17) / __gen_e_acsl_f2_19
+ <= 2147483647;
+ */
+ __gen_e_acsl_if_6 = (__gen_e_acsl_f2_15 * __gen_e_acsl_f2_17) / __gen_e_acsl_f2_19;
+ }
+ return __gen_e_acsl_if_6;
+}
+
/*@ assigns \result;
assigns \result \from *((__e_acsl_mpz_struct *)n); */
int __gen_e_acsl_f2_3(__e_acsl_mpz_struct * n)
@@ -602,23 +606,23 @@ int __gen_e_acsl_f2_3(__e_acsl_mpz_struct * n)
/*@ assigns \result;
assigns \result \from n; */
-int __gen_e_acsl_g(int n)
+int __gen_e_acsl_g_3(long n)
{
int __retres = 0;
return __retres;
}
/*@ assigns \result;
- assigns \result \from n; */
-int __gen_e_acsl_g_3(long n)
+ assigns \result \from *((__e_acsl_mpz_struct *)n); */
+int __gen_e_acsl_g_9(__e_acsl_mpz_struct * n)
{
int __retres = 0;
return __retres;
}
/*@ assigns \result;
- assigns \result \from *((__e_acsl_mpz_struct *)n); */
-int __gen_e_acsl_g_5(__e_acsl_mpz_struct * n)
+ assigns \result \from n; */
+int __gen_e_acsl_g(int n)
{
int __retres = 0;
return __retres;
@@ -626,22 +630,18 @@ int __gen_e_acsl_g_5(__e_acsl_mpz_struct * n)
/*@ assigns \result;
assigns \result \from n; */
-int __gen_e_acsl_f3(int n)
+int __gen_e_acsl_g_11(long n)
{
- int __gen_e_acsl_if_9;
- if (n > 0) {
- int __gen_e_acsl_g_2;
- int __gen_e_acsl_f3_7;
- __gen_e_acsl_g_2 = __gen_e_acsl_g(n);
- __gen_e_acsl_f3_7 = __gen_e_acsl_f3_2(n - 1L);
- __gen_e_acsl_if_9 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_7 - 5;
- }
- else {
- int __gen_e_acsl_g_12;
- __gen_e_acsl_g_12 = __gen_e_acsl_g_3(n + 1L);
- __gen_e_acsl_if_9 = __gen_e_acsl_g_12;
- }
- return __gen_e_acsl_if_9;
+ int __retres = 0;
+ return __retres;
+}
+
+/*@ assigns \result;
+ assigns \result \from *((__e_acsl_mpz_struct *)n); */
+int __gen_e_acsl_g_5(__e_acsl_mpz_struct * n)
+{
+ int __retres = 0;
+ return __retres;
}
/*@ assigns \result;
@@ -683,7 +683,7 @@ int __gen_e_acsl_f3_2(long n)
__gmpz_add(__gen_e_acsl_add_5,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__21));
- __gen_e_acsl_g_10 = __gen_e_acsl_g_5((__e_acsl_mpz_struct *)__gen_e_acsl_add_5);
+ __gen_e_acsl_g_10 = __gen_e_acsl_g_9((__e_acsl_mpz_struct *)__gen_e_acsl_add_5);
__gen_e_acsl_if_8 = __gen_e_acsl_g_10;
__gmpz_clear(__gen_e_acsl_n_5);
__gmpz_clear(__gen_e_acsl__21);
@@ -692,6 +692,26 @@ int __gen_e_acsl_f3_2(long n)
return __gen_e_acsl_if_8;
}
+/*@ assigns \result;
+ assigns \result \from n; */
+int __gen_e_acsl_f3(int n)
+{
+ int __gen_e_acsl_if_9;
+ if (n > 0) {
+ int __gen_e_acsl_g_2;
+ int __gen_e_acsl_f3_7;
+ __gen_e_acsl_g_2 = __gen_e_acsl_g(n);
+ __gen_e_acsl_f3_7 = __gen_e_acsl_f3_2(n - 1L);
+ __gen_e_acsl_if_9 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_7 - 5;
+ }
+ else {
+ int __gen_e_acsl_g_12;
+ __gen_e_acsl_g_12 = __gen_e_acsl_g_11(n + 1L);
+ __gen_e_acsl_if_9 = __gen_e_acsl_g_12;
+ }
+ return __gen_e_acsl_if_9;
+}
+
/*@ assigns \result;
assigns \result \from *((__e_acsl_mpz_struct *)n); */
int __gen_e_acsl_f3_3(__e_acsl_mpz_struct * n)
@@ -742,25 +762,6 @@ int __gen_e_acsl_f3_3(__e_acsl_mpz_struct * n)
return __gen_e_acsl_if_7;
}
-/*@ assigns \result;
- assigns \result \from n; */
-unsigned long __gen_e_acsl_f4(int n)
-{
- unsigned long __gen_e_acsl_if_15;
- if (n < 100) {
- unsigned long __gen_e_acsl_f4_7;
- __gen_e_acsl_f4_7 = __gen_e_acsl_f4_2(n + 1L);
- __gen_e_acsl_if_15 = __gen_e_acsl_f4_7;
- }
- else {
- unsigned long __gen_e_acsl_if_14;
- if ((long)n < 9223372036854775807L) __gen_e_acsl_if_14 = 9223372036854775807UL;
- else __gen_e_acsl_if_14 = 6UL;
- __gen_e_acsl_if_15 = __gen_e_acsl_if_14;
- }
- return __gen_e_acsl_if_15;
-}
-
/*@ assigns \result;
assigns \result \from n; */
unsigned long __gen_e_acsl_f4_2(long n)
@@ -796,6 +797,25 @@ unsigned long __gen_e_acsl_f4_2(long n)
return __gen_e_acsl_if_13;
}
+/*@ assigns \result;
+ assigns \result \from n; */
+unsigned long __gen_e_acsl_f4(int n)
+{
+ unsigned long __gen_e_acsl_if_15;
+ if (n < 100) {
+ unsigned long __gen_e_acsl_f4_7;
+ __gen_e_acsl_f4_7 = __gen_e_acsl_f4_2(n + 1L);
+ __gen_e_acsl_if_15 = __gen_e_acsl_f4_7;
+ }
+ else {
+ unsigned long __gen_e_acsl_if_14;
+ if ((long)n < 9223372036854775807L) __gen_e_acsl_if_14 = 9223372036854775807UL;
+ else __gen_e_acsl_if_14 = 6UL;
+ __gen_e_acsl_if_15 = __gen_e_acsl_if_14;
+ }
+ return __gen_e_acsl_if_15;
+}
+
/*@ assigns \result;
assigns \result \from *((__e_acsl_mpz_struct *)n); */
unsigned long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * n)
@@ -839,40 +859,6 @@ unsigned long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * n)
return __gen_e_acsl_if_11;
}
-/*@ assigns (*__retres_arg)[0];
- assigns (*__retres_arg)[0] \from n; */
-void __gen_e_acsl_f5(__e_acsl_mpz_t *__retres_arg, int n)
-{
- __e_acsl_mpz_t __gen_e_acsl_if_18;
- if (n >= 0) {
- __e_acsl_mpz_t __gen_e_acsl__26;
- __gmpz_init_set_si(__gen_e_acsl__26,0L);
- __gmpz_init_set(__gen_e_acsl_if_18,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__26));
- __gmpz_clear(__gen_e_acsl__26);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_f5_7;
- __e_acsl_mpz_t __gen_e_acsl_n_8;
- __e_acsl_mpz_t __gen_e_acsl_add_12;
- __gen_e_acsl_f5_2(& __gen_e_acsl_f5_7,n + 1L);
- __gmpz_init_set_si(__gen_e_acsl_n_8,(long)n);
- __gmpz_init(__gen_e_acsl_add_12);
- __gmpz_add(__gen_e_acsl_add_12,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_8));
- __gmpz_init_set(__gen_e_acsl_if_18,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_12));
- __gmpz_clear(__gen_e_acsl_f5_7);
- __gmpz_clear(__gen_e_acsl_n_8);
- __gmpz_clear(__gen_e_acsl_add_12);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_18));
- __gmpz_clear(__gen_e_acsl_if_18);
- return;
-}
-
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f5_2(__e_acsl_mpz_t *__retres_arg, long n)
@@ -917,6 +903,40 @@ void __gen_e_acsl_f5_2(__e_acsl_mpz_t *__retres_arg, long n)
return;
}
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from n; */
+void __gen_e_acsl_f5(__e_acsl_mpz_t *__retres_arg, int n)
+{
+ __e_acsl_mpz_t __gen_e_acsl_if_18;
+ if (n >= 0) {
+ __e_acsl_mpz_t __gen_e_acsl__26;
+ __gmpz_init_set_si(__gen_e_acsl__26,0L);
+ __gmpz_init_set(__gen_e_acsl_if_18,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__26));
+ __gmpz_clear(__gen_e_acsl__26);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_f5_7;
+ __e_acsl_mpz_t __gen_e_acsl_n_8;
+ __e_acsl_mpz_t __gen_e_acsl_add_12;
+ __gen_e_acsl_f5_2(& __gen_e_acsl_f5_7,n + 1L);
+ __gmpz_init_set_si(__gen_e_acsl_n_8,(long)n);
+ __gmpz_init(__gen_e_acsl_add_12);
+ __gmpz_add(__gen_e_acsl_add_12,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_8));
+ __gmpz_init_set(__gen_e_acsl_if_18,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_12));
+ __gmpz_clear(__gen_e_acsl_f5_7);
+ __gmpz_clear(__gen_e_acsl_n_8);
+ __gmpz_clear(__gen_e_acsl_add_12);
+ }
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_18));
+ __gmpz_clear(__gen_e_acsl_if_18);
+ return;
+}
+
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from *((__e_acsl_mpz_struct *)n);
*/
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
index 9ac7afd8b8ecfa88cd0ccb3c3d80452fa14c7fc8..3e95b3e2b5551274c74f8492877e680b51c01534 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
@@ -386,7 +386,7 @@ int main(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_9 =
{.values = (void *)0};
__gen_e_acsl_forall_10 = 1;
- __gen_e_acsl_i_2 = (char)0;
+ __gen_e_acsl_i_2 = 0;
while (1) {
if (__gen_e_acsl_i_2 < 10) ; else break;
{
@@ -1121,13 +1121,13 @@ int main(void)
;
{
int __gen_e_acsl_forall_18;
- int __gen_e_acsl_r;
+ unsigned int __gen_e_acsl_r;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_35 =
{.values = (void *)0};
__gen_e_acsl_forall_18 = 1;
__gen_e_acsl_r = 0U;
while (1) {
- if (__gen_e_acsl_r < 1) ; else break;
+ if (__gen_e_acsl_r < 1U) ; else break;
{
int __gen_e_acsl_and_18;
if (1 <= __gen_e_acsl_r + 1) __gen_e_acsl_and_18 = __gen_e_acsl_r + 1 < 2;
diff --git a/src/plugins/e-acsl/tests/bts/issue-framac-1119.c b/src/plugins/e-acsl/tests/bts/issue-framac-1119.c
new file mode 100644
index 0000000000000000000000000000000000000000..44383d02f3f5ecb0659b26266f89941c22d9210f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/issue-framac-1119.c
@@ -0,0 +1,19 @@
+/* run.config
+ COMMENT: cf issue framac#1119
+*/
+
+#include <limits.h>
+#include <stddef.h>
+
+int find_last_of(int const *a, int len, int value) {
+ //@ ghost size_t o = len ;
+ //@ loop invariant \forall integer i ; len <= i < o ==> a[i] != value ;
+ while (len) {
+ len--;
+ }
+ return INT_MAX;
+}
+int main(void) {
+ int a[1] = {1};
+ find_last_of(a, 1, 0);
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
index 3973feccd6cfb68535d6238401f85481ba91983c..73c880a96c69d88ef21b70357a687cf4a8799d7a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -77,18 +77,17 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_store_block((void *)(& __retres),8UL);
{
int __gen_e_acsl_exists;
- unsigned int __gen_e_acsl_i;
+ int __gen_e_acsl_i;
int __gen_e_acsl_forall;
- unsigned int __gen_e_acsl_k;
+ int __gen_e_acsl_k;
__e_acsl_store_block((void *)(& buf),8UL);
__gen_e_acsl_at = buf;
__gen_e_acsl_at_2 = c;
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__gen_e_acsl_exists = 0;
- __gen_e_acsl_i = 0U;
+ __gen_e_acsl_i = 0;
while (1) {
- if (__gen_e_acsl_i < (unsigned int)((int)((unsigned int)n))) ;
- else break;
+ if (__gen_e_acsl_i < (int)((unsigned int)n)) ; else break;
{
int __gen_e_acsl_valid_read;
__e_acsl_assert_data_t __gen_e_acsl_assert_data =
@@ -99,8 +98,8 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
(void *)(& buf));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"buf",
(void *)buf);
- __e_acsl_assert_register_uint(& __gen_e_acsl_assert_data,
- "__gen_e_acsl_i",0,__gen_e_acsl_i);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
+ "__gen_e_acsl_i",0,__gen_e_acsl_i);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,
"sizeof(char)",0,sizeof(char));
__gen_e_acsl_assert_data.blocking = 1;
@@ -124,10 +123,9 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,0UL,
__gen_e_acsl_exists);
__gen_e_acsl_forall = 1;
- __gen_e_acsl_k = 0U;
+ __gen_e_acsl_k = 0;
while (1) {
- if (__gen_e_acsl_k < (unsigned int)((int)((unsigned int)n))) ;
- else break;
+ if (__gen_e_acsl_k < (int)((unsigned int)n)) ; else break;
{
int __gen_e_acsl_valid_read_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
@@ -138,8 +136,8 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
(void *)(& buf));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"buf",
(void *)buf);
- __e_acsl_assert_register_uint(& __gen_e_acsl_assert_data_2,
- "__gen_e_acsl_k",0,__gen_e_acsl_k);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
+ "__gen_e_acsl_k",0,__gen_e_acsl_k);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
"sizeof(char)",0,sizeof(char));
__gen_e_acsl_assert_data_2.blocking = 1;
@@ -175,7 +173,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
__gen_e_acsl_forall_2 = 1;
- __gen_e_acsl_j = 0;
+ __gen_e_acsl_j = 0U;
while (1) {
{
unsigned long __gen_e_acsl_offset;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c
index 653cc715d841d60bba178d65d4d065e6338a0da6..a2747577a2e31d9dcdac29e19aab071900f4bd9c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c
@@ -14,13 +14,13 @@ int main(int argc, char **argv)
__e_acsl_memory_init(& argc,& argv,8UL);
{
int __gen_e_acsl_exists;
- int __gen_e_acsl_x;
+ unsigned int __gen_e_acsl_x;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gen_e_acsl_exists = 0;
__gen_e_acsl_x = (unsigned int)(-1 + 1);
while (1) {
- if (__gen_e_acsl_x < 5) ; else break;
- if (! (__gen_e_acsl_x == 0)) ;
+ if (__gen_e_acsl_x < 5U) ; else break;
+ if (! (__gen_e_acsl_x == 0U)) ;
else {
__gen_e_acsl_exists = 1;
goto e_acsl_end_loop1;
@@ -43,14 +43,14 @@ int main(int argc, char **argv)
/*@ assert \exists unsigned int x; -1 < x < 5 && x == 0; */ ;
{
int __gen_e_acsl_forall;
- int __gen_e_acsl_x_2;
+ unsigned int __gen_e_acsl_x_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
__gen_e_acsl_forall = 1;
__gen_e_acsl_x_2 = (unsigned int)(-1 + 1);
while (1) {
- if (__gen_e_acsl_x_2 < 5) ; else break;
- if (__gen_e_acsl_x_2 != 0) ;
+ if (__gen_e_acsl_x_2 < 5U) ; else break;
+ if (__gen_e_acsl_x_2 != 0U) ;
else {
__gen_e_acsl_forall = 0;
goto e_acsl_end_loop2;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c
index ecb9e3f1e8c4f820254c7696b1173cb4bf5d0988..b1a1f4f23f54b533ae7bebc03525c5ebf687757f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c
@@ -13,10 +13,10 @@ logic integer f(integer n) =
n <= 2147483647 + 1 || n >= 9223372036854775807L + 1? 0: f(n + 1) + n;
*/
-void __gen_e_acsl_f(__e_acsl_mpz_t *__retres_arg, int n);
-
void __gen_e_acsl_f_2(__e_acsl_mpz_t *__retres_arg, long n);
+void __gen_e_acsl_f(__e_acsl_mpz_t *__retres_arg, int n);
+
void __gen_e_acsl_f_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
int main(void)
@@ -79,54 +79,6 @@ int main(void)
return __retres;
}
-/*@ assigns (*__retres_arg)[0];
- assigns (*__retres_arg)[0] \from n; */
-void __gen_e_acsl_f(__e_acsl_mpz_t *__retres_arg, int n)
-{
- int __gen_e_acsl_or;
- __e_acsl_mpz_t __gen_e_acsl_if_3;
- if ((long)n <= 2147483648L) __gen_e_acsl_or = 1;
- else {
- __e_acsl_mpz_t __gen_e_acsl_n;
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_ge;
- __gmpz_init_set_si(__gen_e_acsl_n,(long)n);
- __gmpz_init_set_ui(__gen_e_acsl_,9223372036854775807UL + 1UL);
- __gen_e_acsl_ge = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gen_e_acsl_or = __gen_e_acsl_ge >= 0;
- __gmpz_clear(__gen_e_acsl_n);
- __gmpz_clear(__gen_e_acsl_);
- }
- if (__gen_e_acsl_or) {
- __e_acsl_mpz_t __gen_e_acsl__2;
- __gmpz_init_set_si(__gen_e_acsl__2,0L);
- __gmpz_init_set(__gen_e_acsl_if_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __gmpz_clear(__gen_e_acsl__2);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_f_7;
- __e_acsl_mpz_t __gen_e_acsl_n_4;
- __e_acsl_mpz_t __gen_e_acsl_add_5;
- __gen_e_acsl_f_2(& __gen_e_acsl_f_7,n + 1L);
- __gmpz_init_set_si(__gen_e_acsl_n_4,(long)n);
- __gmpz_init(__gen_e_acsl_add_5);
- __gmpz_add(__gen_e_acsl_add_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4));
- __gmpz_init_set(__gen_e_acsl_if_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
- __gmpz_clear(__gen_e_acsl_f_7);
- __gmpz_clear(__gen_e_acsl_n_4);
- __gmpz_clear(__gen_e_acsl_add_5);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_3));
- __gmpz_clear(__gen_e_acsl_if_3);
- return;
-}
-
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f_2(__e_acsl_mpz_t *__retres_arg, long n)
@@ -189,6 +141,54 @@ void __gen_e_acsl_f_2(__e_acsl_mpz_t *__retres_arg, long n)
return;
}
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from n; */
+void __gen_e_acsl_f(__e_acsl_mpz_t *__retres_arg, int n)
+{
+ int __gen_e_acsl_or;
+ __e_acsl_mpz_t __gen_e_acsl_if_3;
+ if ((long)n <= 2147483648L) __gen_e_acsl_or = 1;
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ int __gen_e_acsl_ge;
+ __gmpz_init_set_si(__gen_e_acsl_n,(long)n);
+ __gmpz_init_set_ui(__gen_e_acsl_,9223372036854775807UL + 1UL);
+ __gen_e_acsl_ge = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gen_e_acsl_or = __gen_e_acsl_ge >= 0;
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_);
+ }
+ if (__gen_e_acsl_or) {
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gmpz_init_set(__gen_e_acsl_if_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_clear(__gen_e_acsl__2);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_f_7;
+ __e_acsl_mpz_t __gen_e_acsl_n_4;
+ __e_acsl_mpz_t __gen_e_acsl_add_5;
+ __gen_e_acsl_f_2(& __gen_e_acsl_f_7,n + 1L);
+ __gmpz_init_set_si(__gen_e_acsl_n_4,(long)n);
+ __gmpz_init(__gen_e_acsl_add_5);
+ __gmpz_add(__gen_e_acsl_add_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4));
+ __gmpz_init_set(__gen_e_acsl_if_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
+ __gmpz_clear(__gen_e_acsl_f_7);
+ __gmpz_clear(__gen_e_acsl_n_4);
+ __gmpz_clear(__gen_e_acsl_add_5);
+ }
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_3));
+ __gmpz_clear(__gen_e_acsl_if_3);
+ return;
+}
+
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from *((__e_acsl_mpz_struct *)n);
*/
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-187.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-187.c
index 72135b496add2b6864b690efab013831e0728431..3dc0c92b8dc55ae7382be288144e3847b05d073f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-187.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-187.c
@@ -49,7 +49,7 @@ int __gen_e_acsl_p(int n)
__gen_e_acsl_i = 0;
while (1) {
if (__gen_e_acsl_i < n) ; else break;
- if (2L * __gen_e_acsl_i < n * (long)__gen_e_acsl_i + 1L) ;
+ if (2 * __gen_e_acsl_i < n * __gen_e_acsl_i + 1) ;
else {
__gen_e_acsl_forall = 0;
goto e_acsl_end_loop1;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-framac-1119.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-framac-1119.c
new file mode 100644
index 0000000000000000000000000000000000000000..35d3af3e2b31799b74a4ee8904ccca0bd672b7f0
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-framac-1119.c
@@ -0,0 +1,208 @@
+/* Generated by Frama-C */
+#include "pthread.h"
+#include "sched.h"
+#include "signal.h"
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+#include "time.h"
+extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+int find_last_of(int const *a, int len, int value)
+{
+ int __retres;
+ __e_acsl_store_block((void *)(& a),8UL);
+ size_t o = (size_t)len;
+ {
+ int __gen_e_acsl_forall;
+ __e_acsl_mpz_t __gen_e_acsl_i;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __gen_e_acsl_forall = 1;
+ __gmpz_init(__gen_e_acsl_i);
+ {
+ __e_acsl_mpz_t __gen_e_acsl_len;
+ __gmpz_init_set_si(__gen_e_acsl_len,(long)len);
+ __gmpz_set(__gen_e_acsl_i,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_len));
+ __gmpz_clear(__gen_e_acsl_len);
+ }
+ while (1) {
+ {
+ __e_acsl_mpz_t __gen_e_acsl_o;
+ int __gen_e_acsl_lt;
+ __gmpz_init_set_ui(__gen_e_acsl_o,o);
+ __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_o));
+ if (__gen_e_acsl_lt < 0) ; else break;
+ __gmpz_clear(__gen_e_acsl_o);
+ }
+ {
+ long __gen_e_acsl_i_2;
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_i_2 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i));
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
+ {.values = (void *)0};
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(a + __gen_e_acsl_i_2),
+ sizeof(int const),
+ (void *)a,
+ (void *)(& a));
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"a",
+ (void *)a);
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_2,
+ "__gen_e_acsl_i_2",0,__gen_e_acsl_i_2);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
+ "sizeof(int const)",0,
+ sizeof(int const));
+ __gen_e_acsl_assert_data_2.blocking = 1;
+ __gen_e_acsl_assert_data_2.kind = "RTE";
+ __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(a + __gen_e_acsl_i_2)";
+ __gen_e_acsl_assert_data_2.file = "issue-framac-1119.c";
+ __gen_e_acsl_assert_data_2.fct = "find_last_of";
+ __gen_e_acsl_assert_data_2.line = 10;
+ __gen_e_acsl_assert_data_2.name = "mem_access";
+ __e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
+ /*@ assert Eva: mem_access: \valid_read(a + __gen_e_acsl_i_2); */
+ if (*(a + __gen_e_acsl_i_2) != value) ;
+ else {
+ __gen_e_acsl_forall = 0;
+ goto e_acsl_end_loop1;
+ }
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __gmpz_init_set_str(__gen_e_acsl_,"1",10);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_i),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_set(__gen_e_acsl_i,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_add);
+ }
+ }
+ e_acsl_end_loop1: ;
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
+ "\\forall integer i; len <= i < o ==> *(a + i) != value",
+ 0,__gen_e_acsl_forall);
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "Invariant";
+ __gen_e_acsl_assert_data.pred_txt = "\\forall integer i; len <= i < o ==> *(a + i) != value";
+ __gen_e_acsl_assert_data.file = "issue-framac-1119.c";
+ __gen_e_acsl_assert_data.fct = "find_last_of";
+ __gen_e_acsl_assert_data.line = 10;
+ __e_acsl_assert(__gen_e_acsl_forall,& __gen_e_acsl_assert_data);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+ __gmpz_clear(__gen_e_acsl_i);
+ }
+ /*@ loop invariant \forall integer i; len <= i < o ==> *(a + i) != value;
+ */
+ while (len) {
+ int __gen_e_acsl_forall_2;
+ __e_acsl_mpz_t __gen_e_acsl_i_3;
+ len --;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
+ {.values = (void *)0};
+ __gen_e_acsl_forall_2 = 1;
+ __gmpz_init(__gen_e_acsl_i_3);
+ {
+ __e_acsl_mpz_t __gen_e_acsl_len_2;
+ __gmpz_init_set_si(__gen_e_acsl_len_2,(long)len);
+ __gmpz_set(__gen_e_acsl_i_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_len_2));
+ __gmpz_clear(__gen_e_acsl_len_2);
+ }
+ while (1) {
+ {
+ __e_acsl_mpz_t __gen_e_acsl_o_2;
+ int __gen_e_acsl_lt_2;
+ __gmpz_init_set_ui(__gen_e_acsl_o_2,o);
+ __gen_e_acsl_lt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_o_2));
+ if (__gen_e_acsl_lt_2 < 0) ; else break;
+ __gmpz_clear(__gen_e_acsl_o_2);
+ }
+ {
+ long __gen_e_acsl_i_4;
+ int __gen_e_acsl_valid_read_2;
+ __gen_e_acsl_i_4 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3));
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
+ {.values = (void *)0};
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(a + __gen_e_acsl_i_4),
+ sizeof(int const),
+ (void *)a,
+ (void *)(& a));
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,"a",
+ (void *)a);
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_4,
+ "__gen_e_acsl_i_4",0,__gen_e_acsl_i_4);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,
+ "sizeof(int const)",0,
+ sizeof(int const));
+ __gen_e_acsl_assert_data_4.blocking = 1;
+ __gen_e_acsl_assert_data_4.kind = "RTE";
+ __gen_e_acsl_assert_data_4.pred_txt = "\\valid_read(a + __gen_e_acsl_i_4)";
+ __gen_e_acsl_assert_data_4.file = "issue-framac-1119.c";
+ __gen_e_acsl_assert_data_4.fct = "find_last_of";
+ __gen_e_acsl_assert_data_4.line = 10;
+ __gen_e_acsl_assert_data_4.name = "mem_access";
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,
+ & __gen_e_acsl_assert_data_4);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
+ /*@ assert Eva: mem_access: \valid_read(a + __gen_e_acsl_i_4); */
+ if (*(a + __gen_e_acsl_i_4) != value) ;
+ else {
+ __gen_e_acsl_forall_2 = 0;
+ goto e_acsl_end_loop2;
+ }
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __gmpz_init_set_str(__gen_e_acsl__2,"1",10);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_set(__gen_e_acsl_i_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ }
+ }
+ e_acsl_end_loop2: ;
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
+ "\\forall integer i; len <= i < o ==> *(a + i) != value",
+ 0,__gen_e_acsl_forall_2);
+ __gen_e_acsl_assert_data_3.blocking = 1;
+ __gen_e_acsl_assert_data_3.kind = "Invariant";
+ __gen_e_acsl_assert_data_3.pred_txt = "\\forall integer i; len <= i < o ==> *(a + i) != value";
+ __gen_e_acsl_assert_data_3.file = "issue-framac-1119.c";
+ __gen_e_acsl_assert_data_3.fct = "find_last_of";
+ __gen_e_acsl_assert_data_3.line = 10;
+ __e_acsl_assert(__gen_e_acsl_forall_2,& __gen_e_acsl_assert_data_3);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
+ __gmpz_clear(__gen_e_acsl_i_3);
+ }
+ __retres = 2147483647;
+ __e_acsl_delete_block((void *)(& a));
+ return __retres;
+}
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ int a[1] = {1};
+ __e_acsl_store_block((void *)(a),4UL);
+ __e_acsl_full_init((void *)(& a));
+ find_last_of((int const *)(a),1,0);
+ __retres = 0;
+ __e_acsl_delete_block((void *)(a));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
index 00ad900d9e595db233712cad254e9308f4ad2bef..d91b15ef3db86e0965741288cdc16217fc904080 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
@@ -17,7 +17,7 @@ int main(void)
int __gen_e_acsl_c;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gen_e_acsl_forall = 1;
- __gen_e_acsl_c = (unsigned char)4;
+ __gen_e_acsl_c = 4;
while (1) {
if (__gen_e_acsl_c < 256) ; else break;
{
@@ -59,7 +59,7 @@ int main(void)
__gen_e_acsl_forall_2 = 1;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
- __gen_e_acsl_u = (char)(1 + 1);
+ __gen_e_acsl_u = 1 + 1;
while (1) {
{
int __gen_e_acsl_and_2;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-framac-1119.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-framac-1119.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..07a2f42bf48fe04064bda92c5fd5d3e4a181859f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-framac-1119.res.oracle
@@ -0,0 +1,14 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] :0: Warning:
+ function __e_acsl_assert_register_long: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] issue-framac-1119.c:10: Warning:
+ function __e_acsl_assert_register_ulong: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] issue-framac-1119.c:10: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] issue-framac-1119.c:10: Warning:
+ out of bounds read. assert \valid_read(a + __gen_e_acsl_i_2);
+[eva:alarm] issue-framac-1119.c:10: Warning:
+ out of bounds read. assert \valid_read(a + __gen_e_acsl_i_4);
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-framac-1119.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-framac-1119.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_printed_data.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_printed_data.c
index be87f4316d4767a77bc52abcaccebb591f960b44..4204fcd3ed9ba4bacc3a12bcddb6007ff628a85e 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_printed_data.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_printed_data.c
@@ -109,7 +109,7 @@ int main(void)
__e_acsl_store_block((void *)(& int_bool),1UL);
__e_acsl_full_init((void *)(& int_bool));
{
- int __gen_e_acsl_x;
+ _Bool __gen_e_acsl_x;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gen_e_acsl_x = int_bool;
__e_acsl_assert_register_bool(& __gen_e_acsl_assert_data,"int_bool",0,
@@ -128,7 +128,7 @@ int main(void)
__e_acsl_store_block((void *)(& int_char),1UL);
__e_acsl_full_init((void *)(& int_char));
{
- int __gen_e_acsl_x_2;
+ char __gen_e_acsl_x_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
__gen_e_acsl_x_2 = int_char;
@@ -148,7 +148,7 @@ int main(void)
__e_acsl_store_block((void *)(& int_schar),1UL);
__e_acsl_full_init((void *)(& int_schar));
{
- int __gen_e_acsl_x_3;
+ signed char __gen_e_acsl_x_3;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
__gen_e_acsl_x_3 = int_schar;
@@ -168,7 +168,7 @@ int main(void)
__e_acsl_store_block((void *)(& int_uchar),1UL);
__e_acsl_full_init((void *)(& int_uchar));
{
- int __gen_e_acsl_x_4;
+ unsigned char __gen_e_acsl_x_4;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
__gen_e_acsl_x_4 = int_uchar;
@@ -228,7 +228,7 @@ int main(void)
__e_acsl_store_block((void *)(& int_short),2UL);
__e_acsl_full_init((void *)(& int_short));
{
- int __gen_e_acsl_x_7;
+ short __gen_e_acsl_x_7;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
__gen_e_acsl_x_7 = int_short;
@@ -248,7 +248,7 @@ int main(void)
__e_acsl_store_block((void *)(& int_ushort),2UL);
__e_acsl_full_init((void *)(& int_ushort));
{
- int __gen_e_acsl_x_8;
+ unsigned short __gen_e_acsl_x_8;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_8 =
{.values = (void *)0};
__gen_e_acsl_x_8 = int_ushort;
@@ -308,7 +308,7 @@ int main(void)
__e_acsl_store_block((void *)(& int_llong),8UL);
__e_acsl_full_init((void *)(& int_llong));
{
- long __gen_e_acsl_x_11;
+ long long __gen_e_acsl_x_11;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_11 =
{.values = (void *)0};
__gen_e_acsl_x_11 = int_llong;
@@ -328,7 +328,7 @@ int main(void)
__e_acsl_store_block((void *)(& int_ullong),8UL);
__e_acsl_full_init((void *)(& int_ullong));
{
- unsigned long __gen_e_acsl_x_12;
+ unsigned long long __gen_e_acsl_x_12;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_12 =
{.values = (void *)0};
__gen_e_acsl_x_12 = int_ullong;
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/functions.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle/functions.res.oracle
index 50ab698f34137e2d3fc68063d9b09415c60c8953..7b7c602e07492d03d1fe06d0850a36d4d077515f 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle/functions.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/functions.res.oracle
@@ -44,16 +44,16 @@
[eva:alarm] functions.c:56: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] functions.c:59: Warning:
- function __e_acsl_assert_register_int: precondition data->values == \null ||
- \valid(data->values) got status unknown.
+ function __e_acsl_assert_register_char: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
[eva:alarm] functions.c:59: Warning:
function __e_acsl_assert_register_char: precondition data->values == \null ||
\valid(data->values) got status unknown.
[eva:alarm] functions.c:59: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] functions.c:61: Warning:
- function __e_acsl_assert_register_int: precondition data->values == \null ||
- \valid(data->values) got status unknown.
+ function __e_acsl_assert_register_short: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
[eva:alarm] functions.c:61: Warning:
function __e_acsl_assert_register_short: precondition data->values == \null ||
\valid(data->values) got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
index 8f452ad172b58a7fb0f229306e351c8a10287f59..11e868ecff42b57483b231fea8c40d5782b95b31 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
@@ -24,24 +24,29 @@ int __gen_e_acsl_p2(int x, int y);
int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y);
+int __gen_e_acsl_p2_5(int x, __e_acsl_mpz_struct * y);
+
/*@ logic integer f1(integer x, integer y) = x + y;
*/
-void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y);
+void __gen_e_acsl_f1_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
+ __e_acsl_mpz_struct * y);
-void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
+void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
__e_acsl_mpz_struct * y);
void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
__e_acsl_mpz_struct * y);
+void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y);
+
/*@ logic char h_char(char c) = c;
*/
-int __gen_e_acsl_h_char(int c);
+char __gen_e_acsl_h_char(char c);
/*@ logic short h_short(short s) = s;
*/
-int __gen_e_acsl_h_short(int s);
+short __gen_e_acsl_h_short(short s);
/*@ logic int g_hidden(int x) = x;
*/
@@ -175,16 +180,22 @@ int main(void)
}
/*@ assert f1(x, y) == 3; */ ;
{
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl__7;
__e_acsl_mpz_t __gen_e_acsl_f1_4;
int __gen_e_acsl_p2_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
- __gen_e_acsl_f1(& __gen_e_acsl_f1_4,3,4);
+ __gmpz_init_set_str(__gen_e_acsl__6,"4",10);
+ __gmpz_init_set_str(__gen_e_acsl__7,"3",10);
+ __gen_e_acsl_f1_3(& __gen_e_acsl_f1_4,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__7,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__6);
/*@ assert
Eva: initialization:
\initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_4);
*/
- __gen_e_acsl_p2_6 = __gen_e_acsl_p2_3(x,
+ __gen_e_acsl_p2_6 = __gen_e_acsl_p2_5(x,
(__e_acsl_mpz_struct *)__gen_e_acsl_f1_4);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_5,"f1(3, 4)",0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_4));
@@ -199,22 +210,27 @@ int main(void)
__gen_e_acsl_assert_data_5.line = 49;
__e_acsl_assert(__gen_e_acsl_p2_6,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl__7);
__gmpz_clear(__gen_e_acsl_f1_4);
}
/*@ assert p2(x, f1(3, 4)); */ ;
{
- __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ __e_acsl_mpz_t __gen_e_acsl__10;
__e_acsl_mpz_t __gen_e_acsl_f1_6;
- __e_acsl_mpz_t __gen_e_acsl__7;
- int __gen_e_acsl_gt_4;
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ int __gen_e_acsl_gt_5;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
- __gmpz_init_set_str(__gen_e_acsl__6,"99999999999999999999999999999",10);
- __gen_e_acsl_f1_5(& __gen_e_acsl_f1_6,9,
- (__e_acsl_mpz_struct *)__gen_e_acsl__6);
- __gmpz_init_set_si(__gen_e_acsl__7,0L);
- __gen_e_acsl_gt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __gmpz_init_set_str(__gen_e_acsl__9,"99999999999999999999999999999",10);
+ __gmpz_init_set_str(__gen_e_acsl__10,"9",10);
+ __gen_e_acsl_f1_5(& __gen_e_acsl_f1_6,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__10,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__9);
+ __gmpz_init_set_si(__gen_e_acsl__11,0L);
+ __gen_e_acsl_gt_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,
"f1(9, 99999999999999999999999999999)",0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6));
@@ -224,27 +240,28 @@ int main(void)
__gen_e_acsl_assert_data_6.file = "functions.c";
__gen_e_acsl_assert_data_6.fct = "main";
__gen_e_acsl_assert_data_6.line = 50;
- __e_acsl_assert(__gen_e_acsl_gt_4 > 0,& __gen_e_acsl_assert_data_6);
+ __e_acsl_assert(__gen_e_acsl_gt_5 > 0,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
- __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl__10);
__gmpz_clear(__gen_e_acsl_f1_6);
- __gmpz_clear(__gen_e_acsl__7);
+ __gmpz_clear(__gen_e_acsl__11);
}
/*@ assert f1(9, 99999999999999999999999999999) > 0; */ ;
{
- __e_acsl_mpz_t __gen_e_acsl__8;
+ __e_acsl_mpz_t __gen_e_acsl__12;
__e_acsl_mpz_t __gen_e_acsl_f1_8;
- __e_acsl_mpz_t __gen_e_acsl__9;
+ __e_acsl_mpz_t __gen_e_acsl__13;
int __gen_e_acsl_eq_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
- __gmpz_init_set_str(__gen_e_acsl__8,"99999999999999999999999999999",10);
+ __gmpz_init_set_str(__gen_e_acsl__12,"99999999999999999999999999999",10);
__gen_e_acsl_f1_7(& __gen_e_acsl_f1_8,
- (__e_acsl_mpz_struct *)__gen_e_acsl__8,
- (__e_acsl_mpz_struct *)__gen_e_acsl__8);
- __gmpz_init_set_str(__gen_e_acsl__9,"199999999999999999999999999998",10);
+ (__e_acsl_mpz_struct *)__gen_e_acsl__12,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__12);
+ __gmpz_init_set_str(__gen_e_acsl__13,"199999999999999999999999999998",10);
__gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_8),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_7,
"f1(99999999999999999999999999999, 99999999999999999999999999999)",
0,
@@ -257,9 +274,9 @@ int main(void)
__gen_e_acsl_assert_data_7.line = 51;
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
- __gmpz_clear(__gen_e_acsl__8);
+ __gmpz_clear(__gen_e_acsl__12);
__gmpz_clear(__gen_e_acsl_f1_8);
- __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl__13);
}
/*@
assert
@@ -296,20 +313,20 @@ int main(void)
/*@ assert g(x) == x; */ ;
char c = (char)'c';
{
- int __gen_e_acsl_h_char_2;
+ char __gen_e_acsl_h_char_2;
__e_acsl_mpz_t __gen_e_acsl_app_2;
__e_acsl_mpz_t __gen_e_acsl_c;
int __gen_e_acsl_eq_4;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_9 =
{.values = (void *)0};
- __gen_e_acsl_h_char_2 = __gen_e_acsl_h_char((int)c);
+ __gen_e_acsl_h_char_2 = __gen_e_acsl_h_char(c);
__gmpz_init_set_si(__gen_e_acsl_app_2,(long)__gen_e_acsl_h_char_2);
__gmpz_init_set_si(__gen_e_acsl_c,(long)c);
__gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_app_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_c));
__e_acsl_assert_register_char(& __gen_e_acsl_assert_data_9,"c",0,c);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_9,"h_char(c)",0,
- __gen_e_acsl_h_char_2);
+ __e_acsl_assert_register_char(& __gen_e_acsl_assert_data_9,"h_char(c)",0,
+ __gen_e_acsl_h_char_2);
__e_acsl_assert_register_char(& __gen_e_acsl_assert_data_9,"c",0,c);
__gen_e_acsl_assert_data_9.blocking = 1;
__gen_e_acsl_assert_data_9.kind = "Assertion";
@@ -325,20 +342,20 @@ int main(void)
/*@ assert h_char(c) == c; */ ;
short s = (short)1;
{
- int __gen_e_acsl_h_short_2;
+ short __gen_e_acsl_h_short_2;
__e_acsl_mpz_t __gen_e_acsl_app_3;
__e_acsl_mpz_t __gen_e_acsl_s;
int __gen_e_acsl_eq_5;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_10 =
{.values = (void *)0};
- __gen_e_acsl_h_short_2 = __gen_e_acsl_h_short((int)s);
+ __gen_e_acsl_h_short_2 = __gen_e_acsl_h_short(s);
__gmpz_init_set_si(__gen_e_acsl_app_3,(long)__gen_e_acsl_h_short_2);
__gmpz_init_set_si(__gen_e_acsl_s,(long)s);
__gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_app_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_s));
__e_acsl_assert_register_short(& __gen_e_acsl_assert_data_10,"s",0,s);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_10,"h_short(s)",
- 0,__gen_e_acsl_h_short_2);
+ __e_acsl_assert_register_short(& __gen_e_acsl_assert_data_10,
+ "h_short(s)",0,__gen_e_acsl_h_short_2);
__e_acsl_assert_register_short(& __gen_e_acsl_assert_data_10,"s",0,s);
__gen_e_acsl_assert_data_10.blocking = 1;
__gen_e_acsl_assert_data_10.kind = "Assertion";
@@ -357,15 +374,15 @@ int main(void)
{
mystruct __gen_e_acsl_t1_2;
__e_acsl_mpz_t __gen_e_acsl_t2_2;
- __e_acsl_mpz_t __gen_e_acsl__12;
+ __e_acsl_mpz_t __gen_e_acsl__16;
int __gen_e_acsl_eq_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_11 =
{.values = (void *)0};
__gen_e_acsl_t1_2 = __gen_e_acsl_t1(m);
__gen_e_acsl_t2(& __gen_e_acsl_t2_2,__gen_e_acsl_t1_2);
- __gmpz_init_set_si(__gen_e_acsl__12,17L);
+ __gmpz_init_set_si(__gen_e_acsl__16,17L);
__gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_t2_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
__e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_11,"m");
__e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_11,"t1(m)");
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_11,"t2(t1(m))",0,
@@ -379,25 +396,25 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_eq_6 == 0,& __gen_e_acsl_assert_data_11);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_11);
__gmpz_clear(__gen_e_acsl_t2_2);
- __gmpz_clear(__gen_e_acsl__12);
+ __gmpz_clear(__gen_e_acsl__16);
}
/*@ assert t2(t1(m)) == 17; */ ;
__gen_e_acsl_k(9);
double d = 2.0;
{
double __gen_e_acsl_f2_2;
- __e_acsl_mpq_t __gen_e_acsl__15;
- __e_acsl_mpq_t __gen_e_acsl__16;
- int __gen_e_acsl_gt_5;
+ __e_acsl_mpq_t __gen_e_acsl__19;
+ __e_acsl_mpq_t __gen_e_acsl__20;
+ int __gen_e_acsl_gt_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_12 =
{.values = (void *)0};
__gen_e_acsl_f2_2 = __gen_e_acsl_f2(d);
- __gmpq_init(__gen_e_acsl__15);
- __gmpq_set_str(__gen_e_acsl__15,"0",10);
- __gmpq_init(__gen_e_acsl__16);
- __gmpq_set_d(__gen_e_acsl__16,__gen_e_acsl_f2_2);
- __gen_e_acsl_gt_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__16),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__15));
+ __gmpq_init(__gen_e_acsl__19);
+ __gmpq_set_str(__gen_e_acsl__19,"0",10);
+ __gmpq_init(__gen_e_acsl__20);
+ __gmpq_set_d(__gen_e_acsl__20,__gen_e_acsl_f2_2);
+ __gen_e_acsl_gt_6 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__20),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__19));
__e_acsl_assert_register_double(& __gen_e_acsl_assert_data_12,"d",d);
__e_acsl_assert_register_double(& __gen_e_acsl_assert_data_12,"f2(d)",
__gen_e_acsl_f2_2);
@@ -407,10 +424,10 @@ int main(void)
__gen_e_acsl_assert_data_12.file = "functions.c";
__gen_e_acsl_assert_data_12.fct = "main";
__gen_e_acsl_assert_data_12.line = 71;
- __e_acsl_assert(__gen_e_acsl_gt_5 > 0,& __gen_e_acsl_assert_data_12);
+ __e_acsl_assert(__gen_e_acsl_gt_6 > 0,& __gen_e_acsl_assert_data_12);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_12);
- __gmpq_clear(__gen_e_acsl__15);
- __gmpq_clear(__gen_e_acsl__16);
+ __gmpq_clear(__gen_e_acsl__19);
+ __gmpq_clear(__gen_e_acsl__20);
}
/*@ assert f2(d) > 0; */ ;
__retres = 0;
@@ -515,47 +532,63 @@ int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
return __retres;
}
-/*@ assigns (*__retres_arg)[0];
- assigns (*__retres_arg)[0] \from x, y; */
-void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
+/*@ assigns \result;
+ assigns \result \from x, *((__e_acsl_mpz_struct *)y); */
+int __gen_e_acsl_p2_5(int x, __e_acsl_mpz_struct * y)
{
- __e_acsl_mpz_t __gen_e_acsl_x_4;
- __e_acsl_mpz_t __gen_e_acsl_y_3;
- __e_acsl_mpz_t __gen_e_acsl_add_4;
- __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
- __gmpz_init(__gen_e_acsl_add_4);
- __gmpz_add(__gen_e_acsl_add_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3));
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
- __gmpz_clear(__gen_e_acsl_x_4);
- __gmpz_clear(__gen_e_acsl_y_3);
- __gmpz_clear(__gen_e_acsl_add_4);
- return;
+ __e_acsl_mpz_t __gen_e_acsl_x_5;
+ __e_acsl_mpz_t __gen_e_acsl_add_6;
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ int __gen_e_acsl_gt_4;
+ __gmpz_init_set_si(__gen_e_acsl_x_5,(long)x);
+ __gmpz_init(__gen_e_acsl_add_6);
+ __gmpz_add(__gen_e_acsl_add_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
+ (__e_acsl_mpz_struct const *)(y));
+ __gmpz_init_set_si(__gen_e_acsl__8,0L);
+ __gen_e_acsl_gt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ int __retres = __gen_e_acsl_gt_4 > 0;
+ __gmpz_clear(__gen_e_acsl_x_5);
+ __gmpz_clear(__gen_e_acsl_add_6);
+ __gmpz_clear(__gen_e_acsl__8);
+ return __retres;
}
/*@ assigns (*__retres_arg)[0];
- assigns (*__retres_arg)[0] \from x, *((__e_acsl_mpz_struct *)y);
+ assigns (*__retres_arg)[0]
+ \from *((__e_acsl_mpz_struct *)x), *((__e_acsl_mpz_struct *)y);
*/
-void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
+void __gen_e_acsl_f1_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
__e_acsl_mpz_struct * y)
{
- __e_acsl_mpz_t __gen_e_acsl_x_5;
__e_acsl_mpz_t __gen_e_acsl_add_5;
- __gmpz_init_set_si(__gen_e_acsl_x_5,(long)x);
__gmpz_init(__gen_e_acsl_add_5);
- __gmpz_add(__gen_e_acsl_add_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
+ __gmpz_add(__gen_e_acsl_add_5,(__e_acsl_mpz_struct const *)(x),
(__e_acsl_mpz_struct const *)(y));
__gmpz_init_set(*__retres_arg,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
- __gmpz_clear(__gen_e_acsl_x_5);
__gmpz_clear(__gen_e_acsl_add_5);
return;
}
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0]
+ \from *((__e_acsl_mpz_struct *)x), *((__e_acsl_mpz_struct *)y);
+ */
+void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
+ __e_acsl_mpz_struct * y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_add_7;
+ __gmpz_init(__gen_e_acsl_add_7);
+ __gmpz_add(__gen_e_acsl_add_7,(__e_acsl_mpz_struct const *)(x),
+ (__e_acsl_mpz_struct const *)(y));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
+ __gmpz_clear(__gen_e_acsl_add_7);
+ return;
+}
+
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0]
\from *((__e_acsl_mpz_struct *)x), *((__e_acsl_mpz_struct *)y);
@@ -563,26 +596,47 @@ void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
__e_acsl_mpz_struct * y)
{
- __e_acsl_mpz_t __gen_e_acsl_add_6;
- __gmpz_init(__gen_e_acsl_add_6);
- __gmpz_add(__gen_e_acsl_add_6,(__e_acsl_mpz_struct const *)(x),
+ __e_acsl_mpz_t __gen_e_acsl_add_8;
+ __gmpz_init(__gen_e_acsl_add_8);
+ __gmpz_add(__gen_e_acsl_add_8,(__e_acsl_mpz_struct const *)(x),
(__e_acsl_mpz_struct const *)(y));
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
- __gmpz_clear(__gen_e_acsl_add_6);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_8));
+ __gmpz_clear(__gen_e_acsl_add_8);
+ return;
+}
+
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from x, y; */
+void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_4;
+ __e_acsl_mpz_t __gen_e_acsl_y_3;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
+ __gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+ __gmpz_clear(__gen_e_acsl_x_4);
+ __gmpz_clear(__gen_e_acsl_y_3);
+ __gmpz_clear(__gen_e_acsl_add_4);
return;
}
/*@ assigns \result;
assigns \result \from c; */
-int __gen_e_acsl_h_char(int c)
+char __gen_e_acsl_h_char(char c)
{
return c;
}
/*@ assigns \result;
assigns \result \from s; */
-int __gen_e_acsl_h_short(int s)
+short __gen_e_acsl_h_short(short s)
{
return s;
}
@@ -614,20 +668,20 @@ mystruct __gen_e_acsl_t1(mystruct m)
assigns (*__retres_arg)[0] \from m; */
void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m)
{
- __e_acsl_mpz_t __gen_e_acsl__10;
- __e_acsl_mpz_t __gen_e_acsl__11;
- __e_acsl_mpz_t __gen_e_acsl_add_7;
- __gmpz_init_set_si(__gen_e_acsl__10,(long)m.k);
- __gmpz_init_set_si(__gen_e_acsl__11,(long)m.l);
- __gmpz_init(__gen_e_acsl_add_7);
- __gmpz_add(__gen_e_acsl_add_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ __e_acsl_mpz_t __gen_e_acsl__14;
+ __e_acsl_mpz_t __gen_e_acsl__15;
+ __e_acsl_mpz_t __gen_e_acsl_add_9;
+ __gmpz_init_set_si(__gen_e_acsl__14,(long)m.k);
+ __gmpz_init_set_si(__gen_e_acsl__15,(long)m.l);
+ __gmpz_init(__gen_e_acsl_add_9);
+ __gmpz_add(__gen_e_acsl_add_9,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__14),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
- __gmpz_clear(__gen_e_acsl__10);
- __gmpz_clear(__gen_e_acsl__11);
- __gmpz_clear(__gen_e_acsl_add_7);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_9));
+ __gmpz_clear(__gen_e_acsl__14);
+ __gmpz_clear(__gen_e_acsl__15);
+ __gmpz_clear(__gen_e_acsl_add_9);
return;
}
@@ -652,21 +706,21 @@ int __gen_e_acsl_k_pred(int x)
assigns \result \from x; */
double __gen_e_acsl_f2(double x)
{
- __e_acsl_mpq_t __gen_e_acsl__13;
- __e_acsl_mpq_t __gen_e_acsl__14;
+ __e_acsl_mpq_t __gen_e_acsl__17;
+ __e_acsl_mpq_t __gen_e_acsl__18;
__e_acsl_mpq_t __gen_e_acsl_div;
double __gen_e_acsl_cast;
- __gmpq_init(__gen_e_acsl__13);
- __gmpq_set_str(__gen_e_acsl__13,"1",10);
- __gmpq_init(__gen_e_acsl__14);
- __gmpq_set_d(__gen_e_acsl__14,x);
+ __gmpq_init(__gen_e_acsl__17);
+ __gmpq_set_str(__gen_e_acsl__17,"1",10);
+ __gmpq_init(__gen_e_acsl__18);
+ __gmpq_set_d(__gen_e_acsl__18,x);
__gmpq_init(__gen_e_acsl_div);
__gmpq_div(__gen_e_acsl_div,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__13),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__14));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__17),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__18));
__gen_e_acsl_cast = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
- __gmpq_clear(__gen_e_acsl__13);
- __gmpq_clear(__gen_e_acsl__14);
+ __gmpq_clear(__gen_e_acsl__17);
+ __gmpq_clear(__gen_e_acsl__18);
__gmpq_clear(__gen_e_acsl_div);
/*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast); */
return __gen_e_acsl_cast;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
index 608476b0834378db467b2c0b70f0b858ccc7d2dd..7244509fa59a1d36e166341d9f8c317efc1f5c3e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
@@ -30,7 +30,7 @@ int __gen_e_acsl_main(int argc, char **argv)
__e_acsl_store_block((void *)(& argv),8UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gen_e_acsl_forall = 1;
- __gen_e_acsl_k = 0;
+ __gen_e_acsl_k = 0L;
while (1) {
if (__gen_e_acsl_k <= (long)argc) ; else break;
{
@@ -270,7 +270,7 @@ int __gen_e_acsl_main(int argc, char **argv)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_9 =
{.values = (void *)0};
__gen_e_acsl_forall_2 = 1;
- __gen_e_acsl_k_2 = 0;
+ __gen_e_acsl_k_2 = 0L;
while (1) {
if (__gen_e_acsl_k_2 <= (long)len) ; else break;
{