diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 47b5ee44e5d8e5511c0be5206f368905810323c8..fc9b5349f30bd57b7b4b40dc4845a32b7051612b 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -73,7 +73,6 @@ PLUGIN_CMO:= local_config \
env \
keep_status \
dup_functions \
- interval_system \
interval \
typing \
loops \
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 52b9b519800f3bb9e17354da585870dd10b3c948..d1e50bebe74c088da2b7f6050b02021d859661b0 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -27,8 +27,6 @@ gmpz.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
gmpz.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
interval.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
interval.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-interval_system.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-interval_system.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
keep_status.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
keep_status.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
label.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 432338f3c3bc41204bcc8d6a90605687b2972fab..a889332eac3a820642740ee1777f898b7eac2118 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -29,9 +29,7 @@ open Cil_types
(* Basic datatypes and operations *)
(* ********************************************************************* *)
-exception Not_an_integer = Interval_system.Not_an_integer
-let interv_of_typ = Interval_system.interv_of_typ
-let ikind_of_interv = Interval_system.ikind_of_interv
+exception Not_an_integer
(* constructors *)
@@ -45,8 +43,35 @@ let interv_of_unknown_block =
(Some Integer.zero)
(Some (Bit_utils.max_byte_address ())))
-(* imperative environments *)
-module Env: sig
+let rec interv_of_typ ty = match Cil.unrollType ty with
+ | TInt (k,_) as ty ->
+ let n = Cil.bitsSizeOf ty in
+ let l, u =
+ if Cil.isSigned k then Cil.min_signed_number n, Cil.max_signed_number n
+ else Integer.zero, Cil.max_unsigned_number n
+ in
+ Ival.inject_range (Some l) (Some u)
+ | TEnum(enuminfo, _) -> interv_of_typ (TInt (enuminfo.ekind, []))
+ | _ ->
+ raise Not_an_integer
+
+let ikind_of_interv i =
+ if Ival.is_bottom i then IInt
+ else match Ival.min_and_max i with
+ | Some l, Some u ->
+ let is_pos = Integer.ge l Integer.zero in
+ let lkind = Cil.intKindForValue l is_pos in
+ let ukind = Cil.intKindForValue u is_pos in
+ (* kind corresponding to the interval *)
+ let kind = if Cil.intTypeIncluded lkind ukind then ukind else lkind in
+ (* convert the kind to [IInt] whenever smaller. *)
+ if Cil.intTypeIncluded kind IInt then IInt else kind
+ | None, None -> raise Cil.Not_representable (* GMP *)
+ | None, Some _ | Some _, None ->
+ Kernel.fatal ~current:true "ival: %a" Ival.pretty i
+
+(* Imperative environments *)
+module rec Env: sig
val clear: unit -> unit
val add: Cil_types.logic_var -> Ival.t -> unit
val find: Cil_types.logic_var -> Ival.t
@@ -55,11 +80,85 @@ module Env: sig
end = struct
open Cil_datatype
let tbl: Ival.t Logic_var.Hashtbl.t = Logic_var.Hashtbl.create 7
- let clear () = Logic_var.Hashtbl.clear tbl
+
let add = Logic_var.Hashtbl.add tbl
let remove = Logic_var.Hashtbl.remove tbl
let replace = Logic_var.Hashtbl.replace tbl
let find = Logic_var.Hashtbl.find tbl
+
+ let clear () =
+ Logic_var.Hashtbl.clear tbl;
+ Logic_function_env.clear ()
+
+end
+
+(* Environment for handling recursive logic functions *)
+and Logic_function_env: sig
+ val widen: infer:(term -> Ival.t) -> term -> Ival.t -> bool * Ival.t
+ val clear: unit -> unit
+end = struct
+
+ module Profile =
+ Datatype.List_with_collections
+ (Ival)
+ (struct
+ let module_name = "E_ACSL.Interval.Logic_function_env.Profile"
+ end)
+
+ module LF =
+ Datatype.Pair_with_collections
+ (Datatype.String)
+ (Profile)
+ (struct
+ let module_name = "E_ACSL.Interval.Logic_function_env.LF"
+ end)
+
+ let tbl = LF.Hashtbl.create 7
+
+ let clear () = LF.Hashtbl.clear tbl
+
+ let interv_of_typ_containing_interv i =
+ try
+ let kind = ikind_of_interv i in
+ interv_of_typ (TInt(kind, []))
+ with Cil.Not_representable ->
+ (* infinity *)
+ Ival.inject_range None None
+
+ let extract_profile ~infer t = match t.term_node with
+ | Tapp(li, _, args) ->
+ li.l_var_info.lv_name,
+ List.map2
+ (fun param arg ->
+ try
+ let i = infer arg in
+ (* over-approximation of the interval to reach the fixpoint
+ faster, and to generate fewer specialized functions *)
+ let larger_i = interv_of_typ_containing_interv i in
+ Env.add param larger_i;
+ larger_i
+ with Not_an_integer ->
+ (* no need to add [param] to the environment *)
+ Ival.bottom)
+ li.l_profile
+ args
+ | _ ->
+ assert false
+
+ let widen ~infer t i =
+ let p = extract_profile ~infer t in
+ try
+ let old_i = LF.Hashtbl.find tbl p in
+ if Ival.is_included i old_i then true, old_i
+ else begin
+ let j = Ival.join i old_i in
+ LF.Hashtbl.replace tbl p j;
+ false, j
+ end
+ with Not_found ->
+ LF.Hashtbl.add tbl p i;
+ false, i
+
end
(* ********************************************************************* *)
@@ -179,43 +278,28 @@ let rec infer t =
let i2 = infer t2 in
Ival.meet i1 i2
- | Tapp (li, _, args) ->
- (match li.l_type with
- | None -> assert false (* [None] only possible for predicates *)
- | Some Linteger ->
- begin match li.l_body with
- | LBpred _ ->
- Ival.zero_or_one
- | LBterm t' ->
- (* TODO: should not be necessary to distinguish the recursive case.
- Stack overflow if not distingued *)
- if Interval_system.is_recursive li then
- Interval_system.build_and_solve ~infer t
- else begin (* non-recursive case *)
- (* add the arguments to the context *)
- List.iter2
- (fun lv arg ->
- try
- let i = infer arg in
- Env.add lv i
- with Not_an_integer ->
- ())
- li.l_profile
- args;
- let i = infer t' in
- (* remove arguments from the context *)
- List.iter (fun lv -> Env.remove lv) li.l_profile;
- i
- end
- | LBnone ->
- Error.not_yet "logic functions with no definition nor reads clause"
- | LBreads _ ->
- Error.not_yet "logic functions performing read accesses"
- | LBinductive _ ->
- Error.not_yet "logic functions inductively defined"
- end
- | Some (Ctype ty) -> interv_of_typ ty
- | Some _ -> raise Not_an_integer)
+ | Tapp (li, _, _args) ->
+ (match li.l_body with
+ | LBpred _ ->
+ Ival.zero_or_one
+ | LBterm t' ->
+ let rec fixpoint i =
+ let is_included, new_i = Logic_function_env.widen ~infer t i 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 Ival.bottom
+ | LBnone ->
+ Error.not_yet "logic functions with no definition nor reads clause"
+ | LBreads _ ->
+ Error.not_yet "logic functions performing read accesses"
+ | 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"
diff --git a/src/plugins/e-acsl/interval_system.ml b/src/plugins/e-acsl/interval_system.ml
deleted file mode 100644
index 71dd4dbea7d4294a8d203044452e0e15b23dcd2d..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/interval_system.ml
+++ /dev/null
@@ -1,344 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of the Frama-C's E-ACSL plug-in. *)
-(* *)
-(* Copyright (C) 2012-2018 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-
-(**************************************************************************)
-(******************************* Types ************************************)
-(**************************************************************************)
-
-type ival_binop = Ival_add | Ival_min | Ival_mul | Ival_div | Ival_join
-
-type ivar =
- (* it would be possible to get more precise results by storing an ival for
- each argument instead of a logic type, but the system would converge too
- slowly to a solution. *)
- { iv_name: string; iv_types: logic_type list }
-
-type ival_exp =
- | Iconst of Ival.t
- | Ivar of ivar
- | Ibinop of ival_binop * ival_exp * ival_exp
- | Iunsupported
-
-module LT_List =
- Datatype.List_with_collections
- (Cil_datatype.Logic_type)
- (struct let module_name = "E_ACSL.Interval_system.LT_List" end)
-
-module Ivar =
- Datatype.Make_with_collections(struct
- type t = ivar
- let name = "E_ACSL.Interval_system.Ivar"
- let reprs = [ { iv_name = "a"; iv_types = Cil_datatype.Logic_type.reprs } ]
- include Datatype.Undefined
- let compare iv1 iv2 =
- let n = Datatype.String.compare iv1.iv_name iv2.iv_name in
- if n = 0 then LT_List.compare iv1.iv_types iv2.iv_types
- else n
- let equal = Datatype.from_compare
- let hash iv = Datatype.String.hash iv.iv_name + 7 * LT_List.hash iv.iv_types
- end)
-
-(**************************************************************************)
-(***************************** Helpers ************************************)
-(**************************************************************************)
-
-let rec eval_iexp env = function
- | Iunsupported | Ibinop(_, Iunsupported, _) | Ibinop(_, _, Iunsupported) ->
- Ival.inject_range None None
- | Iconst i -> i
- | Ivar iv -> Ivar.Map.find iv env
- | Ibinop(ibinop, iexp1, iexp2) ->
- let i1 = eval_iexp env iexp1 in
- let i2 = eval_iexp env iexp2 in
- match ibinop with
- | Ival_add -> Ival.add_int i1 i2
- | Ival_min -> Ival.sub_int i1 i2
- | Ival_mul -> Ival.mul i1 i2
- | Ival_div -> Ival.div i1 i2
- | Ival_join -> Ival.join i1 i2
-
-exception Not_an_integer
-
-let is_recursive li = match li.l_body with
- | LBpred _ | LBnone | LBreads _ | LBinductive _ -> false
- | LBterm t ->
- let rec has_recursive_call t = match t.term_node with
- | TConst _ | TLval _ | TSizeOf _ | TSizeOfStr _ | TAlignOf _
- | Tnull | TAddrOf _ | TStartOf _ | Tempty_set | Ttypeof _
- | Ttype _->
- false
- | Tapp(li', _, ts) ->
- String.equal li.l_var_info.lv_name li'.l_var_info.lv_name
- || List.exists has_recursive_call ts
- | TUnOp(_, t) | TSizeOfE t | TCastE(_, t) | Tat(t, _) | Tlambda(_, t)
- | Toffset(_, t) | Tbase_addr(_, t) | TAlignOfE t | Tblock_length(_, t)
- | TLogic_coerce(_, t) | TCoerce(t, _) | Tcomprehension(t, _, _)
- | Tlet(_, t) ->
- has_recursive_call t
- | TBinOp(_, t1, t2) | TCoerceE(t1, t2) | TUpdate(t1, _, t2) ->
- has_recursive_call t1 || has_recursive_call t2
- | Trange(t1_opt, t2_opt) ->
- (match t1_opt with
- | None -> begin match t2_opt with
- | None -> false
- | Some t2 -> has_recursive_call t2
- end
- | Some t1 -> begin match t2_opt with
- | None -> has_recursive_call t1
- | Some t2 -> has_recursive_call t1 || has_recursive_call t2
- end)
- | Tif(t0, t1, t2) ->
- has_recursive_call t0 || has_recursive_call t1 || has_recursive_call t2
- | TDataCons(_, ts) | Tunion ts | Tinter ts ->
- List.exists has_recursive_call ts
- in
- has_recursive_call t
-
-let rec interv_of_typ ty = match Cil.unrollType ty with
- | TInt (k,_) as ty ->
- let n = Cil.bitsSizeOf ty in
- let l, u =
- if Cil.isSigned k then Cil.min_signed_number n, Cil.max_signed_number n
- else Integer.zero, Cil.max_unsigned_number n
- in
- Ival.inject_range (Some l) (Some u)
- | TEnum(enuminfo, _) -> interv_of_typ (TInt (enuminfo.ekind, []))
- | _ ->
- raise Not_an_integer
-
-let ikind_of_interv i =
- if Ival.is_bottom i then IInt
- else match Ival.min_and_max i with
- | Some l, Some u ->
- let is_pos = Integer.ge l Integer.zero in
- let lkind = Cil.intKindForValue l is_pos in
- let ukind = Cil.intKindForValue u is_pos in
- (* kind corresponding to the interval *)
- let kind = if Cil.intTypeIncluded lkind ukind then ukind else lkind in
- (* convert the kind to [IInt] whenever smaller. *)
- if Cil.intTypeIncluded kind IInt then IInt else kind
- | None, None -> raise Cil.Not_representable (* GMP *)
- | None, Some _ | Some _, None ->
- Kernel.fatal ~current:true "ival: %a" Ival.pretty i
-
-let interv_of_typ_containing_interv i =
- try
- let kind = ikind_of_interv i in
- interv_of_typ (TInt(kind, []))
- with Cil.Not_representable ->
- (* infinity *)
- Ival.inject_range None None
-
-(**************************************************************************)
-(***************************** Builder ************************************)
-(**************************************************************************)
-
-(* Build the system of interval equations for the logic function called
- through [t].
- Example: the following function:
- f(Z n) = n < 0 ? 1 : f(n - 1) * f(n - 2) / f(n - 3)
- when called with f(37)
- will generate the following system of equations:
- X = [1; 1] U Y*Y/Y /\
- Y = [1; 1] U Z*Z/Z /\
- Z = [1; 1] U Z*Z/Z
- where X is the interval for f(int) (since 37 \in int),
- Y the one for f(long) (from int-1, int-2 and int-3)
- and Z the for the f(Z) (from long-1, long-2 and long-3) *)
-let build ~infer t =
- let rec aux ieqs ivars t = match t.term_node with
- | Tapp(li, _, args) ->
- if li.l_type = Some Linteger && is_recursive li then begin
- let args_lty =
- List.map2
- (fun lv arg ->
- try
- (* speed-up convergence; because of this approximation, no need
- to associate [i] to [lv] in [Interval.Env]: the very same
- interval will be computed anyway. *)
- let i = interv_of_typ_containing_interv (infer arg) in
- Ctype (TInt(ikind_of_interv i, []))
- with
- | Cil.Not_representable -> Linteger
- | Not_an_integer -> lv.lv_type)
- li.l_profile
- args
- in
- let ivar = { iv_name = li.l_var_info.lv_name; iv_types = args_lty } in
- (* Adding x = g(x) if it is not yet in the system of equations.
- Without this check, the algorithm would not terminate. *)
- let ieqs, ivars =
- if List.exists (fun ivar' -> Ivar.equal ivar ivar') ivars
- then ieqs, ivars
- else
- let iexp, ieqs, ivars =
- aux ieqs (ivar :: ivars) (Misc.term_of_li li)
- in
- (* Adding x = g(x) *)
- let ieqs = Ivar.Map.add ivar iexp ieqs in
- ieqs, ivars
- in
- Ivar ivar, ieqs, ivars
- end else begin
- try Iconst (infer t), ieqs, ivars
- with Not_an_integer -> Iunsupported, ieqs, ivars
- end
- | TConst _ ->
- (try Iconst(infer t), ieqs, ivars
- with Not_an_integer -> Iunsupported, ieqs, ivars)
- | TLval(TVar _, _) ->
- (try Iconst(infer t), ieqs, ivars
- with Not_an_integer -> Iunsupported, ieqs, ivars)
- | TBinOp (PlusA, t1, t2) ->
- let iexp1, ieqs, ivars = aux ieqs ivars t1 in
- let iexp2, ieqs, ivars = aux ieqs ivars t2 in
- Ibinop(Ival_add, iexp1, iexp2), ieqs, ivars
- | TBinOp (MinusA, t1, t2) ->
- let iexp1, ieqs, ivars = aux ieqs ivars t1 in
- let iexp2, ieqs, ivars = aux ieqs ivars t2 in
- Ibinop(Ival_min, iexp1, iexp2), ieqs, ivars
- | TBinOp (Mult, t1, t2) ->
- let iexp1, ieqs, ivars = aux ieqs ivars t1 in
- let iexp2, ieqs, ivars = aux ieqs ivars t2 in
- Ibinop(Ival_mul, iexp1, iexp2), ieqs, ivars
- | TBinOp (Div, t1, t2) ->
- let iexp1, ieqs, ivars = aux ieqs ivars t1 in
- let iexp2, ieqs, ivars = aux ieqs ivars t2 in
- Ibinop(Ival_div, iexp1, iexp2), ieqs, ivars
- | Tif(_, t1, t2) ->
- let iexp1, ieqs, ivars = aux ieqs ivars t1 in
- let iexp2, ieqs, ivars = aux ieqs ivars t2 in
- Ibinop(Ival_join, iexp1, iexp2), ieqs, ivars
- | _ ->
- Iunsupported, ieqs, ivars
- in
- aux Ivar.Map.empty [] t
-
-(*************************************************************************)
-(******************************** Solver *********************************)
-(*************************************************************************)
-
-(* [iterate indexes max] increases by 1 the leftmost element of [indexes] that
- is less or equal to [max].
- Eg: from index=[| 0; 0; 0 |] and max=2, the successive iterates
- until reaching index=[| max; max; max |] are as follows:
- [| 0; 0; 0 |]
- [| 1; 0; 0 |]
- [| 1; 1; 0 |]
- [| 1; 1; 1 |]
- [| 2; 1; 1 |]
- [| 2; 2; 1 |]
- [| 2; 2; 2 |]
- Note that the number [N] of iterates is linear in [max*l] where [l] is the
- length of [index]: [N=max*l+1].
- [int array] (instead of [int list]) is the proper data structure for storing
- [indexes], at least because its length is known in advance: the number of
- variables. *)
-let iterate indexes max =
- let min_i = ref 0 in
- for indexes_i = 1 to Array.length indexes - 1 do
- if indexes.(indexes_i) < indexes.(!min_i) then min_i := indexes_i
- done;
- if indexes.(!min_i) + 1 <= max then
- (* The if-test is because the last iterate cannot be increased *)
- indexes.(!min_i) <- indexes.(!min_i) + 1
-
-(* Returns an assignement to each variable of [ieqs] such that:
- - the n-th element of [indexes] is associated to the n-th variable of [ieqs]
- - a variable that is associated to an index [index] ranging in [0..max-1] is
- associated to the finite interval
- [-chain_of_ivalmax.(index), chain_of_ivalmax.(index)]
- - a variable that is associated to an index [index] equals to [max] is
- associated to [Z]. *)
-let to_iconsts chain_of_ivalmax indexes ieqs =
- let max = Array.length chain_of_ivalmax in
- let indexes_i = ref 0 in
- Ivar.Map.map
- (fun _ ->
- let ival =
- let index = indexes.(!indexes_i) in
- if index < max then
- let ivalmax = chain_of_ivalmax.(index) in
- Ival.inject_range (Some (Integer.neg ivalmax)) (Some ivalmax)
- else if index = max then Ival.inject_range None None
- else assert false
- in
- indexes_i := !indexes_i + 1;
- ival)
- ieqs
-
-let is_post_fixpoint ieqs env =
- Ivar.Map.for_all
- (fun ivar iexp ->
- let i1 = eval_iexp env iexp in
- let i2 = Ivar.Map.find ivar env in
- Ival.is_included i1 i2)
- ieqs
-
-let rec iterate_till_post_fixpoint chain_of_ivalmax indexes ieqs =
- let iconsts = to_iconsts chain_of_ivalmax indexes ieqs in
- if is_post_fixpoint ieqs iconsts then
- iconsts
- else
- let index_max = Array.length chain_of_ivalmax in
- iterate indexes index_max;
- iterate_till_post_fixpoint chain_of_ivalmax indexes ieqs
-
-let solve chain_of_ivalmax ivar ieqs =
- let dim = Ivar.Map.cardinal ieqs in
- let bottom = Array.make dim 0 in
- let post_fixpoint =
- iterate_till_post_fixpoint chain_of_ivalmax bottom ieqs
- in
- Ivar.Map.find ivar post_fixpoint
-
-let build_and_solve ~infer t =
- (* 1) Build a system of interval equations that constrain the solution: do so
- by returning a variable when encoutering a call of a recursive function
- instead of performing the usual interval inference.
-
- BEWARE: we might be tempted to memoize the solution for a given function
- signature HOWEVER: it cannot be done in a straightforward manner due to the
- cases of functions that use C (global) variables in their definition (as
- the values of those variables can change between two function calls).
-
- TODO: I do not understand the remark above. The interval of a C global
- variable is computed from its type. *)
- let iexp, ieqs, _ivars = build ~infer t in
- (* 2) Solve it:
- The problem is probably undecidable in the general case.
- Thus we just look for reasonably precise approximations
- without being too computationally expensive:
- simply iterate over a finite set of pre-defined intervals.
- See [Interval_system_solver.solve] for details. *)
- let chain_of_ivalmax =
- [| Integer.one; Integer.billion_one; Integer.max_int64 |]
- (* This set can be changed based on experimental evidences,
- but it works fine for now. *)
- in
- match iexp with
- | Ivar ivar -> solve chain_of_ivalmax ivar ieqs
- | Iconst _ | Ibinop _ | Iunsupported ->
- (* TODO: check this assert false carefully *)
- assert false
diff --git a/src/plugins/e-acsl/interval_system.mli b/src/plugins/e-acsl/interval_system.mli
deleted file mode 100644
index c0202642fbb3b82f190d36365d448aefd5b48f1d..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/interval_system.mli
+++ /dev/null
@@ -1,39 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of the Frama-C's E-ACSL plug-in. *)
-(* *)
-(* Copyright (C) 2012-2018 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-
-(** Fixpoint equation solver for infering intervals of recursively defined logic
- functions. *)
-
-val build_and_solve: infer:(term -> Ival.t) -> term -> Ival.t
-(** @return the interval of the given term denoting a recursive function. *)
-
-(*/*)
-(** The following functions should be defined in [Interval] but are here to
- break mutual module dependencies *)
-
-exception Not_an_integer
-val is_recursive: logic_info -> bool
-val interv_of_typ: typ -> Ival.t
-val ikind_of_interv: Ival.t -> Cil_types.ikind
-(*/*)
diff --git a/src/plugins/e-acsl/logic_functions.ml b/src/plugins/e-acsl/logic_functions.ml
index 01d77938dcd9799aea5608ec91d83a79a1325bac..df860ca85ce03907ed5cd5200dffbaba3f324101 100644
--- a/src/plugins/e-acsl/logic_functions.ml
+++ b/src/plugins/e-acsl/logic_functions.ml
@@ -320,10 +320,10 @@ let fill_kf lfs kf =
module Memo = Hashtbl.Make(struct
type t = lfsig_info
let equal lfs1 lfs2 =
- Cil_datatype.Logic_info.equal lfs1.lfs_li lfs2.lfs_li &&
- List.fold_left2
- (fun b lty1 lty2 -> b && Cil_datatype.Logic_type.equal lty1 lty2)
- true
+ Cil_datatype.Logic_info.equal lfs1.lfs_li lfs2.lfs_li
+ && Cil_datatype.Logic_type.equal lfs1.lfs_lty lfs2.lfs_lty
+ && List.for_all2
+ Cil_datatype.Logic_type.equal
lfs1.lfs_args_lty
lfs2.lfs_args_lty
let hash = Hashtbl.hash
@@ -370,34 +370,32 @@ let find_kfs li =
let generate ~loc env t li args args_lty =
let name = li.l_var_info.lv_name ^ "_tapp" in
let mk_call vi =
- (* Building the arguments 1/3:
- If the result is an array (eg gmp), then it cannot be returned.
- Thus we let it be the (additional) first argument. *)
+ (* Building the arguments 1/3: If the result is an array (e.g. gmp), then it
+ cannot be returned. Thus we let it be the (additional) first
+ argument. *)
let vi_f_typ = Typing.get_typ t in
let args, lvl_opt =
- if Cil.isArrayType vi_f_typ then
- (Cil.evar ~loc vi) :: args, None
- else
- args, Some (Cil.var vi)
+ if Cil.isArrayType vi_f_typ then Cil.evar ~loc vi :: args, None
+ else args, Some (Cil.var vi)
in
- (* Building the arguments 2/3:
- AST sanity: arrays that are given as arguments of functions
- must be explicitely indicated as being pointers *)
- let args = List.map
- (fun arg ->
- if Cil_datatype.Typ.equal (Cil.typeOf arg) (Gmpz.t ()) then
- (* TODO: real numbers *)
- Cil.mkCast ~force:true ~e:arg ~newt:(Gmpz.t_ptr ())
- else
- arg)
- args
+ (* Building the arguments 2/3: AST sanity: arrays that are given as
+ arguments of functions must be explicitely indicated as being pointers *)
+ let args =
+ List.map
+ (fun arg ->
+ if Cil_datatype.Typ.equal (Cil.typeOf arg) (Gmpz.t ()) then
+ (* TODO: real numbers *)
+ Cil.mkCast ~force:true ~e:arg ~newt:(Gmpz.t_ptr ())
+ else
+ arg)
+ args
in
- (* Building the arguments 3/3:
- E-ACSL typing: short and other integer types less than in
- are cast into int *)
- let args = List.map
- (fun arg ->
- match Cil.typeOf arg with
+ (* Building the arguments 3/3: E-ACSL typing: short and other integer types
+ less than int are casted into int *)
+ let args =
+ List.map
+ (fun arg ->
+ match Cil.typeOf arg with
| TInt(kind, _) ->
if Cil.intTypeIncluded kind IInt then
Cil.mkCast ~force:false ~e:arg ~newt:Cil.intType
@@ -413,12 +411,7 @@ let generate ~loc env t li args args_lty =
| Typing.C_type ik -> Ctype (TInt (ik, []))
| Typing.Other -> t.term_type
in
- let lfs = {
- lfs_li = li;
- lfs_lty = lty;
- lfs_args_lty = args_lty;
- }
- in
+ let lfs = { lfs_li = li; lfs_lty = lty; lfs_args_lty = args_lty } in
(* Memoization. We MUST guarantee that interval and type bindings
for logic vars, terms and predicates from the logic definition of
the function are restored after memoization. *)
@@ -430,12 +423,7 @@ let generate ~loc env t li args args_lty =
(* The call stmt *)
let fundec = get_fundec kf in
let vi_f = fundec.svar in
- Cil.mkStmtOneInstr
- (Call (
- lvl_opt,
- (Cil.evar vi_f),
- args,
- loc))
+ Cil.mkStmtOneInstr (Call (lvl_opt, Cil.evar vi_f, args, loc))
in
match Typing.get_integer_ty t with
| Typing.C_type _ | Typing.Other ->
diff --git a/src/plugins/e-acsl/tests/gmp/functions.c b/src/plugins/e-acsl/tests/gmp/functions.c
index 28bc4017c14c2a2bafef9f87b752f3d69866025a..80f796bad6a411b8a1b6a62cec3b07e2d481e244 100644
--- a/src/plugins/e-acsl/tests/gmp/functions.c
+++ b/src/plugins/e-acsl/tests/gmp/functions.c
@@ -64,8 +64,9 @@ int main (void) {
k(9);
- double d = 2.0;
- /*@ assert f2(d) > 0; */ ;
- /*@ assert p_notyet(27); */ ;
- /*@ assert f_notyet(27) == 27; */ ;
+ // not yet supported
+ /* double d = 2.0; */
+ /* /\*@ assert f2(d) > 0; *\/ ; */
+ /* /\*@ assert p_notyet(27); *\/ ; */
+ /* /\*@ assert f_notyet(27) == 27; *\/ ; */
}
diff --git a/src/plugins/e-acsl/tests/gmp/functions_rec.c b/src/plugins/e-acsl/tests/gmp/functions_rec.c
index 990f4826c59baa838f86b3998f87eb0f61ba3391..c6d10713c13db41ea1ae49ada585bd394b20262b 100644
--- a/src/plugins/e-acsl/tests/gmp/functions_rec.c
+++ b/src/plugins/e-acsl/tests/gmp/functions_rec.c
@@ -27,4 +27,4 @@ int main (void) {
/*@ assert f3(6) == -5; */ ;
/*@assert f4(9) > 0; */ ;
-}
\ No newline at end of file
+}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
index e336cb46d6955e3ea0106a7d95aaabeb96f12b65..d4d91c76d035679d586c57d4ad1c69bfdd4215af 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
@@ -1,14 +1,4 @@
[e-acsl] beginning translation.
-[e-acsl] tests/gmp/functions.c:34: Warning:
- E-ACSL construct `logic functions with no definition nor reads clause'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/gmp/functions.c:69: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/gmp/functions.c:70: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -32,6 +22,8 @@
[eva] using specification for function __gmpz_clear
[eva:alarm] tests/gmp/functions.c:44: Warning:
function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:47: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/functions.c:48: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle
index 70b854b31ac15b270cfc7416945a12c5719fab24..50251e30668c0c2def5e8e3c11cdc954dbe9fbdf 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle
@@ -1,14 +1,4 @@
[e-acsl] beginning translation.
-[e-acsl] tests/gmp/functions.c:34: Warning:
- E-ACSL construct `logic functions with no definition nor reads clause'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/gmp/functions.c:69: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/gmp/functions.c:70: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
index fd3c27e93ad526159f4e3faafe4429befb662b3c..ff3377f7af83998145077713848304f591b5c218 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
@@ -17,19 +17,19 @@ int __gen_e_acsl_p1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
*/
int __gen_e_acsl_p2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
+int __gen_e_acsl_p2_3(int __gen_e_acsl_x_arg, long __gen_e_acsl_y_arg);
+
int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg);
/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
*/
-void __gen_e_acsl_f1_4(__e_acsl_mpz_struct * __retres_arg,
+void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
__e_acsl_mpz_struct * __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg);
-int __gen_e_acsl_f1_2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
-
-void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
+void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
int __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg);
@@ -77,8 +77,6 @@ int glob = 5;
*/
/*@ logic double f2(double x) = (double)(1 / x);
*/
-double __gen_e_acsl_f2(double __gen_e_acsl_x_arg);
-
/*@ predicate p_notyet{L}(ℤ x) = x > 0;
*/
/*@ logic ℤ f_notyet{L}(ℤ x) = x;
@@ -126,59 +124,59 @@ int main(void)
}
/*@ assert p2(x, f1(3, 4)); */
{
- int __gen_e_acsl_f1_tapp_2;
+ long __gen_e_acsl_f1_tapp_2;
int __gen_e_acsl_p2_tapp_3;
- __gen_e_acsl_f1_tapp_2 = __gen_e_acsl_f1_2(3,4);
- __gen_e_acsl_p2_tapp_3 = __gen_e_acsl_p2(x,__gen_e_acsl_f1_tapp_2);
+ __gen_e_acsl_f1_tapp_2 = __gen_e_acsl_f1(3,4);
+ __gen_e_acsl_p2_tapp_3 = __gen_e_acsl_p2_3(x,__gen_e_acsl_f1_tapp_2);
__e_acsl_assert(__gen_e_acsl_p2_tapp_3,(char *)"Assertion",
(char *)"main",(char *)"p2(x, f1(3, 4))",47);
}
/*@ assert f1(9, 99999999999999999999999999999) > 0; */
{
- __e_acsl_mpz_t __gen_e_acsl__3;
- __e_acsl_mpz_t __gen_e_acsl_f1_tapp_3;
__e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_gt_2;
- __gmpz_init_set_str(__gen_e_acsl__3,"99999999999999999999999999999",10);
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_3;
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ int __gen_e_acsl_gt_3;
+ __gmpz_init_set_str(__gen_e_acsl__4,"99999999999999999999999999999",10);
__gmpz_init(__gen_e_acsl_f1_tapp_3);
/*@ assert
Eva: initialization:
\initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3);
*/
- __gen_e_acsl_f1_3((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3,9,
- (__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_tapp_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- __e_acsl_assert(__gen_e_acsl_gt_2 > 0,(char *)"Assertion",(char *)"main",
+ __gen_e_acsl_f1_2((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3,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_tapp_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __e_acsl_assert(__gen_e_acsl_gt_3 > 0,(char *)"Assertion",(char *)"main",
(char *)"f1(9, 99999999999999999999999999999) > 0",48);
- __gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl_f1_tapp_3);
__gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl_f1_tapp_3);
+ __gmpz_clear(__gen_e_acsl__5);
}
/*@ assert
f1(99999999999999999999999999999, 99999999999999999999999999999) ≡
199999999999999999999999999998;
*/
{
- __e_acsl_mpz_t __gen_e_acsl__5;
- __e_acsl_mpz_t __gen_e_acsl_f1_tapp_4;
__e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_4;
+ __e_acsl_mpz_t __gen_e_acsl__7;
int __gen_e_acsl_eq;
- __gmpz_init_set_str(__gen_e_acsl__5,"99999999999999999999999999999",10);
+ __gmpz_init_set_str(__gen_e_acsl__6,"99999999999999999999999999999",10);
__gmpz_init(__gen_e_acsl_f1_tapp_4);
- __gen_e_acsl_f1_4((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_4,
- (__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_f1_3((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_4,
+ (__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);
__gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
(char *)"f1(99999999999999999999999999999, 99999999999999999999999999999) ==\n199999999999999999999999999998",
49);
- __gmpz_clear(__gen_e_acsl__5);
- __gmpz_clear(__gen_e_acsl_f1_tapp_4);
__gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_f1_tapp_4);
+ __gmpz_clear(__gen_e_acsl__7);
}
/*@ assert g(x) ≡ x; */
{
@@ -217,16 +215,6 @@ int main(void)
(char *)"main",(char *)"t2(t1(m)) == 17",63);
}
__gen_e_acsl_k(9);
- double d = 2.0;
- /*@ assert f2(d) > 0; */
- {
- double __gen_e_acsl_f2_tapp;
- __gen_e_acsl_f2_tapp = __gen_e_acsl_f2(d);
- __e_acsl_assert(__gen_e_acsl_f2_tapp > (double)0,(char *)"Assertion",
- (char *)"main",(char *)"f2(d) > 0",68);
- }
- /*@ assert p_notyet(27); */ ;
- /*@ assert f_notyet(27) ≡ 27; */ ;
__retres = 0;
return __retres;
}
@@ -244,13 +232,6 @@ void __gen_e_acsl_k(int x)
return;
}
-double __gen_e_acsl_f2(double __gen_e_acsl_x_arg)
-{
- double __retres;
- __retres = (double)((long double)1 / __gen_e_acsl_x_arg);
- return __retres;
-}
-
int __gen_e_acsl_k_pred(int __gen_e_acsl_x_arg)
{
int __retres;
@@ -309,58 +290,51 @@ long __gen_e_acsl_f1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
return __retres;
}
-void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
+void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
int __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg)
{
- __e_acsl_mpz_t __gen_e_acsl_y_2;
- __e_acsl_mpz_t __gen_e_acsl_x_2;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
- __gmpz_init_set(__gen_e_acsl_y_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
- __gmpz_init_set_si(__gen_e_acsl_x_2,(long)__gen_e_acsl_x_arg);
- __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_2));
- __gmpz_init_set(__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
- __gmpz_clear(__gen_e_acsl_y_2);
- __gmpz_clear(__gen_e_acsl_x_2);
- __gmpz_clear(__gen_e_acsl_add_2);
- return;
-}
-
-int __gen_e_acsl_f1_2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
-{
- long __retres;
- __retres = (int)(__gen_e_acsl_x_arg + (long)__gen_e_acsl_y_arg);
- return __retres;
-}
-
-void __gen_e_acsl_f1_4(__e_acsl_mpz_struct * __retres_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_x_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_y_arg)
-{
- __e_acsl_mpz_t __gen_e_acsl_x_3;
__e_acsl_mpz_t __gen_e_acsl_y_3;
+ __e_acsl_mpz_t __gen_e_acsl_x_3;
__e_acsl_mpz_t __gen_e_acsl_add_3;
- __gmpz_init_set(__gen_e_acsl_x_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_arg));
__gmpz_init_set(__gen_e_acsl_y_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
+ __gmpz_init_set_si(__gen_e_acsl_x_3,(long)__gen_e_acsl_x_arg);
__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_struct const *)(__gen_e_acsl_y_3));
__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_y_3);
+ __gmpz_clear(__gen_e_acsl_x_3);
__gmpz_clear(__gen_e_acsl_add_3);
return;
}
+void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_4;
+ __e_acsl_mpz_t __gen_e_acsl_y_4;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __gmpz_init_set(__gen_e_acsl_x_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_arg));
+ __gmpz_init_set(__gen_e_acsl_y_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
+ __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_4));
+ __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_4);
+ __gmpz_clear(__gen_e_acsl_add_4);
+ return;
+}
+
int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg)
{
@@ -387,6 +361,31 @@ int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
return __retres;
}
+int __gen_e_acsl_p2_3(int __gen_e_acsl_x_arg, long __gen_e_acsl_y_arg)
+{
+ int __retres;
+ __e_acsl_mpz_t __gen_e_acsl_x_2;
+ __e_acsl_mpz_t __gen_e_acsl_y_2;
+ __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)__gen_e_acsl_x_arg);
+ __gmpz_init_set_si(__gen_e_acsl_y_2,__gen_e_acsl_y_arg);
+ __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_2));
+ __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));
+ __retres = __gen_e_acsl_gt_2 > 0;
+ __gmpz_clear(__gen_e_acsl_x_2);
+ __gmpz_clear(__gen_e_acsl_y_2);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl__3);
+ return __retres;
+}
+
int __gen_e_acsl_p2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
index bbf29e6ab39b95c8cc9643beedb22b12c7aeb04f..a06e1629b8c1f2bd11e05973dd83841c789b3e17 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
@@ -78,8 +78,6 @@ int glob = 5;
*/
/*@ logic double f2(double x) = (double)(1 / x);
*/
-double __gen_e_acsl_f2(double __gen_e_acsl_x_arg);
-
/*@ predicate p_notyet{L}(ℤ x) = x > 0;
*/
/*@ logic ℤ f_notyet{L}(ℤ x) = x;
@@ -264,16 +262,6 @@ int main(void)
__gmpz_clear(__gen_e_acsl__12);
}
__gen_e_acsl_k(9);
- double d = 2.0;
- /*@ assert f2(d) > 0; */
- {
- double __gen_e_acsl_f2_tapp;
- __gen_e_acsl_f2_tapp = __gen_e_acsl_f2(d);
- __e_acsl_assert(__gen_e_acsl_f2_tapp > (double)0,(char *)"Assertion",
- (char *)"main",(char *)"f2(d) > 0",68);
- }
- /*@ assert p_notyet(27); */ ;
- /*@ assert f_notyet(27) ≡ 27; */ ;
__retres = 0;
return __retres;
}
@@ -291,13 +279,6 @@ void __gen_e_acsl_k(int x)
return;
}
-double __gen_e_acsl_f2(double __gen_e_acsl_x_arg)
-{
- double __retres;
- __retres = (double)((long double)1 / __gen_e_acsl_x_arg);
- return __retres;
-}
-
int __gen_e_acsl_k_pred(int __gen_e_acsl_x_arg)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c
index 10ad7f46881fda9fd743823410a258bf0a5b50c5..b4ac4d23a38a3311fa9e082569097e0965709471 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c
@@ -45,11 +45,11 @@ logic ℤ f4(ℤ n) =
n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
*/
-long __gen_e_acsl_f4(int __gen_e_acsl_n_arg);
+unsigned long __gen_e_acsl_f4(int __gen_e_acsl_n_arg);
-long __gen_e_acsl_f4_2(long __gen_e_acsl_n_arg);
+unsigned long __gen_e_acsl_f4_2(long __gen_e_acsl_n_arg);
-long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg);
+unsigned long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg);
int main(void)
{
@@ -120,22 +120,22 @@ int main(void)
}
/*@ assert f4(9) > 0; */
{
- long __gen_e_acsl_f4_tapp;
+ unsigned long __gen_e_acsl_f4_tapp;
__gen_e_acsl_f4_tapp = __gen_e_acsl_f4(9);
- __e_acsl_assert(__gen_e_acsl_f4_tapp > 0L,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_f4_tapp > 0UL,(char *)"Assertion",
(char *)"main",(char *)"f4(9) > 0",29);
}
__retres = 0;
return __retres;
}
-long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
+unsigned long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
{
- long __retres;
+ unsigned long __retres;
__e_acsl_mpz_t __gen_e_acsl_n_11;
__e_acsl_mpz_t __gen_e_acsl__23;
int __gen_e_acsl_lt_2;
- long __gen_e_acsl_if_11;
+ unsigned long __gen_e_acsl_if_11;
__gmpz_init_set(__gen_e_acsl_n_11,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n_arg));
__gmpz_init_set_si(__gen_e_acsl__23,100L);
@@ -144,7 +144,7 @@ long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
if (__gen_e_acsl_lt_2 < 0) {
__e_acsl_mpz_t __gen_e_acsl__24;
__e_acsl_mpz_t __gen_e_acsl_add_7;
- long __gen_e_acsl_f4_tapp_4;
+ unsigned long __gen_e_acsl_f4_tapp_4;
__gmpz_init_set_si(__gen_e_acsl__24,1L);
__gmpz_init(__gen_e_acsl_add_7);
__gmpz_add(__gen_e_acsl_add_7,
@@ -164,7 +164,7 @@ long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
if (__gen_e_acsl_lt_3 < 0) __gen_e_acsl_if_10 = 9223372036854775807UL;
else __gen_e_acsl_if_10 = 6UL;
- __gen_e_acsl_if_11 = (long)__gen_e_acsl_if_10;
+ __gen_e_acsl_if_11 = __gen_e_acsl_if_10;
__gmpz_clear(__gen_e_acsl__25);
}
__retres = __gen_e_acsl_if_11;
@@ -173,15 +173,15 @@ long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
return __retres;
}
-long __gen_e_acsl_f4_2(long __gen_e_acsl_n_arg)
+unsigned long __gen_e_acsl_f4_2(long __gen_e_acsl_n_arg)
{
- long __retres;
- long __gen_e_acsl_if_13;
+ unsigned long __retres;
+ unsigned long __gen_e_acsl_if_13;
if (__gen_e_acsl_n_arg < 100L) {
__e_acsl_mpz_t __gen_e_acsl_n_10;
__e_acsl_mpz_t __gen_e_acsl__22;
__e_acsl_mpz_t __gen_e_acsl_add_6;
- long __gen_e_acsl_f4_tapp_3;
+ unsigned long __gen_e_acsl_f4_tapp_3;
__gmpz_init_set_si(__gen_e_acsl_n_10,__gen_e_acsl_n_arg);
__gmpz_init_set_si(__gen_e_acsl__22,1L);
__gmpz_init(__gen_e_acsl_add_6);
@@ -198,18 +198,18 @@ long __gen_e_acsl_f4_2(long __gen_e_acsl_n_arg)
unsigned long __gen_e_acsl_if_12;
if (__gen_e_acsl_n_arg < 9223372036854775807L) __gen_e_acsl_if_12 = 9223372036854775807UL;
else __gen_e_acsl_if_12 = 6UL;
- __gen_e_acsl_if_13 = (long)__gen_e_acsl_if_12;
+ __gen_e_acsl_if_13 = __gen_e_acsl_if_12;
}
__retres = __gen_e_acsl_if_13;
return __retres;
}
-long __gen_e_acsl_f4(int __gen_e_acsl_n_arg)
+unsigned long __gen_e_acsl_f4(int __gen_e_acsl_n_arg)
{
- long __retres;
- long __gen_e_acsl_if_15;
+ unsigned long __retres;
+ unsigned long __gen_e_acsl_if_15;
if (__gen_e_acsl_n_arg < 100) {
- long __gen_e_acsl_f4_tapp_2;
+ unsigned long __gen_e_acsl_f4_tapp_2;
__gen_e_acsl_f4_tapp_2 = __gen_e_acsl_f4_2(__gen_e_acsl_n_arg + 1L);
__gen_e_acsl_if_15 = __gen_e_acsl_f4_tapp_2;
}
@@ -217,7 +217,7 @@ long __gen_e_acsl_f4(int __gen_e_acsl_n_arg)
unsigned long __gen_e_acsl_if_14;
if ((long)__gen_e_acsl_n_arg < 9223372036854775807L) __gen_e_acsl_if_14 = 9223372036854775807UL;
else __gen_e_acsl_if_14 = 6UL;
- __gen_e_acsl_if_15 = (long)__gen_e_acsl_if_14;
+ __gen_e_acsl_if_15 = __gen_e_acsl_if_14;
}
__retres = __gen_e_acsl_if_15;
return __retres;
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 094e827301217b0f90d8946d54e091d2fa7ad76f..65bd562cd774b38aac55279ee042e5260510cbb0 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -477,12 +477,13 @@ and context_insensitive_term_to_exp kf env t =
[ Misc.mk_call ~loc ~result:(Cil.var vi) fname (List.rev args) ])
end
else
- let args_lty = List.map
- (fun targ ->
- match Typing.get_integer_ty targ with
- | Typing.Gmp -> Linteger
- | Typing.C_type _ | Typing.Other -> Ctype (Typing.get_typ targ))
- targs
+ let args_lty =
+ List.map
+ (fun targ ->
+ match Typing.get_integer_ty targ with
+ | Typing.Gmp -> Linteger
+ | Typing.C_type _ | Typing.Other -> Ctype (Typing.get_typ targ))
+ targs
in
Logic_functions.generate ~loc env t li (List.rev args) args_lty
in
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 22799c4839d7ff32dc7dbd5ef5c419abdb78f3f6..c88dafb9106819e2c51158f7febd398d4883c8b3 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -487,9 +487,10 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
Thus using [Extlib.the] is fine *)
dup (ty_of_logic_ty (Extlib.the li.l_type))
else begin
- List.iter
- (fun arg -> ignore (type_term ~use_gmp_opt:true arg))
- args;
+ (* TODO: what if the type of the parameter is smaller than the infered
+ type of the argument? For now, it is silently ignored (both
+ statically and at runtime)... *)
+ List.iter (fun arg -> ignore (type_term ~use_gmp_opt:true arg)) args;
match li.l_body with
| LBpred _ ->
(* We can have an [LBpred] here because we transformed
@@ -503,8 +504,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
match lty with
| Linteger ->
let i = Interval.infer t in
- if Options.Gmp_only.get () then dup Gmp
- else dup (ty_of_interv i)
+ if Options.Gmp_only.get () then dup Gmp else dup (ty_of_interv i)
| Ctype TInt(ik, _ ) ->
dup (C_type ik)
| Ctype TFloat _ -> (* TODO: handle in MR !226 *)