diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 6d65b5a675e468226ef4739331e01a887e5aabe5..27a16ec4928a4fd6f33be06c4e7a69e9fcecf97c 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -21,16 +21,12 @@
(**************************************************************************)
open Cil_types
-open Cil_datatype
open Locations
-open Abstract_interp
open Cvalue
-open Bit_utils
-
(* Truth values for a predicate analyzed by the value analysis *)
-type predicate_status = Comp.result = True | False | Unknown
+type predicate_status = Abstract_interp.Comp.result = True | False | Unknown
let string_of_predicate_status = function
| Unknown -> "unknown"
@@ -46,9 +42,8 @@ let join_predicate_status x y = match x, y with
| True, False | False, True
| Unknown, _ | _, Unknown -> Unknown
-exception Stop
-
let _join_list_predicate_status l =
+ let exception Stop in
try
let r =
List.fold_left
@@ -139,7 +134,12 @@ let contains_invalid_loc access loc =
let valid_loc = Locations.valid_part access loc in
not (Locations.Location.equal loc valid_loc)
-(* Evaluation environments. Used to evaluate predicate on \at nodes *)
+(* -------------------------------------------------------------------------- *)
+(* --- Evaluation environments. --- *)
+(* -------------------------------------------------------------------------- *)
+
+(* Evaluation environments are used to evaluate predicate on \at nodes,
+ the varinfo \result and logic variables introduced by quantifiers. *)
(* Labels:
pre: pre-state of the function. Equivalent to \old in the postcondition
@@ -169,6 +169,7 @@ let contains_invalid_loc access loc =
to force its re-evaluation.
*)
+module Logic_label = Cil_datatype.Logic_label
type labels_states = Cvalue.Model.t Logic_label.Map.t
let join_label_states m1 m2 =
@@ -316,9 +317,9 @@ let bind_logic_vars env lvs =
| Lreal -> bind_logic_var top_float
| Ctype ctyp when Cil.isIntegralType ctyp ->
let base = Base.of_c_logic_var lv in
- let size = Int.of_int (Cil.bitsSizeOf ctyp) in
+ let size = Integer.of_int (Cil.bitsSizeOf ctyp) in
let v = Cvalue.V_Or_Uninitialized.initialized V.top_int in
- let state = Model.add_base_value base ~size v ~size_v:Int.one state in
+ let state = Model.add_base_value base ~size v ~size_v:Integer.one state in
state, logic_vars
| _ -> unsupported_lvar lv
in
@@ -359,68 +360,21 @@ let unbind_logic_vars env lvs =
let state, logic_vars = List.fold_left unbind_one (state, env.logic_vars) lvs in
overwrite_current_state { env with logic_vars } state
-let lop_to_cop op =
- match op with
- | Req -> Eq
- | Rneq -> Ne
- | Rle -> Le
- | Rge -> Ge
- | Rlt -> Lt
- | Rgt -> Gt
-
-(* Types currently understood in the evaluation of the logic: no arrays,
- structs, logic arrays or subtle ACSL types. Sets of sets seem to
- be flattened, so the current treatment of them is correct. *)
-let rec isLogicNonCompositeType t =
- match t with
- | Lvar _ | Larrow _ -> false
- | Ltype (info, _) ->
- Logic_const.is_boolean_type t ||
- info.lt_name = "sign" ||
- (try isLogicNonCompositeType (Logic_const.type_of_element t)
- with Failure _ -> false)
- | Linteger | Lreal -> true
- | Ctype t -> Cil.isArithmeticOrPointerType t
-
-let rec infer_type = function
- | Ctype t ->
- (match t with
- | TInt _ -> Cil.intType
- | TFloat _ -> Cil.doubleType
- | _ -> t)
- | Lvar _ -> Cil.voidPtrType (* For polymorphic empty sets *)
- | Linteger -> Cil.intType
- | Lreal -> Cil.doubleType
- | Ltype _ | Larrow _ as t ->
- if Logic_const.is_plain_type t then
- unsupported (Pretty_utils.to_string Cil_datatype.Logic_type.pretty t)
- else Logic_const.plain_or_set infer_type t
-
-(* Best effort for comparing the types currently understood by Value: ignore
- differences in integer and floating-point sizes, that are meaningless
- in the logic *)
-let same_etype t1 t2 =
- match Cil.unrollType t1, Cil.unrollType t2 with
- | (TInt _ | TEnum _), (TInt _ | TEnum _) -> true
- | TFloat _, TFloat _ -> true
- | TPtr (p1, _), TPtr (p2, _) -> Cil_datatype.Typ.equal p1 p2
- | _, _ -> Cil_datatype.Typ.equal t1 t2
-
-let infer_binop_res_type op targ =
- match op with
- | PlusA | MinusA | Mult | Div -> targ
- | PlusPI | MinusPI | IndexPI ->
- assert (Cil.isPointerType targ); targ
- | MinusPP -> Cil.intType
- | Mod | Shiftlt | Shiftrt | BAnd | BXor | BOr ->
- (* can only be applied on integral arguments *)
- assert (Cil.isIntegralType targ); Cil.intType
- | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr ->
- Cil.intType (* those operators always return a boolean *)
+(* -------------------------------------------------------------------------- *)
+(* --- Evaluation results. --- *)
+(* -------------------------------------------------------------------------- *)
-(* Computes [*tsets], assuming that [tsets] has a pointer type. *)
-let deref_tsets tsets = Cil.mkTermMem ~addr:tsets ~off:TNoOffset
+(* Result of the evaluation of a term as an exact location (to reduce its value
+ in the current state). *)
+type exact_location =
+ | Location of typ * Locations.location
+ (* A location represented in the cvalue state. *)
+ | Logic_var of logic_var
+ (* A logic variable, introduced by a quantifier, and stored in an environment
+ besides the states. *)
+(* Raised when a term cannot be evaluated as an exact location.*)
+exception Not_an_exact_loc
type logic_deps = Zone.t Logic_label.Map.t
@@ -444,7 +398,6 @@ let join_logic_deps (ld1:logic_deps) (ld2: logic_deps) : logic_deps =
let empty_logic_deps =
Logic_label.Map.add lbl_here Zone.bottom Logic_label.Map.empty
-
(* Type holding the result of an evaluation. Currently, 'a is either
[Cvalue.V.t] for [eval_term], and [Location_Bits.t] for [eval_tlval_as_loc],
and [Ival.t] for [eval_toffset].
@@ -487,13 +440,121 @@ let under_from_over eover =
if Cvalue.V.cardinal_zero_or_one eover
then eover
else Cvalue.V.bottom
-;;
let under_loc_from_over eover =
if Locations.Location_Bits.cardinal_zero_or_one eover
then eover
else Locations.Location_Bits.bottom
-;;
+
+(* Injects [cvalue] as an eval_result of type [typ] with no dependencies. *)
+let inject_no_deps typ cvalue =
+ { etype = typ;
+ eunder = under_from_over cvalue;
+ eover = cvalue;
+ empty = false;
+ ldeps = empty_logic_deps }
+
+(* Integer result with no memory dependencies: constants, sizeof & alignof,
+ and values of logic variables.*)
+let einteger = inject_no_deps Cil.intType
+
+(* Note: some reals cannot be exactly represented as floats; in which
+ case we do not know their under-approximation. *)
+let ereal fval = inject_no_deps Cil.doubleType (Cvalue.V.inject_float fval)
+let efloat fval = inject_no_deps Cil.floatType (Cvalue.V.inject_float fval)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Utilitary functions on the Cil AST --- *)
+(* -------------------------------------------------------------------------- *)
+
+let is_rel_binop = function
+ | Lt
+ | Gt
+ | Le
+ | Ge
+ | Eq
+ | Ne -> true
+ | _ -> false
+
+let lop_to_cop op =
+ match op with
+ | Req -> Eq
+ | Rneq -> Ne
+ | Rle -> Le
+ | Rge -> Ge
+ | Rlt -> Lt
+ | Rgt -> Gt
+
+let rel_of_binop = function
+ | Lt -> Rlt
+ | Gt -> Rgt
+ | Le -> Rle
+ | Ge -> Rge
+ | Eq -> Req
+ | Ne -> Rneq
+ | _ -> assert false
+
+(* Types currently understood in the evaluation of the logic: no arrays,
+ structs, logic arrays or subtle ACSL types. Sets of sets seem to
+ be flattened, so the current treatment of them is correct. *)
+let rec isLogicNonCompositeType t =
+ match t with
+ | Lvar _ | Larrow _ -> false
+ | Ltype (info, _) ->
+ Logic_const.is_boolean_type t ||
+ info.lt_name = "sign" ||
+ (try isLogicNonCompositeType (Logic_const.type_of_element t)
+ with Failure _ -> false)
+ | Linteger | Lreal -> true
+ | Ctype t -> Cil.isArithmeticOrPointerType t
+
+let rec infer_type = function
+ | Ctype t ->
+ (match t with
+ | TInt _ -> Cil.intType
+ | TFloat _ -> Cil.doubleType
+ | _ -> t)
+ | Lvar _ -> Cil.voidPtrType (* For polymorphic empty sets *)
+ | Linteger -> Cil.intType
+ | Lreal -> Cil.doubleType
+ | Ltype _ | Larrow _ as t ->
+ if Logic_const.is_plain_type t then
+ unsupported (Pretty_utils.to_string Cil_datatype.Logic_type.pretty t)
+ else Logic_const.plain_or_set infer_type t
+
+(* Best effort for comparing the types currently understood by Value: ignore
+ differences in integer and floating-point sizes, that are meaningless
+ in the logic *)
+let same_etype t1 t2 =
+ match Cil.unrollType t1, Cil.unrollType t2 with
+ | (TInt _ | TEnum _), (TInt _ | TEnum _) -> true
+ | TFloat _, TFloat _ -> true
+ | TPtr (p1, _), TPtr (p2, _) -> Cil_datatype.Typ.equal p1 p2
+ | _, _ -> Cil_datatype.Typ.equal t1 t2
+
+let infer_binop_res_type op targ =
+ match op with
+ | PlusA | MinusA | Mult | Div -> targ
+ | PlusPI | MinusPI | IndexPI ->
+ assert (Cil.isPointerType targ); targ
+ | MinusPP -> Cil.intType
+ | Mod | Shiftlt | Shiftrt | BAnd | BXor | BOr ->
+ (* can only be applied on integral arguments *)
+ assert (Cil.isIntegralType targ); Cil.intType
+ | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr ->
+ Cil.intType (* those operators always return a boolean *)
+
+(* Computes [*tsets], assuming that [tsets] has a pointer type. *)
+let deref_tsets tsets = Cil.mkTermMem ~addr:tsets ~off:TNoOffset
+
+(* returns true iff the logic variable is defined by the
+ Frama-C standard library *)
+let comes_from_fc_stdlib lvar =
+ Cil.is_in_libc lvar.lv_attr ||
+ match lvar.lv_origin with
+ | None -> false
+ | Some vi ->
+ Cil.is_in_libc vi.vattr
let is_noop_cast ~src_typ ~dst_typ =
let src_typ = Logic_const.plain_or_set
@@ -512,45 +573,39 @@ let is_noop_cast ~src_typ ~dst_typ =
| Some (TSPtr _), Some (TSPtr _) -> true
| _ -> false
-(* Injects [cvalue] as an eval_result of type [typ] with no dependencies. *)
-let inject_no_deps typ cvalue =
- { etype = typ;
- eunder = under_from_over cvalue;
- eover = cvalue;
- empty = false;
- ldeps = empty_logic_deps }
-
-(* Integer result with no memory dependencies: constants, sizeof & alignof,
- and values of logic variables.*)
-let einteger = inject_no_deps Cil.intType
+(* If casting [trm] to [typ] has no effect in terms of the values contained
+ in [trm], do nothing. Otherwise, raise [exn]. Adapted from [pass_cast] *)
+let pass_logic_cast exn typ trm =
+ match Logic_utils.unroll_type typ, Logic_utils.unroll_type trm.term_type with
+ | Linteger, Ctype (TInt _ | TEnum _) -> () (* Always inclusion *)
+ | Ctype (TInt _ | TEnum _ as typ), Ctype (TInt _ | TEnum _ as typeoftrm) ->
+ let sztyp = Bit_utils.sizeof typ in
+ let szexpr = Bit_utils.sizeof typeoftrm in
+ let styp, sexpr =
+ match sztyp, szexpr with
+ | Int_Base.Value styp, Int_Base.Value sexpr -> styp, sexpr
+ | _ -> raise exn
+ in
+ let sityp = Bit_utils.is_signed_int_enum_pointer typ in
+ let sisexpr = Bit_utils.is_signed_int_enum_pointer typeoftrm in
+ if (Integer.ge styp sexpr && sityp = sisexpr) (* larger, same signedness *)
+ || (Integer.gt styp sexpr && sityp) (* strictly larger and signed *)
+ then ()
+ else raise exn
-(* Note: some reals cannot be exactly represented as floats; in which
- case we do not know their under-approximation. *)
-let ereal fval = inject_no_deps Cil.doubleType (Cvalue.V.inject_float fval)
-let efloat fval = inject_no_deps Cil.floatType (Cvalue.V.inject_float fval)
+ | Lreal, Ctype (TFloat _) -> () (* Always inclusion *)
+ | Ctype (TFloat (f1,_)), Ctype (TFloat (f2, _)) ->
+ if Cil.frank f1 < Cil.frank f2
+ then raise exn
-let is_true = function
- | `True | `TrueReduced _ -> true
- | `Unknown _ | `False | `Unreachable -> false
+ | _ -> raise exn (* Not a scalar type *)
-(* Check "logic alarms" when evaluating [v1 op v2]. All operators shifts are
- defined unambiguously in ACSL. *)
-let check_logic_alarms ~alarm_mode typ (_v1: V.t eval_result) op v2 =
- match op with
- | Div | Mod when Cil.isIntegralOrPointerType typ ->
- let truth = Cvalue_forward.assume_non_zero v2.eover in
- let division_by_zero = not (is_true truth) in
- track_alarms division_by_zero alarm_mode
- | Shiftlt | Shiftrt -> begin
- (* Check that [e2] is positive. [e1] can be arbitrary, we use
- the arithmetic vision of shifts *)
- try
- let i2 = Cvalue.V.project_ival_bottom v2.eover in
- let valid = Ival.is_included i2 Ival.positive_integers in
- track_alarms (not valid) alarm_mode
- with Cvalue.V.Not_based_on_null -> track_alarms true alarm_mode
- end
- | _ -> ()
+let is_same_term_coerce t1 t2 =
+ match t1.term_node, t2.term_node with
+ | TLogic_coerce _, TLogic_coerce _ -> Logic_utils.is_same_term t1 t2
+ | TLogic_coerce (_,t1), _ -> Logic_utils.is_same_term t1 t2
+ | _, TLogic_coerce(_,t2) -> Logic_utils.is_same_term t1 t2
+ | _ -> Logic_utils.is_same_term t1 t2
(* Constrain the ACSL range [idx] when it is used to access an array of
[size_arr] cells, and it is a Trange in which one size is not
@@ -569,140 +624,18 @@ let constraint_trange idx size_arr =
in
let up = match up with (* constrained r.h.s *)
| Some _ -> up
- | None -> Some (Logic_const.tint ~loc (Int.pred size))
+ | None -> Some (Logic_const.tint ~loc (Integer.pred size))
in
Logic_const.trange ~loc (low, up)
end
| _ -> idx
else idx
-(* Note: "charlen" stands for either strlen or wcslen *)
+(* -------------------------------------------------------------------------- *)
+(* --- Inlining of defined logic functions and predicates --- *)
+(* -------------------------------------------------------------------------- *)
-(* Applies a cvalue [builtin] to the list of arguments [args_list] in the
- current state of [env]. Returns [v, alarms], where [v] is the resulting
- cvalue, which can be bottom. *)
-let apply_logic_builtin builtin env args_list =
- (* the call below could in theory return Builtins.Invalid_nb_of_args,
- but logic typing constraints prevent that. *)
- builtin (env_current_state env) args_list
-
-(* Never raises exceptions; instead, returns [-1,+oo] in case of alarms
- (most imprecise result possible for the logic strlen/wcslen predicates). *)
-let eval_logic_charlen wrapper env v ldeps =
- let eover =
- let v, alarms = apply_logic_builtin wrapper env [v] in
- if alarms && not (Cvalue.V.is_bottom v)
- then Cvalue.V.inject_ival (Ival.inject_range (Some Int.minus_one) None)
- else v
- in
- let eunder = under_from_over eover in
- (* the C strlen function has type size_t, but the logic strlen function has
- type ℤ (signed) *)
- let etype = Cil.intType in
- { etype; ldeps; eover; empty = false; eunder }
-
-(* Evaluates the logical predicates strchr/wcschr. *)
-let eval_logic_charchr builtin env s c ldeps_s ldeps_c =
- let eover =
- let v, alarms = apply_logic_builtin builtin env [s; c] in
- if Cvalue.V.is_bottom v then v else
- if alarms then Cvalue.V.zero_or_one else
- let ctrue = Cvalue.V.contains_non_zero v
- and cfalse = Cvalue.V.contains_zero v in
- match ctrue, cfalse with
- | true, true -> Cvalue.V.zero_or_one
- | true, false -> Cvalue.V.singleton_one
- | false, true -> Cvalue.V.singleton_zero
- | false, false -> assert false (* a logic alarm would have been raised*)
- in
- let eunder = under_from_over eover in
- (* the C strchr function has type char*, but the logic strchr predicate has
- type 𔹠*)
- let etype = TInt (IBool, []) in
- let ldeps = join_logic_deps ldeps_s ldeps_c in
- { etype; ldeps; eover; empty = false; eunder }
-
-(* Evaluates the logical functions memchr_off/wmemchr_off. *)
-let eval_logic_memchr_off builtin env s c n =
- let minus_one = Cvalue.V.inject_int Integer.minus_one in
- let positive = Cvalue.V.inject_ival Ival.positive_integers in
- let pred_n = Cvalue.V.add_untyped Int_Base.one n.eover minus_one in
- let n_pos = Cvalue.V.narrow positive pred_n in
- let eover =
- if Cvalue.V.is_bottom n_pos then minus_one else
- let args = [s.eover; c.eover; n_pos] in
- let v, alarms = apply_logic_builtin builtin env args in
- if Cvalue.V.is_bottom v then pred_n else
- if alarms then Cvalue.V.join pred_n v else
- if Cvalue.V.equal n_pos pred_n then v else
- Cvalue.V.join minus_one v
- in
- let ldeps = join_logic_deps s.ldeps (join_logic_deps c.ldeps n.ldeps) in
- { (einteger eover) with ldeps }
-
-(* Evaluates the logical predicate is_allocable, according to the following
- logic:
- - if the size to allocate is always too large (> SIZE_MAX), allocation fails;
- - otherwise, if AllocReturnsNull is true or if the size may exceed SIZE_MAX,
- returns Unknown (to simulate non-determinism);
- - otherwise, allocation always succeeds. *)
-let eval_is_allocable size =
- let size_ok = Builtins_malloc.alloc_size_ok size in
- match size_ok, Value_parameters.AllocReturnsNull.get () with
- | Alarmset.False, _ -> False
- | Alarmset.Unknown, _ | _, true -> Unknown
- | Alarmset.True, false -> True
-
-(* returns true iff the logic variable is defined by the
- Frama-C standard library *)
-let comes_from_fc_stdlib lvar =
- Cil.is_in_libc lvar.lv_attr ||
- match lvar.lv_origin with
- | None -> false
- | Some vi ->
- Cil.is_in_libc vi.vattr
-
-(* As usual in this file, [dst_typ] may be misleading: the 'size' is
- meaningless, because [src_typ] may actually be a logic type. Thus,
- this size must not be used below. *)
-let cast ~src_typ ~dst_typ v =
- let open Eval_typ in
- match classify_as_scalar dst_typ, classify_as_scalar src_typ with
- | None, _ | _, None -> v (* unclear whether this happens. *)
- | Some dst, Some src ->
- match dst, src with
- | TSFloat fkind, (TSInt _ | TSPtr _) ->
- Cvalue.V.cast_int_to_float (Fval.kind fkind) v
-
- | (TSInt dst | TSPtr dst), TSFloat fkind ->
- (* This operation is not fully defined in ACSL. We raise an alarm
- in case of overflow. *)
- if is_true (Cvalue_forward.assume_not_nan ~assume_finite:true fkind v)
- then Cvalue_forward.cast_float_to_int dst v
- else c_alarm ()
-
- | (TSInt dst | TSPtr dst), (TSInt _ | TSPtr _) ->
- let size = Integer.of_int dst.i_bits in
- let signed = dst.i_signed in
- V.cast_int_to_int ~signed ~size v
-
- | TSFloat fkind, TSFloat _ ->
- Cvalue.V.cast_float_to_float (Fval.kind fkind) v
-
-(* V.cast_int_to_int is unsound when the destination type is _Bool.
- Use this function instead. *)
-let cast_to_bool r =
- let contains_zero = V.contains_zero r.eover
- and contains_non_zero = V.contains_non_zero r.eover in
- let eover = V.interp_boolean ~contains_zero ~contains_non_zero in
- { eover; eunder = under_from_over eover; empty = r.empty;
- ldeps = r.ldeps; etype = TInt (IBool, []) }
-
-(* -------------------------------------------------------------------------- *)
-(* --- Inlining of defined logic functions and predicates --- *)
-(* -------------------------------------------------------------------------- *)
-
-type pred_fun_origin = ACSL | Libc
+type pred_fun_origin = ACSL | Libc
let known_logic_funs = [
"strlen", Libc;
@@ -777,18 +710,266 @@ let inline logic_info =
let logic_var = logic_info.l_var_info in
not (is_known_logic_fun logic_var || is_known_predicate logic_var)
-(* We evaluate the ACSL sign type as integers 1 or -1. Sign values can only be
- constructed through the \sign function (handled in eval_known_logic_function)
- and the \Positive and \Negative constructors (handled in eval_term). They can
- only be compared through equality and disequality; no other operation exists
- on this type, so our interpretation remains correct. *)
-let positive_cvalue = Cvalue.V.inject_int Int.one
-let negative_cvalue = Cvalue.V.inject_int Int.minus_one
+(* -------------------------------------------------------------------------- *)
+(* --- Auxiliary evaluation functions --- *)
+(* -------------------------------------------------------------------------- *)
+
+(* We evaluate the ACSL sign type as integers 1 or -1. Sign values can only be
+ constructed through the \sign function (handled in eval_known_logic_function)
+ and the \Positive and \Negative constructors (handled in eval_term). They can
+ only be compared through equality and disequality; no other operation exists
+ on this type, so our interpretation remains correct. *)
+let positive_cvalue = Cvalue.V.inject_int Integer.one
+let negative_cvalue = Cvalue.V.inject_int Integer.minus_one
+
+let is_true = function
+ | `True | `TrueReduced _ -> true
+ | `Unknown _ | `False | `Unreachable -> false
+
+(* Check "logic alarms" when evaluating [v1 op v2]. All operators shifts are
+ defined unambiguously in ACSL. *)
+let check_logic_alarms ~alarm_mode typ (_v1: V.t eval_result) op v2 =
+ match op with
+ | Div | Mod when Cil.isIntegralOrPointerType typ ->
+ let truth = Cvalue_forward.assume_non_zero v2.eover in
+ let division_by_zero = not (is_true truth) in
+ track_alarms division_by_zero alarm_mode
+ | Shiftlt | Shiftrt -> begin
+ (* Check that [e2] is positive. [e1] can be arbitrary, we use
+ the arithmetic vision of shifts *)
+ try
+ let i2 = Cvalue.V.project_ival_bottom v2.eover in
+ let valid = Ival.is_included i2 Ival.positive_integers in
+ track_alarms (not valid) alarm_mode
+ with Cvalue.V.Not_based_on_null -> track_alarms true alarm_mode
+ end
+ | _ -> ()
+
+(* As usual in this file, [dst_typ] may be misleading: the 'size' is
+ meaningless, because [src_typ] may actually be a logic type. Thus,
+ this size must not be used below. *)
+let cast ~src_typ ~dst_typ v =
+ let open Eval_typ in
+ match classify_as_scalar dst_typ, classify_as_scalar src_typ with
+ | None, _ | _, None -> v (* unclear whether this happens. *)
+ | Some dst, Some src ->
+ match dst, src with
+ | TSFloat fkind, (TSInt _ | TSPtr _) ->
+ Cvalue.V.cast_int_to_float (Fval.kind fkind) v
+
+ | (TSInt dst | TSPtr dst), TSFloat fkind ->
+ (* This operation is not fully defined in ACSL. We raise an alarm
+ in case of overflow. *)
+ if is_true (Cvalue_forward.assume_not_nan ~assume_finite:true fkind v)
+ then Cvalue_forward.cast_float_to_int dst v
+ else c_alarm ()
+
+ | (TSInt dst | TSPtr dst), (TSInt _ | TSPtr _) ->
+ let size = Integer.of_int dst.i_bits in
+ let signed = dst.i_signed in
+ V.cast_int_to_int ~signed ~size v
+
+ | TSFloat fkind, TSFloat _ ->
+ Cvalue.V.cast_float_to_float (Fval.kind fkind) v
+
+(* V.cast_int_to_int is unsound when the destination type is _Bool.
+ Use this function instead. *)
+let cast_to_bool r =
+ let contains_zero = V.contains_zero r.eover
+ and contains_non_zero = V.contains_non_zero r.eover in
+ let eover = V.interp_boolean ~contains_zero ~contains_non_zero in
+ { eover; eunder = under_from_over eover; empty = r.empty;
+ ldeps = r.ldeps; etype = TInt (IBool, []) }
+
+(* Note: "charlen" stands for either strlen or wcslen *)
+
+(* Applies a cvalue [builtin] to the list of arguments [args_list] in the
+ current state of [env]. Returns [v, alarms], where [v] is the resulting
+ cvalue, which can be bottom. *)
+let apply_logic_builtin builtin env args_list =
+ (* the call below could in theory return Builtins.Invalid_nb_of_args,
+ but logic typing constraints prevent that. *)
+ builtin (env_current_state env) args_list
+
+(* Never raises exceptions; instead, returns [-1,+oo] in case of alarms
+ (most imprecise result possible for the logic strlen/wcslen predicates). *)
+let eval_logic_charlen wrapper env v ldeps =
+ let eover =
+ let v, alarms = apply_logic_builtin wrapper env [v] in
+ if alarms && not (Cvalue.V.is_bottom v)
+ then Cvalue.V.inject_ival (Ival.inject_range (Some Integer.minus_one) None)
+ else v
+ in
+ let eunder = under_from_over eover in
+ (* the C strlen function has type size_t, but the logic strlen function has
+ type ℤ (signed) *)
+ let etype = Cil.intType in
+ { etype; ldeps; eover; empty = false; eunder }
+
+(* Evaluates the logical predicates strchr/wcschr. *)
+let eval_logic_charchr builtin env s c ldeps_s ldeps_c =
+ let eover =
+ let v, alarms = apply_logic_builtin builtin env [s; c] in
+ if Cvalue.V.is_bottom v then v else
+ if alarms then Cvalue.V.zero_or_one else
+ let ctrue = Cvalue.V.contains_non_zero v
+ and cfalse = Cvalue.V.contains_zero v in
+ match ctrue, cfalse with
+ | true, true -> Cvalue.V.zero_or_one
+ | true, false -> Cvalue.V.singleton_one
+ | false, true -> Cvalue.V.singleton_zero
+ | false, false -> assert false (* a logic alarm would have been raised*)
+ in
+ let eunder = under_from_over eover in
+ (* the C strchr function has type char*, but the logic strchr predicate has
+ type 𔹠*)
+ let etype = TInt (IBool, []) in
+ let ldeps = join_logic_deps ldeps_s ldeps_c in
+ { etype; ldeps; eover; empty = false; eunder }
+
+(* Evaluates the logical functions memchr_off/wmemchr_off. *)
+let eval_logic_memchr_off builtin env s c n =
+ let minus_one = Cvalue.V.inject_int Integer.minus_one in
+ let positive = Cvalue.V.inject_ival Ival.positive_integers in
+ let pred_n = Cvalue.V.add_untyped Int_Base.one n.eover minus_one in
+ let n_pos = Cvalue.V.narrow positive pred_n in
+ let eover =
+ if Cvalue.V.is_bottom n_pos then minus_one else
+ let args = [s.eover; c.eover; n_pos] in
+ let v, alarms = apply_logic_builtin builtin env args in
+ if Cvalue.V.is_bottom v then pred_n else
+ if alarms then Cvalue.V.join pred_n v else
+ if Cvalue.V.equal n_pos pred_n then v else
+ Cvalue.V.join minus_one v
+ in
+ let ldeps = join_logic_deps s.ldeps (join_logic_deps c.ldeps n.ldeps) in
+ { (einteger eover) with ldeps }
+
+(* Evaluates the logical predicate is_allocable, according to the following
+ logic:
+ - if the size to allocate is always too large (> SIZE_MAX), allocation fails;
+ - otherwise, if AllocReturnsNull is true or if the size may exceed SIZE_MAX,
+ returns Unknown (to simulate non-determinism);
+ - otherwise, allocation always succeeds. *)
+let eval_is_allocable size =
+ let size_ok = Builtins_malloc.alloc_size_ok size in
+ match size_ok, Value_parameters.AllocReturnsNull.get () with
+ | Alarmset.False, _ -> False
+ | Alarmset.Unknown, _ | _, true -> Unknown
+ | Alarmset.True, false -> True
+
+(* Evaluates a [valid_read_string] or [valid_read_wstring] predicate
+ using str* builtins.
+ - if [bottom] is obtained, return False;
+ - otherwise, if no alarms are emitted, return True;
+ - otherwise, return [Unknown]. *)
+let eval_valid_read_str ~wide env v =
+ let wrapper =
+ if wide then Builtins_string.frama_c_wcslen_wrapper
+ else Builtins_string.frama_c_strlen_wrapper
+ in
+ let v, alarms = apply_logic_builtin wrapper env [v] in
+ if Cvalue.V.is_bottom v
+ then False (* bottom state => string always invalid *)
+ else if alarms
+ then Unknown (* alarm => string possibly invalid *)
+ else True (* no alarm => string always valid for reading *)
+
+(* Evaluates a [valid_string] or [valid_wstring] predicate.
+ First, we check the constness of the arguments.
+ Then, we evaluate [valid_read_string/valid_read_wstring] on non-const ones. *)
+let eval_valid_str ~wide env v =
+ assert (not (Cvalue.V.is_bottom v));
+ (* filter const bases *)
+ let v' = Cvalue.V.filter_base (fun b -> not (Base.is_read_only b)) v in
+ if Cvalue.V.is_bottom v' then False (* all bases were const *)
+ else
+ if Cvalue.V.equal v v' then
+ eval_valid_read_str ~wide env v (* all bases non-const *)
+ else (* at least one base was const *)
+ match eval_valid_read_str ~wide env v with
+ | True -> Unknown (* weaken result *)
+ | False | Unknown as r -> r
+
+(* Do all the possible values of a location in [state] satisfy [test]? [loc] is
+ an over-approximation of the location, so the answer cannot be [False] even
+ if some parts of [loc] do not satisfy [test]. Thus, this function does not
+ fold the location, but instead applies [test] to the join of all values
+ stored in [loc] in [state]. *)
+let forall_in_over_location state loc test =
+ let v = Model.find_indeterminate state loc in
+ test v
+
+(* Do all the possible values of a location in [state] satisfy [test]? [loc] is
+ an under-approximation of the location, so the answer cannot be [True], as
+ the values of some other parts of the location may not satisfy [test].
+ However, it is [False] as soon as some part of [loc] contradicts [test]. *)
+let forall_in_under_location state loc test =
+ let exception EFalse in
+ let inspect_value (_, _) (value, _, _) acc =
+ match test value with
+ | True | Unknown -> acc
+ | False -> raise EFalse
+ in
+ let inspect_itv base itv acc =
+ match Cvalue.Model.find_base_or_default base state with
+ | `Top | `Bottom -> Unknown
+ | `Value offsm ->
+ Cvalue.V_Offsetmap.fold_between ~entire:true itv inspect_value offsm acc
+ in
+ let inspect_base base intervals acc =
+ Int_Intervals.fold (inspect_itv base) intervals acc
+ in
+ let zone = Locations.enumerate_bits loc in
+ try Zone.fold_i inspect_base zone Unknown
+ with EFalse -> False
+ | Abstract_interp.Error_Top -> Unknown
+
+(* Evaluates an universal predicate about the values of a location evaluated to
+ [r] in [state]. The predicates holds whenever all the possible values at the
+ location satisfy [test]. *)
+let eval_forall_predicate state r test =
+ let size_bits = Eval_typ.sizeof_lval_typ r.etype in
+ let make_loc loc = make_loc loc size_bits in
+ let over_loc = make_loc r.eover in
+ if not Locations.(is_valid Read over_loc) then c_alarm ();
+ match forall_in_over_location state over_loc test with
+ | Unknown ->
+ let under_loc = make_loc r.eunder in
+ forall_in_under_location state under_loc test
+ | True -> True
+ | False -> if r.empty then Unknown else False
+
+(* Evaluation of an \initialized predicate on a location evaluated to [r]
+ in the state [state]. *)
+let eval_initialized state r =
+ let test = function
+ | V_Or_Uninitialized.C_init_esc _
+ | V_Or_Uninitialized.C_init_noesc _ -> True
+ | V_Or_Uninitialized.C_uninit_esc _ -> Unknown
+ | V_Or_Uninitialized.C_uninit_noesc v ->
+ if Location_Bytes.is_bottom v then False else Unknown
+ in
+ eval_forall_predicate state r test
+
+(* Evaluation of a \dangling predicate on a location evaluated to [r]
+ in the state [state]. *)
+let eval_dangling state r =
+ let test = function
+ | V_Or_Uninitialized.C_init_esc v ->
+ if Location_Bytes.is_bottom v then True else Unknown
+ | V_Or_Uninitialized.C_uninit_esc _ -> Unknown
+ | V_Or_Uninitialized.C_init_noesc _
+ | V_Or_Uninitialized.C_uninit_noesc _ -> False
+ in
+ eval_forall_predicate state r test
(* -------------------------------------------------------------------------- *)
(* --- Evaluation of terms --- *)
(* -------------------------------------------------------------------------- *)
+exception Reduce_to_bottom
+
let int_or_float_op typ int_op float_op =
match typ with
| TInt _ | TPtr _ | TEnum _ -> int_op
@@ -1070,11 +1251,11 @@ let rec eval_term ~alarm_mode env t =
frontiers are always 0 or 8*k-1 (because validity is in bits and
starts on zero), so we add 1 everywhere, then divide by eight. *)
let convert start_bits end_bits =
- let congr_succ i = Int.(equal zero (e_rem (succ i) eight)) in
- let congr_or_zero i = Int.(equal zero i || congr_succ i) in
+ let congr_succ i = Integer.(equal zero (e_rem (succ i) eight)) in
+ let congr_or_zero i = Integer.(equal zero i || congr_succ i) in
assert (congr_or_zero start_bits || congr_or_zero end_bits);
- let start_bytes = Int.(e_div (Int.succ start_bits) eight) in
- let end_bytes = Int.(e_div (Int.succ end_bits) eight) in
+ let start_bytes = Integer.(e_div (Integer.succ start_bits) eight) in
+ let end_bytes = Integer.(e_div (Integer.succ end_bits) eight) in
Ival.inject_range (Some start_bytes) (Some end_bytes)
in
match Base.validity b with
@@ -1120,11 +1301,19 @@ let rec eval_term ~alarm_mode env t =
| _ -> unsupported "logic inductive types"
end
+ | Tcomprehension (term, quantifiers, predicate) ->
+ let env = bind_comprehension_quantifiers env quantifiers predicate in
+ let r = eval_term ~alarm_mode env term in
+ let pred_deps = Option.bind predicate (predicate_deps env) in
+ let ldeps =
+ Option.fold ~none:r.ldeps ~some:(join_logic_deps r.ldeps) pred_deps
+ in
+ { r with empty = true; ldeps }
+
| Tlambda _ -> unsupported "logic functions or predicates"
| TUpdate _ -> unsupported "functional updates"
| Ttype _ -> unsupported "\\type operator"
| Ttypeof _ -> unsupported "\\typeof operator"
- | Tcomprehension _ -> unsupported "sets defined by comprehension"
| Tinter _ -> unsupported "set intersection"
| Tlet _ -> unsupported "\\let bindings"
| TConst (LStr _) -> unsupported "constant strings"
@@ -1170,149 +1359,6 @@ and eval_binop ~alarm_mode env op t1 t2 =
ldeps = join_logic_deps r1.ldeps r2.ldeps;
eunder; eover; empty = r1.empty || r2.empty; }
-and eval_tlhost ~alarm_mode env lv =
- match lv with
- | TVar lvar ->
- let base, typ =
- match lvar.lv_origin, Logic_utils.unroll_type lvar.lv_type with
- | Some v, _ -> Base.of_varinfo v, v.vtype
- | None, Ctype typ -> Base.of_c_logic_var lvar, typ
- | _ -> unsupported_lvar lvar
- in
- let loc = Location_Bits.inject base Ival.zero in
- { etype = typ;
- ldeps = empty_logic_deps;
- eover = loc;
- eunder = under_loc_from_over loc;
- empty = false; }
- | TResult typ ->
- (match env.result with
- | Some v ->
- let loc = Location_Bits.inject (Base.of_varinfo v) Ival.zero in
- { etype = typ;
- ldeps = empty_logic_deps;
- eunder = loc; eover = loc;
- empty = false; }
- | None -> no_result ())
- | TMem t ->
- let r = eval_term ~alarm_mode env t in
- let tres = match Cil.unrollType r.etype with
- | TPtr (t, _) -> t
- | _ -> ast_error "*p where p is not a pointer"
- in
- { etype = tres;
- ldeps = r.ldeps;
- eunder = loc_bytes_to_loc_bits r.eunder;
- eover = loc_bytes_to_loc_bits r.eover;
- empty = r.empty; }
-
-and eval_toffset ~alarm_mode env typ toffset =
- match toffset with
- | TNoOffset ->
- { etype = typ;
- ldeps = empty_logic_deps;
- eunder = Ival.zero;
- eover = Ival.zero;
- empty = false; }
- | TIndex (idx, remaining) ->
- let typ_e, size = match Cil.unrollType typ with
- | TArray (t, size, _, _) -> t, size
- | _ -> ast_error "index on a non-array"
- in
- let idx = constraint_trange idx size in
- let idxs = eval_term ~alarm_mode env idx in
- let offsrem = eval_toffset ~alarm_mode env typ_e remaining in
- let size_e = Bit_utils.sizeof typ_e in
- let eover =
- let offset =
- try Cvalue.V.project_ival_bottom idxs.eover
- with Cvalue.V.Not_based_on_null -> Ival.top
- in
- let offset = Ival.scale_int_base size_e offset in
- Ival.add_int offset offsrem.eover
- in
- let eunder =
- let offset =
- try Cvalue.V.project_ival idxs.eunder
- with Cvalue.V.Not_based_on_null -> Ival.bottom
- in
- let offset = match size_e with
- | Int_Base.Top -> Ival.bottom
- (* Note: scale_int_base would overapproximate when given a
- Float. Should never happen. *)
- | Int_Base.Value f ->
- assert (Ival.is_int offset);
- Ival.scale f offset
- in
- Ival.add_int_under offset offsrem.eunder
- in
- { etype = offsrem.etype;
- ldeps = join_logic_deps idxs.ldeps offsrem.ldeps;
- eunder; eover; empty = idxs.empty || offsrem.empty; }
-
- | TField (fi, remaining) ->
- let size_current default =
- try Ival.of_int (fst (Cil.fieldBitsOffset fi))
- with Cil.SizeOfError _ -> default
- in
- let attrs = Cil.filter_qualifier_attributes (Cil.typeAttrs typ) in
- let typ_fi = Cil.typeAddAttributes attrs fi.ftype in
- let offsrem = eval_toffset ~alarm_mode env typ_fi remaining in
- { etype = offsrem.etype;
- ldeps = offsrem.ldeps;
- eover = Ival.add_int (size_current Ival.top) offsrem.eover;
- eunder = Ival.add_int_under (size_current Ival.bottom) offsrem.eunder;
- empty = offsrem.empty; }
-
- | TModel _ -> unsupported "model fields"
-
-and eval_tlval ~alarm_mode env (thost, toffs) =
- let rhost = eval_tlhost ~alarm_mode env thost in
- let roffset = eval_toffset ~alarm_mode env rhost.etype toffs in
- { etype = roffset.etype;
- ldeps = join_logic_deps rhost.ldeps roffset.ldeps;
- eunder = Location_Bits.shift_under roffset.eunder rhost.eunder;
- eover = Location_Bits.shift roffset.eover rhost.eover;
- empty = rhost.empty || roffset.empty;
- }
-
-and eval_term_as_lval ~alarm_mode env t =
- match t.term_node with
- | TLval tlval ->
- eval_tlval ~alarm_mode env tlval
- | Tunion l ->
- let eunder, eover, deps, empty = List.fold_left
- (fun (accunder, accover, accdeps, accempty) t ->
- let r = eval_term_as_lval ~alarm_mode env t in
- Location_Bits.link accunder r.eunder,
- Location_Bits.join accover r.eover,
- join_logic_deps accdeps r.ldeps,
- accempty || r.empty
- ) (Location_Bits.top, Location_Bits.bottom, empty_logic_deps, false) l
- in
- { etype = infer_type t.term_type;
- ldeps = deps;
- eover; eunder; empty }
- | Tempty_set ->
- { etype = infer_type t.term_type;
- ldeps = empty_logic_deps;
- eunder = Location_Bits.bottom;
- eover = Location_Bits.bottom;
- empty = true }
- | Tat (t, lab) ->
- ignore (env_state env lab);
- eval_term_as_lval ~alarm_mode { env with e_cur = lab } t
- | TLogic_coerce (_lt, t) ->
- (* Logic coerce on locations (that are pointers) can only introduce
- sets, that do not change the abstract value. *)
- eval_term_as_lval ~alarm_mode env t
- | Tif (tcond, ttrue, tfalse) ->
- eval_tif eval_term_as_lval Location_Bits.join Location_Bits.meet ~alarm_mode env
- tcond ttrue tfalse
- | Tinter _ -> unsupported "intersection of locations"
- | Tcomprehension _ -> unsupported "set comprehension"
- | _ -> ast_error (Format.asprintf "non-lval term %a" Printer.pp_term t)
-
and eval_tif : 'a. (alarm_mode:_ -> _ -> _ -> 'a eval_result) -> ('a -> 'a -> 'a) -> ('a -> 'a -> 'a) -> alarm_mode:_ -> _ -> _ -> _ -> _ -> 'a eval_result =
fun eval join meet ~alarm_mode env tcond ttrue tfalse ->
let r = eval_term ~alarm_mode env tcond in
@@ -1405,7 +1451,8 @@ and eval_known_logic_function ~alarm_mode env li labels args =
| ("\\min" | "\\max"), Some typ, _, t1 :: t2 :: tail_args ->
begin
- let comp = if lvi.lv_name = "\\min" then Comp.Le else Comp.Ge in
+ let min = lvi.lv_name = "\\min" in
+ let comp = Abstract_interp.Comp.(if min then Le else Ge) in
let backward =
match typ with
| Linteger -> Cvalue.V.backward_comp_int_left comp
@@ -1560,62 +1607,178 @@ and eval_quantifier_extremum backward_left ~min ~max eval_term =
let r = eval_term (Cvalue.V.join min.eover max.eover) in
return { r with eover = Cvalue.V.top; eunder = Cvalue.V.bottom }
-let eval_tlval_as_location ~alarm_mode env t =
- let r = eval_term_as_lval ~alarm_mode env t in
- let s = Eval_typ.sizeof_lval_typ r.etype in
- make_loc r.eover s
+(* Introduces the logic variables [quantifiers] in [env], and reduces their
+ value according to [predicate]. *)
+and bind_comprehension_quantifiers env quantifiers predicate =
+ let env = bind_logic_vars env quantifiers in
+ match predicate with
+ | None -> env
+ | Some pred ->
+ try
+ let alarm_mode = Fail in
+ let reduced_env = reduce_by_predicate ~alarm_mode env true pred in
+ copy_logic_vars ~src:reduced_env ~dst:env quantifiers
+ with LogicEvalError error ->
+ display_evaluation_error ~loc:pred.pred_loc error;
+ env
-(* Return a pair of (under-approximating, over-approximating) zones. *)
-let eval_tlval_as_zone_under_over ~alarm_mode access env t =
- let r = eval_term_as_lval ~alarm_mode env t in
- let s = Eval_typ.sizeof_lval_typ r.etype in
- let under = enumerate_valid_bits_under access (make_loc r.eunder s) in
- let over = enumerate_valid_bits access (make_loc r.eover s) in
- (under, over)
+(* -------------------------------------------------------------------------- *)
+(* --- Evaluation of term lval and of terms as location --- *)
+(* -------------------------------------------------------------------------- *)
-let eval_tlval_as_zone ~alarm_mode access env t =
- let _under, over =
- eval_tlval_as_zone_under_over ~alarm_mode access env t
- in
- over
+and eval_tlhost ~alarm_mode env lv =
+ match lv with
+ | TVar lvar ->
+ let base, typ =
+ match lvar.lv_origin, Logic_utils.unroll_type lvar.lv_type with
+ | Some v, _ -> Base.of_varinfo v, v.vtype
+ | None, Ctype typ -> Base.of_c_logic_var lvar, typ
+ | _ -> unsupported_lvar lvar
+ in
+ let loc = Location_Bits.inject base Ival.zero in
+ { etype = typ;
+ ldeps = empty_logic_deps;
+ eover = loc;
+ eunder = under_loc_from_over loc;
+ empty = false; }
+ | TResult typ ->
+ (match env.result with
+ | Some v ->
+ let loc = Location_Bits.inject (Base.of_varinfo v) Ival.zero in
+ { etype = typ;
+ ldeps = empty_logic_deps;
+ eunder = loc; eover = loc;
+ empty = false; }
+ | None -> no_result ())
+ | TMem t ->
+ let r = eval_term ~alarm_mode env t in
+ let tres = match Cil.unrollType r.etype with
+ | TPtr (t, _) -> t
+ | _ -> ast_error "*p where p is not a pointer"
+ in
+ { etype = tres;
+ ldeps = r.ldeps;
+ eunder = loc_bytes_to_loc_bits r.eunder;
+ eover = loc_bytes_to_loc_bits r.eover;
+ empty = r.empty; }
-(* If casting [trm] to [typ] has no effect in terms of the values contained
- in [trm], do nothing. Otherwise, raise [exn]. Adapted from [pass_cast] *)
-let pass_logic_cast exn typ trm =
- match Logic_utils.unroll_type typ, Logic_utils.unroll_type trm.term_type with
- | Linteger, Ctype (TInt _ | TEnum _) -> () (* Always inclusion *)
- | Ctype (TInt _ | TEnum _ as typ), Ctype (TInt _ | TEnum _ as typeoftrm) ->
- let sztyp = sizeof typ in
- let szexpr = sizeof typeoftrm in
- let styp, sexpr =
- match sztyp, szexpr with
- | Int_Base.Value styp, Int_Base.Value sexpr -> styp, sexpr
- | _ -> raise exn
+and eval_toffset ~alarm_mode env typ toffset =
+ match toffset with
+ | TNoOffset ->
+ { etype = typ;
+ ldeps = empty_logic_deps;
+ eunder = Ival.zero;
+ eover = Ival.zero;
+ empty = false; }
+ | TIndex (idx, remaining) ->
+ let typ_e, size = match Cil.unrollType typ with
+ | TArray (t, size, _, _) -> t, size
+ | _ -> ast_error "index on a non-array"
+ in
+ let idx = constraint_trange idx size in
+ let idxs = eval_term ~alarm_mode env idx in
+ let offsrem = eval_toffset ~alarm_mode env typ_e remaining in
+ let size_e = Bit_utils.sizeof typ_e in
+ let eover =
+ let offset =
+ try Cvalue.V.project_ival_bottom idxs.eover
+ with Cvalue.V.Not_based_on_null -> Ival.top
+ in
+ let offset = Ival.scale_int_base size_e offset in
+ Ival.add_int offset offsrem.eover
in
- let sityp = is_signed_int_enum_pointer typ in
- let sisexpr = is_signed_int_enum_pointer typeoftrm in
- if (Int.ge styp sexpr && sityp = sisexpr) (* larger, same signedness *)
- || (Int.gt styp sexpr && sityp) (* strictly larger and signed *)
- then ()
- else raise exn
-
- | Lreal, Ctype (TFloat _) -> () (* Always inclusion *)
- | Ctype (TFloat (f1,_)), Ctype (TFloat (f2, _)) ->
- if Cil.frank f1 < Cil.frank f2
- then raise exn
+ let eunder =
+ let offset =
+ try Cvalue.V.project_ival idxs.eunder
+ with Cvalue.V.Not_based_on_null -> Ival.bottom
+ in
+ let offset = match size_e with
+ | Int_Base.Top -> Ival.bottom
+ (* Note: scale_int_base would overapproximate when given a
+ Float. Should never happen. *)
+ | Int_Base.Value f ->
+ assert (Ival.is_int offset);
+ Ival.scale f offset
+ in
+ Ival.add_int_under offset offsrem.eunder
+ in
+ { etype = offsrem.etype;
+ ldeps = join_logic_deps idxs.ldeps offsrem.ldeps;
+ eunder; eover; empty = idxs.empty || offsrem.empty; }
- | _ -> raise exn (* Not a scalar type *)
+ | TField (fi, remaining) ->
+ let size_current default =
+ try Ival.of_int (fst (Cil.fieldBitsOffset fi))
+ with Cil.SizeOfError _ -> default
+ in
+ let attrs = Cil.filter_qualifier_attributes (Cil.typeAttrs typ) in
+ let typ_fi = Cil.typeAddAttributes attrs fi.ftype in
+ let offsrem = eval_toffset ~alarm_mode env typ_fi remaining in
+ { etype = offsrem.etype;
+ ldeps = offsrem.ldeps;
+ eover = Ival.add_int (size_current Ival.top) offsrem.eover;
+ eunder = Ival.add_int_under (size_current Ival.bottom) offsrem.eunder;
+ empty = offsrem.empty; }
+ | TModel _ -> unsupported "model fields"
-exception Not_an_exact_loc
+and eval_tlval ~alarm_mode env (thost, toffs) =
+ let rhost = eval_tlhost ~alarm_mode env thost in
+ let roffset = eval_toffset ~alarm_mode env rhost.etype toffs in
+ { etype = roffset.etype;
+ ldeps = join_logic_deps rhost.ldeps roffset.ldeps;
+ eunder = Location_Bits.shift_under roffset.eunder rhost.eunder;
+ eover = Location_Bits.shift roffset.eover rhost.eover;
+ empty = rhost.empty || roffset.empty;
+ }
-type exact_location =
- | Location of typ * Locations.location
- | Logic_var of logic_var
+and eval_term_as_lval ~alarm_mode env t =
+ match t.term_node with
+ | TLval tlval ->
+ eval_tlval ~alarm_mode env tlval
+ | Tunion l ->
+ let eunder, eover, deps, empty = List.fold_left
+ (fun (accunder, accover, accdeps, accempty) t ->
+ let r = eval_term_as_lval ~alarm_mode env t in
+ Location_Bits.link accunder r.eunder,
+ Location_Bits.join accover r.eover,
+ join_logic_deps accdeps r.ldeps,
+ accempty || r.empty
+ ) (Location_Bits.top, Location_Bits.bottom, empty_logic_deps, false) l
+ in
+ { etype = infer_type t.term_type;
+ ldeps = deps;
+ eover; eunder; empty }
+ | Tempty_set ->
+ { etype = infer_type t.term_type;
+ ldeps = empty_logic_deps;
+ eunder = Location_Bits.bottom;
+ eover = Location_Bits.bottom;
+ empty = true }
+ | Tat (t, lab) ->
+ ignore (env_state env lab);
+ eval_term_as_lval ~alarm_mode { env with e_cur = lab } t
+ | TLogic_coerce (_lt, t) ->
+ (* Logic coerce on locations (that are pointers) can only introduce
+ sets, that do not change the abstract value. *)
+ eval_term_as_lval ~alarm_mode env t
+ | Tif (tcond, ttrue, tfalse) ->
+ eval_tif eval_term_as_lval Location_Bits.join Location_Bits.meet ~alarm_mode env
+ tcond ttrue tfalse
+ | Tcomprehension (term, quantifiers, predicate) ->
+ let env = bind_comprehension_quantifiers env quantifiers predicate in
+ let r = eval_term_as_lval ~alarm_mode env term in
+ let pred_deps = Option.bind predicate (predicate_deps env) in
+ let ldeps =
+ Option.fold ~none:r.ldeps ~some:(join_logic_deps r.ldeps) pred_deps
+ in
+ { r with empty = true; ldeps }
+ | Tinter _ -> unsupported "intersection of locations"
+ | _ -> ast_error (Format.asprintf "non-lval term %a" Printer.pp_term t)
(* Evaluate a term as a non-empty under-approximated location, or raise
[Not_an_exact_loc]. *)
-let rec eval_term_as_exact_locs ~alarm_mode env t =
+and eval_term_as_exact_locs ~alarm_mode env t =
match t.term_node with
| TLval (TVar ({ lv_type = Linteger | Lreal } as logic_var), TNoOffset) ->
Logic_var logic_var
@@ -1667,153 +1830,18 @@ let rec eval_term_as_exact_locs ~alarm_mode env t =
| Tunion [t] ->
eval_term_as_exact_locs ~alarm_mode env t
- | _ -> raise Not_an_exact_loc
+ | Tcomprehension (term, quantifiers, predicate) ->
+ let env = bind_comprehension_quantifiers env quantifiers predicate in
+ eval_term_as_exact_locs ~alarm_mode env term
+ | _ -> raise Not_an_exact_loc
(* -------------------------------------------------------------------------- *)
-(* --- Evaluation and reduction by predicates --- *)
+(* --- Reduction by predicates --- *)
(* -------------------------------------------------------------------------- *)
-(** Auxiliary functions *)
-
-let is_same_term_coerce t1 t2 =
- match t1.term_node, t2.term_node with
- | TLogic_coerce _, TLogic_coerce _ -> Logic_utils.is_same_term t1 t2
- | TLogic_coerce (_,t1), _ -> Logic_utils.is_same_term t1 t2
- | _, TLogic_coerce(_,t2) -> Logic_utils.is_same_term t1 t2
- | _ -> Logic_utils.is_same_term t1 t2
-
-
-(* Evaluates a [valid_read_string] or [valid_read_wstring] predicate
- using str* builtins.
- - if [bottom] is obtained, return False;
- - otherwise, if no alarms are emitted, return True;
- - otherwise, return [Unknown]. *)
-let eval_valid_read_str ~wide env v =
- let wrapper =
- if wide then Builtins_string.frama_c_wcslen_wrapper
- else Builtins_string.frama_c_strlen_wrapper
- in
- let v, alarms = apply_logic_builtin wrapper env [v] in
- if Cvalue.V.is_bottom v
- then False (* bottom state => string always invalid *)
- else if alarms
- then Unknown (* alarm => string possibly invalid *)
- else True (* no alarm => string always valid for reading *)
-
-(* Evaluates a [valid_string] or [valid_wstring] predicate.
- First, we check the constness of the arguments.
- Then, we evaluate [valid_read_string/valid_read_wstring] on non-const ones. *)
-let eval_valid_str ~wide env v =
- assert (not (Cvalue.V.is_bottom v));
- (* filter const bases *)
- let v' = Cvalue.V.filter_base (fun b -> not (Base.is_read_only b)) v in
- if Cvalue.V.is_bottom v' then False (* all bases were const *)
- else
- if Cvalue.V.equal v v' then
- eval_valid_read_str ~wide env v (* all bases non-const *)
- else (* at least one base was const *)
- match eval_valid_read_str ~wide env v with
- | True -> Unknown (* weaken result *)
- | False | Unknown as r -> r
-
-
-(* Do all the possible values of a location in [state] satisfy [test]? [loc] is
- an over-approximation of the location, so the answer cannot be [False] even
- if some parts of [loc] do not satisfy [test]. Thus, this function does not
- fold the location, but instead applies [test] to the join of all values
- stored in [loc] in [state]. *)
-let forall_in_over_location state loc test =
- let v = Model.find_indeterminate state loc in
- test v
-
-exception EFalse
-
-(* Do all the possible values of a location in [state] satisfy [test]? [loc] is
- an under-approximation of the location, so the answer cannot be [True], as
- the values of some other parts of the location may not satisfy [test].
- However, it is [False] as soon as some part of [loc] contradicts [test]. *)
-let forall_in_under_location state loc test =
- let inspect_value (_, _) (value, _, _) acc =
- match test value with
- | True | Unknown -> acc
- | False -> raise EFalse
- in
- let inspect_itv base itv acc =
- match Cvalue.Model.find_base_or_default base state with
- | `Top | `Bottom -> Unknown
- | `Value offsm ->
- Cvalue.V_Offsetmap.fold_between ~entire:true itv inspect_value offsm acc
- in
- let inspect_base base intervals acc =
- Int_Intervals.fold (inspect_itv base) intervals acc
- in
- let zone = Locations.enumerate_bits loc in
- try Zone.fold_i inspect_base zone Unknown
- with EFalse -> False
- | Abstract_interp.Error_Top -> Unknown
-
-(* Evaluates an universal predicate about the values of a location evaluated to
- [r] in [state]. The predicates holds whenever all the possible values at the
- location satisfy [test]. *)
-let eval_forall_predicate state r test =
- let size_bits = Eval_typ.sizeof_lval_typ r.etype in
- let make_loc loc = make_loc loc size_bits in
- let over_loc = make_loc r.eover in
- if not Locations.(is_valid Read over_loc) then c_alarm ();
- match forall_in_over_location state over_loc test with
- | Unknown ->
- let under_loc = make_loc r.eunder in
- forall_in_under_location state under_loc test
- | True -> True
- | False -> if r.empty then Unknown else False
-
-(* Evaluation of an \initialized predicate on a location evaluated to [r]
- in the state [state]. *)
-let eval_initialized state r =
- let test = function
- | V_Or_Uninitialized.C_init_esc _
- | V_Or_Uninitialized.C_init_noesc _ -> True
- | V_Or_Uninitialized.C_uninit_esc _ -> Unknown
- | V_Or_Uninitialized.C_uninit_noesc v ->
- if Location_Bytes.is_bottom v then False else Unknown
- in
- eval_forall_predicate state r test
-
-(* Evaluation of a \dangling predicate on a location evaluated to [r]
- in the state [state]. *)
-let eval_dangling state r =
- let test = function
- | V_Or_Uninitialized.C_init_esc v ->
- if Location_Bytes.is_bottom v then True else Unknown
- | V_Or_Uninitialized.C_uninit_esc _ -> Unknown
- | V_Or_Uninitialized.C_init_noesc _
- | V_Or_Uninitialized.C_uninit_noesc _ -> False
- in
- eval_forall_predicate state r test
-
-let is_rel_binop = function
- | Lt
- | Gt
- | Le
- | Ge
- | Eq
- | Ne -> true
- | _ -> false
-
-let rel_of_binop = function
- | Lt -> Rlt
- | Gt -> Rgt
- | Le -> Rle
- | Ge -> Rge
- | Eq -> Req
- | Ne -> Rneq
- | _ -> assert false
-
-exception DoNotReduce
-exception Reduce_to_bottom
-
-let reduce_by_valid env positive access (tset: term) =
+and reduce_by_valid env positive access (tset: term) =
+ let exception DoNotReduce in
(* Auxiliary function that reduces \valid(lv+offs), where lv is atomic
(no more tsets), and offs is a bits-expressed constant offset.
[offs_typ] is supposed to be the type of the pointed location after [offs]
@@ -1924,7 +1952,7 @@ let reduce_by_valid env positive access (tset: term) =
in
let li = if op = PlusPI then li else Ival.neg_int li in
let typ_p = Cil.typeOf_pointed rtlv.etype in
- let sbits = Int.of_int (Cil.bitsSizeOf typ_p) in
+ let sbits = Integer.of_int (Cil.bitsSizeOf typ_p) in
(* Compute the offsets expected by [aux], which are [i *
8 * sizeof( *tlv)] *)
let li = Ival.scale sbits li in
@@ -1939,7 +1967,7 @@ let reduce_by_valid env positive access (tset: term) =
do_one env tset
(* reduce [tl] so that [rl rel tr] holds *)
-let reduce_by_left_relation ~alarm_mode env positive tl rel tr =
+and reduce_by_left_relation ~alarm_mode env positive tl rel tr =
try
let debug = false in
if debug then Format.printf "#Left term %a@." Printer.pp_term tl;
@@ -1982,7 +2010,7 @@ let reduce_by_left_relation ~alarm_mode env positive tl rel tr =
Eval_op.apply_on_all_locs aux locs env
with Not_an_exact_loc | LogicEvalError _ -> env
-let rec reduce_by_relation ~alarm_mode env positive t1 rel t2 =
+and reduce_by_relation ~alarm_mode env positive t1 rel t2 =
(* special case: t1 is a term of the form "a rel' b",
and is compared to "== 0" or "!= 0" => evaluate t1 directly;
note: such terms may be created by other evaluation/reduction functions
@@ -2004,7 +2032,7 @@ let rec reduce_by_relation ~alarm_mode env positive t1 rel t2 =
(and of course [eval_known_papp] below).
May raise LogicEvalError or Not_an_exact_loc, when no reduction can be done,
and Reduce_to_bottom, in which case the reduction leads to bottom. *)
-let reduce_by_known_papp ~alarm_mode env positive li _labels args =
+and reduce_by_known_papp ~alarm_mode env positive li _labels args =
(* If the term [arg] is a floating-point lvalue with an exact location,
reduces its value in [env] by using the backward propagator on fval
[fval_reduce]. *)
@@ -2098,7 +2126,7 @@ let reduce_by_known_papp ~alarm_mode env positive li _labels args =
(** Big recursive functions for predicates *)
-let rec reduce_by_predicate ~alarm_mode env positive p =
+and reduce_by_predicate ~alarm_mode env positive p =
let loc = p.pred_loc in
let rec reduce_by_predicate_content env positive p_content =
match positive,p_content with
@@ -2178,7 +2206,7 @@ let rec reduce_by_predicate ~alarm_mode env positive p =
| False -> overwrite_current_state env Cvalue.Model.bottom
| Unknown -> reduce_by_relation ~alarm_mode env positive t1 op t2
with
- | DoNotReduce | LogicEvalError _ -> env
+ | LogicEvalError _ -> env
| Reduce_to_bottom ->
overwrite_current_state env Cvalue.Model.bottom
(* if the exception was obtained without an alarm emitted,
@@ -2284,6 +2312,10 @@ let rec reduce_by_predicate ~alarm_mode env positive p =
in
reduce_by_predicate_content env positive p.pred_content
+(* -------------------------------------------------------------------------- *)
+(* --- Evaluation of predicates --- *)
+(* -------------------------------------------------------------------------- *)
+
and eval_predicate env pred =
let alarm_mode = Fail in
let loc = pred.pred_loc in
@@ -2551,6 +2583,7 @@ and eval_predicate env pred =
(* Logic predicates. Update the list known_predicates above if you
add something here. *)
and eval_known_papp env li _labels args =
+ let open Abstract_interp in
let unary_float unary_fun arg =
try
let eval_result = eval_term ~alarm_mode env arg in
@@ -2629,12 +2662,11 @@ and eval_predicate env pred =
in
do_eval env pred
-
(* -------------------------------------------------------------------------- *)
(* --- Dependencies of predicates --- *)
(* -------------------------------------------------------------------------- *)
-let eval_tsets_deps ~alarm_mode env lbl tsets =
+and eval_tsets_deps ~alarm_mode env lbl tsets =
let star_tsets = deref_tsets tsets in
let r = eval_tlval ~alarm_mode env star_tsets in
let size_bits = Eval_typ.sizeof_lval_typ r.etype in
@@ -2642,7 +2674,7 @@ let eval_tsets_deps ~alarm_mode env lbl tsets =
let zone = enumerate_valid_bits Locations.Read loc in
Logic_label.Map.add lbl zone r.ldeps
-let predicate_deps env pred =
+and predicate_deps env pred =
let alarm_mode = Ignore in
let rec do_eval env p =
let term_deps term = (eval_term ~alarm_mode env term).ldeps in
@@ -2694,12 +2726,12 @@ let predicate_deps env pred =
empty_logic_deps args
else
match Inline.inline_predicate ~inline ~current:env.e_cur p with
- | None -> unsupported (Format.asprintf "%a" Predicate.pretty p)
+ | None -> unsupported (Format.asprintf "%a" Printer.pp_predicate p)
| Some p' -> do_eval env p'
end
| Pfresh _ | Pallocable _ | Pfreeable _
- -> unsupported (Format.asprintf "%a" Predicate.pretty p)
+ -> unsupported (Format.asprintf "%a" Printer.pp_predicate p)
in
try Some (do_eval env pred)
with LogicEvalError _ -> None
@@ -2714,6 +2746,25 @@ let reduce_by_predicate env positive p =
let alarm_mode = alarm_reduce_mode () in
reduce_by_predicate ~alarm_mode env positive p
+let eval_tlval_as_location ~alarm_mode env t =
+ let r = eval_term_as_lval ~alarm_mode env t in
+ let s = Eval_typ.sizeof_lval_typ r.etype in
+ make_loc r.eover s
+
+(* Return a pair of (under-approximating, over-approximating) zones. *)
+let eval_tlval_as_zone_under_over ~alarm_mode access env t =
+ let r = eval_term_as_lval ~alarm_mode env t in
+ let s = Eval_typ.sizeof_lval_typ r.etype in
+ let under = enumerate_valid_bits_under access (make_loc r.eunder s) in
+ let over = enumerate_valid_bits access (make_loc r.eover s) in
+ (under, over)
+
+let eval_tlval_as_zone ~alarm_mode access env t =
+ let _under, over =
+ eval_tlval_as_zone_under_over ~alarm_mode access env t
+ in
+ over
+
let () =
(* TODO: deprecate loc_to_loc, move loc_to_locs into Value *)
Db.Properties.Interp.loc_to_loc :=
diff --git a/tests/value/logic.c b/tests/value/logic.c
index eeea0f321b921cfa138049c8a2c06c30e0ae7e43..8806b1930519098b26629b39b460e9e53098c516 100644
--- a/tests/value/logic.c
+++ b/tests/value/logic.c
@@ -437,6 +437,72 @@ void float_abs () {
Frama_C_show_each_0_3(x);
}
+/* Tests the evaluation of the [Tcomprehension] ACSL constructor. */
+void set_comprehension () {
+ int x = v;
+ if (v) {
+ //@ assert x \in { i | integer i; 10 <= i <= 100 };
+ Frama_C_show_each_10_100(x);
+ }
+ if (v) {
+ //@ assert x \in { i | int i; 10 <= i <= 100 };
+ Frama_C_show_each_10_100(x);
+ }
+ if (v) {
+ //@ assert x \in { 3*i + 1 | integer i; 10 <= i <= 100 };
+ Frama_C_show_each_31_301(x);
+ }
+ if (v) {
+ //@ assert x \in { i | integer i; 10 <= 2*i <= 100 };
+ Frama_C_show_each_5_50(x); // No reduction of i through the multiplication
+ }
+ if (v) {
+ //@ assert x \in { i-i | integer i; 10 <= i <= 100 };
+ Frama_C_show_each_0(x); // Imprecise evaluation of i-i in the logic
+ }
+ if (v) {
+ //@ assert x \in { i-i | integer i; 100 <= i <= 10 };
+ Frama_C_show_each_bottom(x); // No reduction on bottom
+ }
+ int a = Frama_C_interval(12, 24);
+ int b = Frama_C_interval(16, 32);
+ if (v) {
+ //@ assert x \in { i | integer i; a <= i <= b };
+ Frama_C_show_each_12_32(x);
+ }
+ if (v) {
+ //@ assert x \in { i | integer i; b <= i <= a };
+ Frama_C_show_each_16_24(x);
+ }
+ if (v) {
+ //@ assert x \in { 10*i + j | integer i, j; 2 <= i <= 6 && 3 < j < 9 };
+ Frama_C_show_each_24_68(x);
+ }
+ int t[15] = {2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47};
+ if (v) {
+ //@ assert x \in { t[i] | integer i; 2 <= i <= 12 };
+ Frama_C_show_each_5_41(x);
+ }
+ if (v) {
+ //@ assert x \in { t[i] | integer i; 5 <= i <= 25 };
+ Frama_C_show_each(x); // No reduction because of the alarm
+ }
+}
+
+//@ assigns { p[i][j] | int i, j; a <= i <= b && 0 <= j < size } \from \nothing;
+void multi_memset (char **p, int a, int b, int size);
+
+/* Tests assigns clauses through locations defined with set comprehension. */
+void set_comprehension_assigns () {
+ char buf0[10] = {0};
+ char buf1[12] = {0};
+ char buf2[8] = {0};
+ char buf3[10] = {0};
+ char *p[4] = {&buf0, &buf1, &buf2, &buf3 };
+ // assigns the 10 first cells of buf1 and buf2. Others remain at 0.
+ multi_memset(p, 1, 2, 10);
+}
+
void main () {
eq_tsets();
eq_char();
@@ -453,4 +519,6 @@ void main () {
min_max_quantifier ();
int_abs();
float_abs();
+ set_comprehension();
+ set_comprehension_assigns();
}
diff --git a/tests/value/oracle/logic.res.oracle b/tests/value/oracle/logic.res.oracle
index 069377d7cf41cf998dad89d491ccbd8e64839ca3..19994a9a280818d245b4d60cd76ce1e612fb0e48 100644
--- a/tests/value/oracle/logic.res.oracle
+++ b/tests/value/oracle/logic.res.oracle
@@ -14,7 +14,7 @@
arr_ptr[0..2] ∈ {0}
arr_ptr_arr[0..5] ∈ {0}
[eva] computing for function eq_tsets <- main.
- Called from tests/value/logic.c:441.
+ Called from tests/value/logic.c:507.
[eva] tests/value/logic.c:103:
cannot evaluate ACSL term, unsupported ACSL construct: == operation on non-supported type set<_#8>
[eva:alarm] tests/value/logic.c:103: Warning: assertion got status unknown.
@@ -56,20 +56,20 @@
[eva] Recording results for eq_tsets
[eva] Done for function eq_tsets
[eva] computing for function eq_char <- main.
- Called from tests/value/logic.c:442.
+ Called from tests/value/logic.c:508.
[eva] tests/value/logic.c:149: Frama_C_show_each: {-126}
[eva] tests/value/logic.c:150: assertion got status valid.
[eva] tests/value/logic.c:151: assertion got status valid.
[eva] Recording results for eq_char
[eva] Done for function eq_char
[eva] computing for function casts <- main.
- Called from tests/value/logic.c:443.
+ Called from tests/value/logic.c:509.
[eva] tests/value/logic.c:155: assertion got status valid.
[eva] tests/value/logic.c:156: assertion got status valid.
[eva] Recording results for casts
[eva] Done for function casts
[eva] computing for function empty_tset <- main.
- Called from tests/value/logic.c:444.
+ Called from tests/value/logic.c:510.
[eva] computing for function f_empty_tset <- empty_tset <- main.
Called from tests/value/logic.c:166.
[eva] using specification for function f_empty_tset
@@ -82,7 +82,7 @@
[eva] Recording results for empty_tset
[eva] Done for function empty_tset
[eva] computing for function reduce_by_equal <- main.
- Called from tests/value/logic.c:445.
+ Called from tests/value/logic.c:511.
[eva:alarm] tests/value/logic.c:172: Warning:
accessing out of bounds index. assert 0 ≤ v;
[eva:alarm] tests/value/logic.c:172: Warning:
@@ -92,7 +92,7 @@
[eva] Recording results for reduce_by_equal
[eva] Done for function reduce_by_equal
[eva] computing for function alarms <- main.
- Called from tests/value/logic.c:446.
+ Called from tests/value/logic.c:512.
[eva:alarm] tests/value/logic.c:182: Warning:
assertion 'ASSUME' got status unknown.
[eva:alarm] tests/value/logic.c:184: Warning:
@@ -124,7 +124,7 @@
[eva] Recording results for alarms
[eva] Done for function alarms
[eva] computing for function cond_in_lval <- main.
- Called from tests/value/logic.c:447.
+ Called from tests/value/logic.c:513.
[eva] computing for function select_like <- cond_in_lval <- main.
Called from tests/value/logic.c:228.
[eva] using specification for function select_like
@@ -152,7 +152,7 @@
[eva] Recording results for cond_in_lval
[eva] Done for function cond_in_lval
[eva] computing for function pred <- main.
- Called from tests/value/logic.c:448.
+ Called from tests/value/logic.c:514.
[eva] tests/value/logic.c:90: assertion got status valid.
[eva] tests/value/logic.c:91: assertion got status valid.
[eva] tests/value/logic.c:31:
@@ -201,7 +201,7 @@
[eva] Recording results for pred
[eva] Done for function pred
[eva] computing for function float_sign <- main.
- Called from tests/value/logic.c:449.
+ Called from tests/value/logic.c:515.
[eva] tests/value/logic.c:251: assertion got status valid.
[eva] tests/value/logic.c:252: assertion got status valid.
[eva] tests/value/logic.c:253: assertion got status valid.
@@ -210,7 +210,7 @@
[eva] Recording results for float_sign
[eva] Done for function float_sign
[eva] computing for function min_max <- main.
- Called from tests/value/logic.c:450.
+ Called from tests/value/logic.c:516.
[eva] computing for function Frama_C_interval <- min_max <- main.
Called from tests/value/logic.c:274.
[eva] using specification for function Frama_C_interval
@@ -235,7 +235,7 @@
[eva] Recording results for min_max
[eva] Done for function min_max
[eva] computing for function assign_tsets <- main.
- Called from tests/value/logic.c:451.
+ Called from tests/value/logic.c:517.
[eva] computing for function assign_tsets_aux <- assign_tsets <- main.
Called from tests/value/logic.c:269.
[eva] using specification for function assign_tsets_aux
@@ -243,7 +243,7 @@
[eva] Recording results for assign_tsets
[eva] Done for function assign_tsets
[eva] computing for function check_and_assert <- main.
- Called from tests/value/logic.c:452.
+ Called from tests/value/logic.c:518.
[eva:alarm] tests/value/logic.c:295: Warning: assertion got status unknown.
[eva] tests/value/logic.c:296: Frama_C_show_each_42: {42}
[eva] tests/value/logic.c:297: check got status valid.
@@ -258,7 +258,7 @@
[eva] Recording results for check_and_assert
[eva] Done for function check_and_assert
[eva] computing for function min_max_quantifier <- main.
- Called from tests/value/logic.c:453.
+ Called from tests/value/logic.c:519.
[eva] tests/value/logic.c:321: check 'valid' got status valid.
[eva] tests/value/logic.c:322: check 'valid' got status valid.
[eva] tests/value/logic.c:323: check 'valid' got status valid.
@@ -332,7 +332,7 @@
[eva] Recording results for min_max_quantifier
[eva] Done for function min_max_quantifier
[eva] computing for function int_abs <- main.
- Called from tests/value/logic.c:454.
+ Called from tests/value/logic.c:520.
[eva] computing for function abs <- int_abs <- main.
Called from tests/value/logic.c:365.
[eva] using specification for function abs
@@ -455,7 +455,7 @@
[eva] Recording results for int_abs
[eva] Done for function int_abs
[eva] computing for function float_abs <- main.
- Called from tests/value/logic.c:455.
+ Called from tests/value/logic.c:521.
[eva] computing for function fabs <- float_abs <- main.
Called from tests/value/logic.c:421.
[eva] using specification for function fabs
@@ -513,6 +513,51 @@
[eva] tests/value/logic.c:437: Frama_C_show_each_0_3: [-0. .. 3.]
[eva] Recording results for float_abs
[eva] Done for function float_abs
+[eva] computing for function set_comprehension <- main.
+ Called from tests/value/logic.c:522.
+[eva:alarm] tests/value/logic.c:444: Warning: assertion got status unknown.
+[eva] tests/value/logic.c:445: Frama_C_show_each_10_100: [10..100]
+[eva:alarm] tests/value/logic.c:448: Warning: assertion got status unknown.
+[eva] tests/value/logic.c:449: Frama_C_show_each_10_100: [10..100]
+[eva:alarm] tests/value/logic.c:452: Warning: assertion got status unknown.
+[eva] tests/value/logic.c:453: Frama_C_show_each_31_301: [31..301],1%3
+[eva:alarm] tests/value/logic.c:456: Warning: assertion got status unknown.
+[eva] tests/value/logic.c:457: Frama_C_show_each_5_50: [-2147483648..2147483647]
+[eva:alarm] tests/value/logic.c:460: Warning: assertion got status unknown.
+[eva] tests/value/logic.c:461: Frama_C_show_each_0: [-90..90]
+[eva:alarm] tests/value/logic.c:464: Warning: assertion got status unknown.
+[eva] tests/value/logic.c:465:
+ Frama_C_show_each_bottom: [-2147483648..2147483647]
+[eva] computing for function Frama_C_interval <- set_comprehension <- main.
+ Called from tests/value/logic.c:467.
+[eva] tests/value/logic.c:467:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- set_comprehension <- main.
+ Called from tests/value/logic.c:468.
+[eva] tests/value/logic.c:468:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:alarm] tests/value/logic.c:470: Warning: assertion got status unknown.
+[eva] tests/value/logic.c:471: Frama_C_show_each_12_32: [12..32]
+[eva:alarm] tests/value/logic.c:474: Warning: assertion got status unknown.
+[eva] tests/value/logic.c:475: Frama_C_show_each_16_24: [16..24]
+[eva:alarm] tests/value/logic.c:478: Warning: assertion got status unknown.
+[eva] tests/value/logic.c:479: Frama_C_show_each_24_68: [24..68]
+[eva:alarm] tests/value/logic.c:483: Warning: assertion got status unknown.
+[eva] tests/value/logic.c:484: Frama_C_show_each_5_41: [5..41],1%2
+[eva:alarm] tests/value/logic.c:487: Warning: assertion got status unknown.
+[eva] tests/value/logic.c:488: Frama_C_show_each: [-2147483648..2147483647]
+[eva] Recording results for set_comprehension
+[eva] Done for function set_comprehension
+[eva] computing for function set_comprehension_assigns <- main.
+ Called from tests/value/logic.c:523.
+[eva] computing for function multi_memset <- set_comprehension_assigns <- main.
+ Called from tests/value/logic.c:503.
+[eva] using specification for function multi_memset
+[eva] Done for function multi_memset
+[eva] Recording results for set_comprehension_assigns
+[eva] Done for function set_comprehension_assigns
[eva] Recording results for main
[eva] done for function main
[scope:rm_asserts] removing 5 assertion(s)
@@ -657,6 +702,36 @@
b.i1 ∈ {6}
.i2 ∈ {8}
x_0 ∈ [-2147483648..0]
+[eva:final-states] Values at end of function set_comprehension:
+ Frama_C_entropy_source ∈ [--..--]
+ x_0 ∈ [--..--]
+ a ∈ [12..24]
+ b ∈ [16..32]
+ t_0[0] ∈ {2}
+ [1] ∈ {3}
+ [2] ∈ {5}
+ [3] ∈ {7}
+ [4] ∈ {11}
+ [5] ∈ {13}
+ [6] ∈ {17}
+ [7] ∈ {19}
+ [8] ∈ {23}
+ [9] ∈ {29}
+ [10] ∈ {31}
+ [11] ∈ {37}
+ [12] ∈ {41}
+ [13] ∈ {43}
+ [14] ∈ {47}
+[eva:final-states] Values at end of function set_comprehension_assigns:
+ buf0[0..9] ∈ {0}
+ buf1[0..9] ∈ [--..--]
+ [10..11] ∈ {0}
+ buf2[0..7] ∈ [--..--]
+ buf3[0..9] ∈ {0}
+ p[0] ∈ {{ &buf0[0] }}
+ [1] ∈ {{ &buf1[0] }}
+ [2] ∈ {{ &buf2[0] }}
+ [3] ∈ {{ &buf3[0] }}
[eva:final-states] Values at end of function unsup:
t_T{.z; .t} ∈ {21}
[eva:final-states] Values at end of function pred:
@@ -725,6 +800,12 @@
[from] Computing for function select_like <-cond_in_lval
[from] Done for function select_like
[from] Done for function cond_in_lval
+[from] Computing for function set_comprehension
+[from] Done for function set_comprehension
+[from] Computing for function set_comprehension_assigns
+[from] Computing for function multi_memset <-set_comprehension_assigns
+[from] Done for function multi_memset
+[from] Done for function set_comprehension_assigns
[from] Computing for function unsup
[from] Done for function unsup
[from] Computing for function pred
@@ -778,6 +859,9 @@
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function min_max_quantifier:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function multi_memset:
+ buf1[0..9] FROM \nothing (and SELF)
+ buf2[0..7] FROM \nothing (and SELF)
[from] Function reduce_by_equal:
NO EFFECTS
[from] Function select_like:
@@ -786,6 +870,10 @@
b FROM p; q; a; b (and SELF)
[from] Function cond_in_lval:
NO EFFECTS
+[from] Function set_comprehension:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function set_comprehension_assigns:
+ NO EFFECTS
[from] Function unsup:
t_T FROM \nothing
[from] Function pred:
@@ -866,6 +954,14 @@
a; out; b; x_0
[inout] Inputs for function cond_in_lval:
v
+[inout] Out (internal) for function set_comprehension:
+ Frama_C_entropy_source; x_0; a; b; t_0[0..14]
+[inout] Inputs for function set_comprehension:
+ Frama_C_entropy_source; v
+[inout] Out (internal) for function set_comprehension_assigns:
+ buf0[0..9]; buf1[0..11]; buf2[0..7]; buf3[0..9]; p[0..3]
+[inout] Inputs for function set_comprehension_assigns:
+ \nothing
[inout] Out (internal) for function unsup:
t_T
[inout] Inputs for function unsup: