diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index c09f4e6b4fccfd0434b06eda9a42e17544ab4eaa..1da9ccf2e15d1e4cc7265d5ca0a464811ce1d474 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -470,18 +470,6 @@ module Value = struct
Table_By_Callstack.find stmt)
with Not_found -> None
- let fold_stmt_state_callstack f acc ~after stmt =
- assert (is_computed ()); (* this assertion fails during Eva analysis *)
- match get_stmt_state_callstack ~after stmt with
- | None -> acc
- | Some h -> Eva_types.Callstack.Hashtbl.fold (fun _ -> f) h acc
-
- let fold_state_callstack f acc ~after ki =
- assert (is_computed ()); (* this assertion fails during Eva analysis *)
- match ki with
- | Kglobal -> f (globals_state ()) acc
- | Kstmt stmt -> fold_stmt_state_callstack f acc ~after stmt
-
let is_reachable = Cvalue.Model.is_reachable
exception Is_reachable
@@ -506,35 +494,8 @@ module Value = struct
| Kglobal -> Cvalue.Model.is_reachable (globals_state ())
| Kstmt stmt -> is_reachable_stmt stmt
- let eval_lval =
- ref (fun ?with_alarms:_ _ -> mk_labeled_fun "Value.eval_lval")
- let eval_expr =
- ref (fun ?with_alarms:_ _ -> mk_labeled_fun "Value.eval_expr")
-
- let eval_expr_with_state =
- ref (fun ?with_alarms:_ _ -> mk_labeled_fun "Value.eval_expr_with_state")
-
- let reduce_by_cond = mk_fun "Value.reduce_by_cond"
-
- let find_lv_plus = mk_fun "Value.find_lv_plus"
-
let compute = mk_fun "Value.compute"
-
- let lval_to_loc_with_deps = mk_fun "Value.lval_to_loc_with_deps"
- let lval_to_loc_with_deps_state = mk_fun "Value.lval_to_loc_with_deps_state"
- let lval_to_loc = mk_fun "Value.lval_to_loc"
- let lval_to_offsetmap = mk_fun "Value.lval_to_offsetmap"
- let lval_to_offsetmap_state = mk_fun "Value.lval_to_offsetmap_state"
- let lval_to_loc_state = mk_fun "Value.lval_to_loc_state"
- let lval_to_zone = mk_fun "Value.lval_to_zone"
- let lval_to_zone_state = mk_fun "Value.lval_to_zone_state"
- let lval_to_zone_with_deps_state = mk_fun "Value.lval_to_zone_with_deps_state"
- let lval_to_precise_loc_state =
- ref (fun ?with_alarms:_ _ -> mk_labeled_fun "Value.lval_to_precise_loc")
- let lval_to_precise_loc_with_deps_state =
- mk_fun "Value.lval_to_precise_loc_with_deps_state"
-
end
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 18c76a9838ef2d6eb38920f0f7da01e5a6689a46..3e820ffff2a188f6965eade123baf0f20a01d628 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -216,36 +216,6 @@ module Value : sig
(** [after] is false by default.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
- val fold_stmt_state_callstack :
- (state -> 'a -> 'a) -> 'a -> after:bool -> stmt -> 'a
-
- val fold_state_callstack :
- (state -> 'a -> 'a) -> 'a -> after:bool -> kinstr -> 'a
-
- (** {3 Evaluations} *)
-
- val eval_lval :
- (?with_alarms:CilE.warn_mode ->
- Locations.Zone.t option ->
- state ->
- lval ->
- Locations.Zone.t option * t) ref
-
- val eval_expr :
- (?with_alarms:CilE.warn_mode -> state -> exp -> t) ref
-
- val eval_expr_with_state :
- (?with_alarms:CilE.warn_mode -> state -> exp -> state * t) ref
-
- val reduce_by_cond:
- (state -> exp -> bool -> state) ref
-
- val find_lv_plus :
- (Cvalue.Model.t -> Cil_types.exp ->
- (Cil_types.lval * Ival.t) list) ref
- (** returns the list of all decompositions of [expr] into the sum an lvalue
- and an interval. *)
-
(** {3 Reachability} *)
val is_accessible : kinstr -> bool
@@ -254,61 +224,6 @@ module Value : sig
val is_reachable_stmt : stmt -> bool
- (** {3 Locations of left values} *)
-
- val lval_to_loc :
- (kinstr -> ?with_alarms:CilE.warn_mode -> lval -> Locations.location) ref
-
- val lval_to_loc_with_deps :
- (kinstr
- -> ?with_alarms:CilE.warn_mode
- -> deps:Locations.Zone.t
- -> lval
- -> Locations.Zone.t * Locations.location) ref
-
- val lval_to_loc_with_deps_state :
- (state
- -> deps:Locations.Zone.t
- -> lval
- -> Locations.Zone.t * Locations.location) ref
-
- val lval_to_loc_state :
- (state -> lval -> Locations.location) ref
-
- val lval_to_offsetmap :
- ( kinstr -> ?with_alarms:CilE.warn_mode -> lval ->
- Cvalue.V_Offsetmap.t option) ref
-
- val lval_to_offsetmap_state :
- (state -> lval -> Cvalue.V_Offsetmap.t option) ref
- (** @since Carbon-20110201 *)
-
- val lval_to_zone :
- (kinstr -> ?with_alarms:CilE.warn_mode -> lval -> Locations.Zone.t) ref
-
- val lval_to_zone_state :
- (state -> lval -> Locations.Zone.t) ref
- (** Does not emit alarms. *)
-
- val lval_to_zone_with_deps_state:
- (state -> for_writing:bool -> deps:Locations.Zone.t option -> lval ->
- Locations.Zone.t * Locations.Zone.t * bool) ref
- (** [lval_to_zone_with_deps_state state ~for_writing ~deps lv] computes
- [res_deps, zone_lv, exact], where [res_deps] are the memory zones needed
- to evaluate [lv] in [state] joined with [deps]. [zone_lv] contains the
- valid memory zones that correspond to the location that [lv] evaluates
- to in [state]. If [for_writing] is true, [zone_lv] is restricted to
- memory zones that are writable. [exact] indicates that [lv] evaluates
- to a valid location of cardinal at most one. *)
-
- val lval_to_precise_loc_state:
- (?with_alarms:CilE.warn_mode -> state -> lval ->
- state * Precise_locs.precise_location * typ) ref
-
- val lval_to_precise_loc_with_deps_state:
- (state -> deps:Locations.Zone.t option -> lval ->
- Locations.Zone.t * Precise_locs.precise_location) ref
-
val no_results: (fundec -> bool) ref
(** Returns [true] if the user has requested that no results should
diff --git a/src/plugins/eva/domains/cvalue/builtins_misc.ml b/src/plugins/eva/domains/cvalue/builtins_misc.ml
index 93fbcf970dc1d94407aa23aed067188751b4f5b3..47d8da9c980db7c8e0dad4beb6625dd7aef98d90 100644
--- a/src/plugins/eva/domains/cvalue/builtins_misc.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_misc.ml
@@ -22,6 +22,7 @@
open Eva_utils
+open Lattice_bounds.Bottom.Operators
let frama_C_assert state actuals =
let do_bottom () =
@@ -35,10 +36,14 @@ let frama_C_assert state actuals =
then do_bottom ()
else if Cvalue.V.contains_zero arg
then begin
- let state = !Db.Value.reduce_by_cond state arg_exp true in
- if Cvalue.Model.is_reachable state
- then (warning_once_current "Frama_C_assert: unknown"; state)
- else do_bottom ()
+ let state =
+ let* valuation = fst (Cvalue_queries.reduce state arg_exp true) in
+ let valuation = Cvalue_queries.to_domain_valuation valuation in
+ Cvalue_transfer.update valuation state
+ in
+ match state with
+ | `Value state -> warning_once_current "Frama_C_assert: unknown"; state
+ | `Bottom -> do_bottom ()
end
else begin
warning_once_current "Frama_C_assert: true";
diff --git a/src/plugins/eva/domains/cvalue/builtins_split.ml b/src/plugins/eva/domains/cvalue/builtins_split.ml
index 5d6721b188a2ca2c2efc6d93ea2834e83db29bb5..a6a2cf2812a911993cd1ed76bfefdec413ca2933 100644
--- a/src/plugins/eva/domains/cvalue/builtins_split.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_split.ml
@@ -74,7 +74,7 @@ let warning warn s =
[max_card] elements. *)
let split_v ~warn lv state max_card =
if Cil.isArithmeticOrPointerType (Cil.typeOfLval lv) then
- let loc = !Db.Value.lval_to_loc_state state lv in
+ let loc = Cvalue_queries.lval_to_loc state lv in
if Locations.Location_Bits.cardinal_zero_or_one loc.Locations.loc then
let v_indet = Cvalue.Model.find_indeterminate state loc in
let v = Cvalue.V_Or_Uninitialized.get_v v_indet in
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 56b16b97f71b400fa7502c214f14319382e12f95..c6f8db8b6f69c634ccfd265263e9bd025c290884 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -24,142 +24,14 @@ open Eval
let dkey_card = Self.register_category "cardinal"
-module Model = struct
+module State = struct
- include Cvalue.Model
+ type state = Cvalue.Model.t * Locals_scoping.clobbered_set
type value = Main_values.CVal.t
type location = Main_locations.PLoc.location
- (* The origin is the value stored in the state for a lvalue, when this value
- has a type incompatible with the type of the lvalue. This may happen on
- union with fields of different types, or on code pattern such as
- int x = v; float f = *(float* )&x
- In this case, the value stored in the state and the value computed for the
- lvalue can be incomparable. The origin is then used to store the value from
- the state, to later choose which value to keep. This is done by the update
- function in cvalue_transfer. *)
- type origin = value
-
- let extract_expr _state _expr = `Value (Cvalue.V.top, None), Alarmset.all
-
- let indeterminate_alarms lval v =
- let open Cvalue.V_Or_Uninitialized in
- let status =
- if Cvalue.V.is_bottom (get_v v) then Alarmset.False else Alarmset.Unknown
- in
- match v with
- | C_uninit_noesc _ -> Alarmset.singleton ~status (Alarms.Uninitialized lval)
- | C_init_esc _ -> Alarmset.singleton ~status (Alarms.Dangling lval)
- | C_uninit_esc _ ->
- (* Unknown alarms: [v] can be either dangling or uninit *)
- Alarmset.(set (Alarms.Dangling lval) Unknown
- (set (Alarms.Uninitialized lval) Unknown none))
- | C_init_noesc _ -> Alarmset.none
-
-
- let eval_one_loc state lval typ =
- let eval_one_loc single_loc =
- let v = Cvalue.Model.find_indeterminate state single_loc in
- Cvalue.V_Or_Uninitialized.get_v v, indeterminate_alarms lval v
- in
- (* We have no good neutral element for "no alarm emitted yet", so we use
- [None] instead. *)
- let join_alarms acc alarms =
- match acc with
- | None -> Some alarms
- | Some acc -> Some (Alarmset.union alarms acc)
- in
- fun loc (acc_result, acc_alarms) ->
- let result, alarms = eval_one_loc loc in
- let result = Cvalue_forward.make_volatile ~typ:typ result in
- Cvalue.V.join result acc_result, join_alarms acc_alarms alarms
-
- (* The zero singleton is shared between float and integer representations in
- ival, and is thus untyped. *)
- let is_float v =
- Cvalue.V.(is_included v top_float) && Cvalue.V.contains_non_zero v
-
- let extract_scalar_lval state lval typ loc =
- let process_one_loc = eval_one_loc state lval typ in
- let acc = Cvalue.V.bottom, None in
- let value, alarms = Precise_locs.fold process_one_loc loc acc in
- let alarms = match alarms with None -> Alarmset.none | Some a -> a in
- (* The origin is set to false when the value stored in the memory has not
- the same type as the read lvalue. In this case, we don't update the state
- with the new value stemming from the evaluation, even if it has been
- reduced, in order to not propagate incompatible type. *)
- let incompatible_type = is_float value <> Cil.isFloatingType typ in
- let origin = if incompatible_type then Some value else None in
- let value = Cvalue_forward.reinterpret typ value in
- if Cvalue.V.is_bottom value
- then `Bottom, alarms
- else `Value (value, origin), alarms
-
- (* Imprecise version for aggregate types that cvalues are unable to precisely
- represent. The initialization alarms must remain sound, though. *)
- let extract_aggregate_lval state lval _typ ploc =
- let loc = Precise_locs.imprecise_location ploc in
- match loc.Locations.size with
- | Int_Base.Top -> `Value (Cvalue.V.top, None), Alarmset.all
- | Int_Base.Value size ->
- let offsm = Cvalue.Model.copy_offsetmap loc.Locations.loc size state in
- match offsm with
- | `Bottom -> `Bottom, Alarmset.none
- | `Value offsm ->
- let value = Cvalue.V_Offsetmap.find_imprecise_everywhere offsm in
- let alarms = indeterminate_alarms lval value in
- let v = Cvalue.V_Or_Uninitialized.get_v value in
- let v = if Cvalue.V.is_bottom v then `Bottom else `Value (v, None) in
- v, alarms
-
- let extract_lval state lval typ loc =
- if Cil.isArithmeticOrPointerType typ
- then extract_scalar_lval state lval typ loc
- else extract_aggregate_lval state lval typ loc
-
- let backward_location state _lval typ precise_loc value =
- let size = Precise_locs.loc_size precise_loc in
- let upto = succ (Int_set.get_small_cardinal()) in
- let loc = Precise_locs.imprecise_location precise_loc in
- let eval_one_loc single_loc =
- let v = Cvalue.Model.find state single_loc in
- let v = Cvalue_forward.make_volatile ~typ v in
- Cvalue_forward.reinterpret typ v
- in
- let process_ival base ival (acc_loc, acc_val as acc) =
- let loc_bits = Locations.Location_Bits.inject base ival in
- let single_loc = Locations.make_loc loc_bits size in
- let v = eval_one_loc single_loc in
- if Cvalue.V.intersects v value
- then Locations.Location_Bits.join loc_bits acc_loc, Cvalue.V.join v acc_val
- else acc
- in
- let fold_ival base ival acc =
- if Ival.cardinal_is_less_than ival upto
- then Ival.fold_enum (process_ival base) ival acc
- else process_ival base ival acc
- in
- let fold_location loc acc =
- try
- let loc = loc.Locations.loc in
- Locations.Location_Bits.fold_i fold_ival loc acc
- with
- Abstract_interp.Error_Top -> loc.Locations.loc, value
- in
- let acc = Locations.Location_Bits.bottom, Cvalue.V.bottom in
- let loc_bits, value = fold_location loc acc in
- if Locations.Location_Bits.is_bottom loc_bits
- then `Bottom
- else
- let loc = Precise_locs.inject_location_bits loc_bits in
- `Value (Precise_locs.make_precise_loc loc ~size, value)
-
-end
-
-
-module State = struct
-
- type state = Model.t * Locals_scoping.clobbered_set
+ let value_dependencies = Main_values.cval
+ let location_dependencies = Main_locations.ploc
let log_category = Self.dkey_cvalue_domain
@@ -167,15 +39,16 @@ module State = struct
struct
include Datatype.Serializable_undefined
type t = state
- let name = Model.name ^ "+clobbered_set"
- let reprs = List.map (fun s -> s, Locals_scoping.bottom ()) Model.reprs
+ let name = Cvalue.Model.name ^ "+clobbered_set"
+ let reprs =
+ List.map (fun s -> s, Locals_scoping.bottom ()) Cvalue.Model.reprs
let structural_descr =
- Structural_descr.(
- t_tuple [| Model.packed_descr; pack Locals_scoping.structural_descr |])
- let pretty fmt (s, _) = Model.pretty fmt s
- let equal (a, _) (b, _) = Model.equal a b
- let compare (a, _) (b, _) = Model.compare a b
- let hash (s, _) = Model.hash s
+ Structural_descr.t_tuple
+ [| Cvalue.Model.packed_descr; Locals_scoping.packed_descr |]
+ let pretty fmt (s, _) = Cvalue.Model.pretty fmt s
+ let equal (a, _) (b, _) = Cvalue.Model.equal a b
+ let compare (a, _) (b, _) = Cvalue.Model.compare a b
+ let hash (s, _) = Cvalue.Model.hash s
let rehash = Datatype.identity
let copy = Datatype.undefined
let mem_project = Datatype.never_any_project
@@ -184,33 +57,31 @@ module State = struct
let name = "cvalue"
let key = Structure.Key_Domain.create_key name
- type value = Model.value
- type location = Model.location
-
- let value_dependencies = Main_values.cval
- let location_dependencies = Main_locations.ploc
-
- let top = Model.top, Locals_scoping.bottom ()
- let is_included (a, _) (b, _) = Model.is_included a b
- let join (a, clob) (b, _) = Model.join a b, clob
+ let top = Cvalue.Model.top, Locals_scoping.bottom ()
+ let is_included (a, _) (b, _) = Cvalue.Model.is_included a b
+ let join (a, clob) (b, _) = Cvalue.Model.join a b, clob
let widen kf stmt (a, clob) (b, _) =
let hint = Widen.getWidenHints kf stmt in
- Model.widen hint a b, clob
+ Cvalue.Model.widen hint a b, clob
let narrow (a, clob) (b, _) =
- let s = Model.narrow a b in
- if Model.(equal bottom s) then `Bottom else `Value (s, clob)
+ let s = Cvalue.Model.narrow a b in
+ if Cvalue.Model.(equal bottom s) then `Bottom else `Value (s, clob)
- type origin = Model.origin
+ type origin = Cvalue_queries.origin
+
+ let extract_expr ~oracle context (state, _) expr =
+ Cvalue_queries.extract_expr ~oracle context state expr
+
+ let extract_lval ~oracle context (state, _) lval typ loc =
+ Cvalue_queries.extract_lval ~oracle context state lval typ loc
- let extract_expr ~oracle:_ _context (s, _) expr =
- Model.extract_expr s expr
- let extract_lval ~oracle:_ _context (s, _) lval typ loc =
- Model.extract_lval s lval typ loc
let backward_location (state, _) lval typ precise_loc value =
- Model.backward_location state lval typ precise_loc value
- let reduce_further _ _ _ = []
+ Cvalue_queries.backward_location state lval typ precise_loc value
+
+ let reduce_further (state, _) expr value =
+ Cvalue_queries.reduce_further state expr value
(* ------------------------------------------------------------------------ *)
(* Transfer Functions *)
@@ -241,11 +112,11 @@ module State = struct
let start_recursive_call stmt call recursion (state, clob) =
let direct = is_direct_recursion stmt call in
- let state = Model.remove_variables recursion.withdrawal state in
+ let state = Cvalue.Model.remove_variables recursion.withdrawal state in
let substitution = recursion.base_substitution in
let clob = if direct then clob else Locals_scoping.top () in
let state = Locals_scoping.substitute substitution clob state in
- Model.replace_base substitution state
+ Cvalue.Model.replace_base substitution state
let start_call stmt call recursion valuation (state, clob) =
(* Uses the [valuation] to update the [state] before the substitution
@@ -263,7 +134,7 @@ module State = struct
let direct = is_direct_recursion stmt call in
let pre, clob = pre in
let substitution = recursion.base_substitution in
- let state = Model.replace_base substitution state in
+ let state = Cvalue.Model.replace_base substitution state in
let clob = if direct then clob else Locals_scoping.top () in
let state = Locals_scoping.substitute substitution clob state in
let inter = Cvalue.Model.filter_by_shape recursion.base_withdrawal pre in
@@ -365,7 +236,7 @@ module State = struct
else Cvalue.V_Or_Uninitialized.C_uninit_noesc value
in
let loc = Precise_locs.imprecise_location loc in
- Model.add_indeterminate_binding ~exact:true state loc cvalue, clob
+ Cvalue.Model.add_indeterminate_binding ~exact:true state loc cvalue, clob
let empty () =
let open Cvalue in
@@ -399,7 +270,7 @@ module State = struct
| Abstract_domain.Result kf ->
let value = Library_functions.returned_value kf in
let loc = Locations.loc_of_varinfo varinfo in
- Model.add_binding ~exact:true state loc value, clob
+ Cvalue.Model.add_binding ~exact:true state loc value, clob
(* ------------------------------------------------------------------------ *)
(* Misc *)
@@ -416,13 +287,13 @@ module State = struct
else
Bottom.non_bottom (Cvalue.Default_offsetmap.default_offsetmap b)
in
- Model.add_base b offsm state
+ Cvalue.Model.add_base b offsm state
let bind_global state varinfo =
let base = Base.of_varinfo varinfo in
let loc = Locations.loc_of_base base in
let value = Cvalue.V_Or_Uninitialized.uninitialized in
- Model.add_indeterminate_binding ~exact:true state loc value
+ Cvalue.Model.add_indeterminate_binding ~exact:true state loc value
let enter_scope kind vars (state, clob) =
let bind =
@@ -433,7 +304,7 @@ module State = struct
List.fold_left bind state vars, clob
let leave_scope kf vars (state, clob) =
- let state = Model.remove_variables vars state in
+ let state = Cvalue.Model.remove_variables vars state in
try
let fdec = Kernel_function.get_definition kf in
Locals_scoping.make_escaping_fundec fdec clob vars state, clob
@@ -595,16 +466,16 @@ let registered =
type prefix = Hptmap.prefix
module Subpart = struct
- type t = Model.subtree
- let hash = Model.hash_subtree
- let equal = Model.equal_subtree
+ type t = Cvalue.Model.subtree
+ let hash = Cvalue.Model.hash_subtree
+ let equal = Cvalue.Model.equal_subtree
end
let distinct_subpart (a, _) (b, _) =
- if Model.equal a b then None
+ if Cvalue.Model.equal a b then None
else
- try Model.comp_prefixes a b; None
- with Model.Found_prefix (p, s1, s2) -> Some (p, s1, s2)
-let find_subpart (s, _) prefix = Model.find_prefix s prefix
+ try Cvalue.Model.comp_prefixes a b; None
+ with Cvalue.Model.Found_prefix (p, s1, s2) -> Some (p, s1, s2)
+let find_subpart (s, _) prefix = Cvalue.Model.find_prefix s prefix
module Getters (Dom : Abstract.Domain.External) = struct
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.ml b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
new file mode 100644
index 0000000000000000000000000000000000000000..ae31230b0e8ede332ce8a485e99431acb7c51d83
--- /dev/null
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
@@ -0,0 +1,184 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module Queries = struct
+
+ type state = Cvalue.Model.t
+ type value = Main_values.CVal.t
+ type location = Main_locations.PLoc.location
+
+ (* The origin is the value stored in the state for a lvalue, when this value
+ has a type incompatible with the type of the lvalue. This may happen on
+ union with fields of different types, or on code pattern such as
+ int x = v; float f = *(float* )&x
+ In this case, the value stored in the state and the value computed for the
+ lvalue can be incomparable. The origin is then used to store the value from
+ the state, to later choose which value to keep. This is done by the update
+ function in cvalue_transfer. *)
+ type origin = value
+
+ let extract_expr ~oracle:_ _context _state _expr =
+ `Value (Cvalue.V.top, None), Alarmset.all
+
+ let indeterminate_alarms lval v =
+ let open Cvalue.V_Or_Uninitialized in
+ let status =
+ if Cvalue.V.is_bottom (get_v v) then Alarmset.False else Alarmset.Unknown
+ in
+ match v with
+ | C_uninit_noesc _ -> Alarmset.singleton ~status (Alarms.Uninitialized lval)
+ | C_init_esc _ -> Alarmset.singleton ~status (Alarms.Dangling lval)
+ | C_uninit_esc _ ->
+ (* Unknown alarms: [v] can be either dangling or uninit *)
+ Alarmset.(set (Alarms.Dangling lval) Unknown
+ (set (Alarms.Uninitialized lval) Unknown none))
+ | C_init_noesc _ -> Alarmset.none
+
+
+ let eval_one_loc state lval typ =
+ let eval_one_loc single_loc =
+ let v = Cvalue.Model.find_indeterminate state single_loc in
+ Cvalue.V_Or_Uninitialized.get_v v, indeterminate_alarms lval v
+ in
+ (* We have no good neutral element for "no alarm emitted yet", so we use
+ [None] instead. *)
+ let join_alarms acc alarms =
+ match acc with
+ | None -> Some alarms
+ | Some acc -> Some (Alarmset.union alarms acc)
+ in
+ fun loc (acc_result, acc_alarms) ->
+ let result, alarms = eval_one_loc loc in
+ let result = Cvalue_forward.make_volatile ~typ:typ result in
+ Cvalue.V.join result acc_result, join_alarms acc_alarms alarms
+
+ (* The zero singleton is shared between float and integer representations in
+ ival, and is thus untyped. *)
+ let is_float v =
+ Cvalue.V.(is_included v top_float) && Cvalue.V.contains_non_zero v
+
+ let extract_scalar_lval state lval typ loc =
+ let process_one_loc = eval_one_loc state lval typ in
+ let acc = Cvalue.V.bottom, None in
+ let value, alarms = Precise_locs.fold process_one_loc loc acc in
+ let alarms = match alarms with None -> Alarmset.none | Some a -> a in
+ (* The origin is set to false when the value stored in the memory has not
+ the same type as the read lvalue. In this case, we don't update the state
+ with the new value stemming from the evaluation, even if it has been
+ reduced, in order to not propagate incompatible type. *)
+ let incompatible_type = is_float value <> Cil.isFloatingType typ in
+ let origin = if incompatible_type then Some value else None in
+ let value = Cvalue_forward.reinterpret typ value in
+ if Cvalue.V.is_bottom value
+ then `Bottom, alarms
+ else `Value (value, origin), alarms
+
+ (* Imprecise version for aggregate types that cvalues are unable to precisely
+ represent. The initialization alarms must remain sound, though. *)
+ let extract_aggregate_lval state lval _typ ploc =
+ let loc = Precise_locs.imprecise_location ploc in
+ match loc.Locations.size with
+ | Int_Base.Top -> `Value (Cvalue.V.top, None), Alarmset.all
+ | Int_Base.Value size ->
+ let offsm = Cvalue.Model.copy_offsetmap loc.Locations.loc size state in
+ match offsm with
+ | `Bottom -> `Bottom, Alarmset.none
+ | `Value offsm ->
+ let value = Cvalue.V_Offsetmap.find_imprecise_everywhere offsm in
+ let alarms = indeterminate_alarms lval value in
+ let v = Cvalue.V_Or_Uninitialized.get_v value in
+ let v = if Cvalue.V.is_bottom v then `Bottom else `Value (v, None) in
+ v, alarms
+
+ let extract_lval ~oracle:_ _context state lval typ loc =
+ if Cil.isArithmeticOrPointerType typ
+ then extract_scalar_lval state lval typ loc
+ else extract_aggregate_lval state lval typ loc
+
+ let backward_location state _lval typ precise_loc value =
+ let size = Precise_locs.loc_size precise_loc in
+ let upto = succ (Int_set.get_small_cardinal()) in
+ let loc = Precise_locs.imprecise_location precise_loc in
+ let eval_one_loc single_loc =
+ let v = Cvalue.Model.find state single_loc in
+ let v = Cvalue_forward.make_volatile ~typ v in
+ Cvalue_forward.reinterpret typ v
+ in
+ let process_ival base ival (acc_loc, acc_val as acc) =
+ let loc_bits = Locations.Location_Bits.inject base ival in
+ let single_loc = Locations.make_loc loc_bits size in
+ let v = eval_one_loc single_loc in
+ if Cvalue.V.intersects v value
+ then Locations.Location_Bits.join loc_bits acc_loc, Cvalue.V.join v acc_val
+ else acc
+ in
+ let fold_ival base ival acc =
+ if Ival.cardinal_is_less_than ival upto
+ then Ival.fold_enum (process_ival base) ival acc
+ else process_ival base ival acc
+ in
+ let fold_location loc acc =
+ try
+ let loc = loc.Locations.loc in
+ Locations.Location_Bits.fold_i fold_ival loc acc
+ with
+ Abstract_interp.Error_Top -> loc.Locations.loc, value
+ in
+ let acc = Locations.Location_Bits.bottom, Cvalue.V.bottom in
+ let loc_bits, value = fold_location loc acc in
+ if Locations.Location_Bits.is_bottom loc_bits
+ then `Bottom
+ else
+ let loc = Precise_locs.inject_location_bits loc_bits in
+ `Value (Precise_locs.make_precise_loc loc ~size, value)
+
+ let reduce_further _state _expr _value = []
+end
+
+include Queries
+
+(* -------------------------------------------------------------------------- *)
+(* Evaluation engine for the cvalue domain *)
+(* -------------------------------------------------------------------------- *)
+
+module Value = struct
+ module Internal = struct
+ include Main_values.CVal
+ let structure = Abstract.Value.Leaf (key, (module Main_values.CVal))
+ end
+ include Internal
+ include Structure.Open (Abstract.Value) (Internal)
+ let reduce t = t
+end
+
+module Domain = struct
+ include Cvalue.Model
+ include Queries
+end
+
+include Evaluation.Make (Value) (Main_locations.PLoc) (Domain)
+
+let lval_to_loc state lval =
+ let eval, _alarms = lvaluate ~for_writing:false state lval in
+ match eval with
+ | `Bottom -> Locations.loc_bottom
+ | `Value (_valuation, ploc, _typ) -> Precise_locs.imprecise_location ploc
diff --git a/src/plugins/eva/register.mli b/src/plugins/eva/domains/cvalue/cvalue_queries.mli
similarity index 71%
rename from src/plugins/eva/register.mli
rename to src/plugins/eva/domains/cvalue/cvalue_queries.mli
index 3898a7c5ac07923fdae7ad7914c1dcbd1322a25b..e6f423f25439ab77a9e34a23988997122a5e948e 100644
--- a/src/plugins/eva/register.mli
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.mli
@@ -20,9 +20,18 @@
(* *)
(**************************************************************************)
-(** Functions of the Value plugin registered in {!Db}. Only three functions
- are exported. *)
+(** Implementation of domain queries for the cvalue domain. *)
+include Abstract_domain.Queries
+ with type state = Cvalue.Model.t
+ and type value = Main_values.CVal.t
+ and type location = Main_locations.PLoc.location
+ and type origin = Main_values.CVal.t
-val eval_deps : Cvalue_domain.State.t -> Cil_types.exp -> Locations.Zone.t
-val eval_deps_lval : Cvalue_domain.State.t -> Cil_types.lval -> Locations.Zone.t
-val eval_deps_addr : Cvalue_domain.State.t -> Cil_types.lval -> Locations.Zone.t
+(** Evaluation engine specific to the cvalue domain. *)
+include Evaluation_sig.S with type state := state
+ and type value := value
+ and type loc := location
+ and type origin := origin
+
+(** Evaluates the location of a lvalue in a given cvalue state. *)
+val lval_to_loc: state -> Cil_types.lval -> Locations.location
diff --git a/src/plugins/eva/domains/cvalue/locals_scoping.ml b/src/plugins/eva/domains/cvalue/locals_scoping.ml
index ce41844e798d31a73797da73a637810395c92398..2e263ae8d1f369514c6351153e9628b3e8b0bc62 100644
--- a/src/plugins/eva/domains/cvalue/locals_scoping.ml
+++ b/src/plugins/eva/domains/cvalue/locals_scoping.ml
@@ -27,9 +27,9 @@ type clobbered_set = {
mutable clob: Base.SetLattice.t
}
-let structural_descr =
+let packed_descr =
let open Structural_descr in
- t_record [| Base.SetLattice.packed_descr |]
+ pack (t_record [| Base.SetLattice.packed_descr |])
let bottom () = { clob = Base.SetLattice.bottom }
let top () = { clob = Base.SetLattice.top }
diff --git a/src/plugins/eva/domains/cvalue/locals_scoping.mli b/src/plugins/eva/domains/cvalue/locals_scoping.mli
index 274e3ea64d0991b14b936e847a82cbeaec21750f..abaf168a64d782eb7106b29bde409b2099d48271 100644
--- a/src/plugins/eva/domains/cvalue/locals_scoping.mli
+++ b/src/plugins/eva/domains/cvalue/locals_scoping.mli
@@ -30,7 +30,7 @@ type clobbered_set = {
mutable clob: Base.SetLattice.t
}
-val structural_descr: Structural_descr.t
+val packed_descr: Structural_descr.pack
val bottom: unit -> clobbered_set
val top: unit -> clobbered_set
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index a93c6903e27d182ab6bc564fa6a3b82ae951c8ad..6bbfef27ba4dc1a948398cb182431dd2c0fda689 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -187,6 +187,8 @@ let cvalue_initial_state () =
let _, lib_entry = Globals.entry_point () in
G.get_cvalue_or_bottom (A.initial_state ~lib_entry)
+let () = Db.Value.initial_state_only_globals := cvalue_initial_state
+
(* Builds the Analyzer module corresponding to a given configuration,
and sets it as the current analyzer. *)
let make_analyzer config =
@@ -207,6 +209,12 @@ let reset_analyzer () =
if not (Abstractions.Config.equal config (fst !ref_analyzer))
then make_analyzer config
+(* Resets the Analyzer when the current project is changed. *)
+let () =
+ Project.register_after_set_current_hook
+ ~user_only:true (fun _ -> reset_analyzer ());
+ Project.register_after_global_load_hook reset_analyzer
+
(* Builds the analyzer if needed, and run the analysis. *)
let force_compute () =
Ast.compute ();
@@ -230,8 +238,12 @@ let compute =
let name = "Eva.Analysis.compute" in
fst (State_builder.apply_once name [ Self.state ] compute)
-(* Resets the Analyzer when the current project is changed. *)
-let () =
- Project.register_after_set_current_hook
- ~user_only:true (fun _ -> reset_analyzer ());
- Project.register_after_global_load_hook reset_analyzer
+let () = Db.Value.compute := compute
+let () = Parameters.ForceValues.set_output_dependencies [Self.state]
+
+let main () =
+ (* Value computations *)
+ if Parameters.ForceValues.get () then compute ();
+ if is_computed () then Red_statuses.report ()
+
+let () = Db.Main.extend main
diff --git a/src/plugins/eva/engine/analysis.mli b/src/plugins/eva/engine/analysis.mli
index 8dd74f365d0902882070a351b18b404853d35eef..fe482f514af1c500e3757d6505f5dc40adc3c5f7 100644
--- a/src/plugins/eva/engine/analysis.mli
+++ b/src/plugins/eva/engine/analysis.mli
@@ -154,6 +154,3 @@ val use_spec_instead_of_definition: Cil_types.kernel_function -> bool
to known whether results are available for a given function. *)
val save_results: Cil_types.kernel_function -> bool
[@@@ api_end]
-
-val cvalue_initial_state: unit -> Cvalue.Model.t
-(** Return the initial state of the cvalue domain only. *)
diff --git a/src/plugins/eva/register.ml b/src/plugins/eva/register.ml
deleted file mode 100644
index 7fd5081fe77c76679b400b083619f092d505611e..0000000000000000000000000000000000000000
--- a/src/plugins/eva/register.ml
+++ /dev/null
@@ -1,367 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* 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
-open Locations
-
-let () = Db.Value.compute := Analysis.compute
-let () = Parameters.ForceValues.set_output_dependencies [Self.state]
-
-let main () =
- (* Value computations *)
- if Parameters.ForceValues.get () then Analysis.compute ();
- if Analysis.is_computed () then Red_statuses.report ()
-
-let () = Db.Main.extend main
-
-(* -------------------------------------------------------------------------- *)
-(* Register Evaluation Functions *)
-(* -------------------------------------------------------------------------- *)
-
-open Eval
-
-module CVal = struct
- include Main_values.CVal
- let structure = Abstract.Value.Leaf (key, (module Main_values.CVal))
-end
-
-module Val = struct
- include CVal
- include Structure.Open (Abstract.Value) (CVal)
- let reduce t = t
-end
-
-module Eva =
- Evaluation.Make
- (Val)
- (Main_locations.PLoc)
- (Cvalue_domain.State)
-
-let inject_cvalue state = state, Locals_scoping.bottom ()
-
-let bot_value = function
- | `Bottom -> Cvalue.V.bottom
- | `Value v -> v
-
-let bot_state = function
- | `Bottom -> Cvalue.Model.bottom
- | `Value s -> s
-
-let update valuation state =
- let domain_valuation = Eva.to_domain_valuation valuation in
- bot_state (Cvalue_domain.State.update domain_valuation state >>-: fst)
-
-let rec eval_deps state e =
- match e.enode with
- | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ | Const _ ->
- Locations.Zone.bottom
- | Lval lv -> eval_deps_lval state lv
- | BinOp (_,e1,e2,_) ->
- Locations.Zone.join (eval_deps state e1) (eval_deps state e2)
- | CastE (_,e) | UnOp (_,e,_) ->
- eval_deps state e
- | AddrOf lv | StartOf lv -> eval_deps_addr state lv
-and eval_deps_lval state lv =
- let for_writing = false in
- let deps = eval_deps_addr state lv in
- let loc =
- fst (Eva.lvaluate ~for_writing state lv)
- >>-: fun (_valuation, loc, _typ) -> loc
- in
- match loc with
- | `Bottom -> deps
- | `Value loc ->
- let deps_lv = Precise_locs.enumerate_valid_bits Read loc in
- Locations.Zone.join deps deps_lv
-and eval_deps_addr state (h, o:lval) =
- Locations.Zone.join (eval_deps_host state h) (eval_deps_offset state o)
-and eval_deps_host state h = match h with
- | Var _ -> Locations.Zone.bottom
- | Mem e -> eval_deps state e
-and eval_deps_offset state o = match o with
- | NoOffset -> Locations.Zone.bottom
- | Field (_, o) -> eval_deps_offset state o
- | Index (i, o) ->
- Locations.Zone.join (eval_deps state i) (eval_deps_offset state o)
-
-let notify_opt with_alarms alarms =
- Option.iter (fun mode -> Alarmset.notify mode alarms) with_alarms
-
-let eval_expr_with_valuation ?with_alarms deps state expr=
- let state = inject_cvalue state in
- let deps = match deps with
- | None -> None
- | Some deps ->
- let deps' = eval_deps state expr in
- Some (Locations.Zone.join deps' deps)
- in
- let eval, alarms = Eva.evaluate state expr in
- notify_opt with_alarms alarms;
- match eval with
- | `Bottom -> (Cvalue.Model.bottom, deps, Cvalue.V.bottom), None
- | `Value (valuation, result) ->
- let state = update valuation state in
- (state, deps, result), Some valuation
-
-(* Compatibility layer between the old API of eval_exprs and the new evaluation
- scheme. *)
-module Eval = struct
-
- let eval_expr ?with_alarms state expr =
- let state = inject_cvalue state in
- let eval, alarms = Eva.evaluate ~reduction:false state expr in
- notify_opt with_alarms alarms;
- bot_value (eval >>-: snd)
-
- let eval_lval ?with_alarms deps state lval =
- let expr = Eva_utils.lval_to_exp lval in
- let res, valuation = eval_expr_with_valuation ?with_alarms deps state expr in
- let typ = match valuation with
- | None -> Cil.typeOfLval lval
- | Some valuation -> match Eva.Valuation.find_loc valuation lval with
- | `Value record -> record.typ
- | `Top -> Cil.typeOfLval lval
- in
- let state, deps, v = res in
- state, deps, v, typ
-
- let eval_expr_with_deps_state ?with_alarms deps state expr =
- fst (eval_expr_with_valuation ?with_alarms deps state expr)
-
-
- let reduce_by_cond state expr positive =
- let state = inject_cvalue state in
- let eval, _alarms =
- Eva.reduce state expr positive
- in
- bot_state (eval >>-: fun valuation -> update valuation state)
-
-
- let lval_to_precise_loc_deps_state ?with_alarms ~deps state ~reduce_valid_index:(_:bool) lval =
- if not (Cvalue.Model.is_reachable state)
- then state, deps, Precise_locs.loc_bottom, (Cil.typeOfLval lval)
- else
- let state = inject_cvalue state in
- let deps = match deps with
- | None -> None
- | Some deps ->
- let deps' = eval_deps_addr state lval in
- Some (Locations.Zone.join deps' deps)
- in
- let eval, alarms =
- Eva.lvaluate ~for_writing:false state lval
- in
- notify_opt with_alarms alarms;
- match eval with
- | `Bottom -> Cvalue.Model.bottom, deps, Precise_locs.loc_bottom, (Cil.typeOfLval lval)
- | `Value (valuation, loc, typ) -> update valuation state, deps, loc, typ
-
- let lval_to_loc_deps_state ?with_alarms ~deps state ~reduce_valid_index lv =
- let state, deps, pl, typ =
- lval_to_precise_loc_deps_state
- ?with_alarms ~deps state ~reduce_valid_index lv
- in
- state, deps, Precise_locs.imprecise_location pl, typ
-
- let lval_to_precise_loc_state ?with_alarms state lv =
- let state, _, r, typ =
- lval_to_precise_loc_deps_state
- ?with_alarms ~deps:None ~reduce_valid_index:(Kernel.SafeArrays.get ())
- state lv
- in
- state, r, typ
-
- and lval_to_loc_state ?with_alarms state lv =
- let state, _, r, typ =
- lval_to_loc_deps_state
- ?with_alarms ~deps:None ~reduce_valid_index:(Kernel.SafeArrays.get ())
- state lv
- in
- state, r, typ
-
- let lval_to_precise_loc ?with_alarms state lv =
- let _, r, _typ = lval_to_precise_loc_state ?with_alarms state lv in
- r
-
- let lval_to_loc ?with_alarms state lv =
- let _, r, _typ = lval_to_loc_state ?with_alarms state lv in
- r
-
-
- let resolv_func_vinfo ?with_alarms deps state funcexp =
- let open Cil_types in
- let state = inject_cvalue state in
- let deps = match funcexp.enode with
- | Lval (Var _, NoOffset) -> deps
- | Lval (Mem v, _) ->
- begin match deps with
- | None -> None
- | Some deps ->
- let deps' = eval_deps state v in
- Some (Locations.Zone.join deps' deps)
- end
- | _ -> assert false
- in
- let kfs, alarms = Eva.eval_function_exp funcexp state in
- notify_opt with_alarms alarms;
- let kfs = match kfs with
- | `Bottom -> Kernel_function.Hptset.empty
- | `Value kfs ->
- List.fold_left
- (fun acc (kf, _) -> Kernel_function.Hptset.add kf acc)
- Kernel_function.Hptset.empty kfs
- in
- kfs, deps
-
-end
-
-module type Eval = module type of Eval
-
-(* Functions to register in Db.Value that depend on evaluation functions. *)
-module Export (Eval : Eval) = struct
-
- open Eval
-
- let lval_to_loc_with_deps_state ?with_alarms state ~deps lv =
- let _state, deps, r, _ =
- lval_to_loc_deps_state
- ?with_alarms
- ~deps:(Some deps)
- ~reduce_valid_index:(Kernel.SafeArrays.get ())
- state
- lv
- in
- Option.value ~default:Locations.Zone.bottom deps, r
-
- let lval_to_loc_with_deps kinstr ?with_alarms ~deps lv =
- let state = Db.Value.noassert_get_state kinstr in
- lval_to_loc_with_deps_state ?with_alarms state ~deps lv
-
- let lval_to_loc_kinstr kinstr ?with_alarms lv =
- let state = Db.Value.noassert_get_state kinstr in
- lval_to_loc ?with_alarms state lv
-
- let lval_to_precise_loc_with_deps_state_alarm ?with_alarms state ~deps lv =
- let _state, deps, ploc, _ =
- lval_to_precise_loc_deps_state ?with_alarms
- ~deps ~reduce_valid_index:(Kernel.SafeArrays.get ()) state lv
- in
- let deps = Option.value ~default:Locations.Zone.bottom deps in
- deps, ploc
-
- let lval_to_precise_loc_with_deps_state =
- lval_to_precise_loc_with_deps_state_alarm ?with_alarms:None
-
- let lval_to_zone kinstr ?with_alarms lv =
- let state_to_joined_zone state acc =
- let _, r =
- lval_to_precise_loc_with_deps_state_alarm ?with_alarms state ~deps:None lv
- in
- let zone = Precise_locs.enumerate_valid_bits Read r in
- Locations.Zone.join acc zone
- in
- Db.Value.fold_state_callstack
- state_to_joined_zone Locations.Zone.bottom ~after:false kinstr
-
- let lval_to_zone_state state lv =
- let _, r = lval_to_precise_loc_with_deps_state state ~deps:None lv in
- Precise_locs.enumerate_valid_bits Read r
-
- let lval_to_zone_with_deps_state state ~for_writing ~deps lv =
- let deps, r = lval_to_precise_loc_with_deps_state state ~deps lv in
- let r = (* No write effect if [lv] is const *)
- if for_writing && (Eva_utils.is_const_write_invalid (Cil.typeOfLval lv))
- then Precise_locs.loc_bottom
- else r
- in
- let access = if for_writing then Write else Read in
- let zone = Precise_locs.enumerate_valid_bits access r in
- let exact = Precise_locs.valid_cardinal_zero_or_one ~for_writing r in
- deps, zone, exact
-
-
- let lval_to_offsetmap_aux ?with_alarms state lv =
- let loc =
- Locations.valid_part Read
- (lval_to_loc ?with_alarms state lv)
- in
- match loc.Locations.size with
- | Int_Base.Top -> None
- | Int_Base.Value size ->
- match Cvalue.Model.copy_offsetmap loc.Locations.loc size state with
- | `Bottom -> None
- | `Value m -> Some m
-
- let lval_to_offsetmap kinstr ?with_alarms lv =
- let state = Db.Value.noassert_get_state kinstr in
- lval_to_offsetmap_aux ?with_alarms state lv
-
- let lval_to_offsetmap_state state lv =
- lval_to_offsetmap_aux state lv
-end
-
-
-module type Export = module type of (Export (Eval))
-
-let register (module Eval: Eval) (module Export: Export) =
- let open Export in
- Db.Value.eval_expr := Eval.eval_expr;
- Db.Value.eval_expr_with_state :=
- (fun ?with_alarms state expr ->
- let (s, _, v) =
- Eval.eval_expr_with_deps_state ?with_alarms None state expr
- in
- s, v);
- Db.Value.reduce_by_cond := Eval.reduce_by_cond;
- Db.Value.eval_lval :=
- (fun ?with_alarms deps state lval ->
- let _, deps, r, _ = Eval.eval_lval ?with_alarms deps state lval in
- deps, r);
- Db.Value.lval_to_loc_with_deps := lval_to_loc_with_deps;
- Db.Value.lval_to_loc_with_deps_state :=
- lval_to_loc_with_deps_state ?with_alarms:None;
- Db.Value.lval_to_loc := lval_to_loc_kinstr;
- Db.Value.lval_to_loc_state := Eval.lval_to_loc ?with_alarms:None;
- Db.Value.lval_to_zone_state := lval_to_zone_state;
- Db.Value.lval_to_zone := lval_to_zone;
- Db.Value.lval_to_zone_with_deps_state := lval_to_zone_with_deps_state;
- Db.Value.lval_to_precise_loc_state := Eval.lval_to_precise_loc_state;
- Db.Value.lval_to_precise_loc_with_deps_state :=
- lval_to_precise_loc_with_deps_state;
- Db.Value.lval_to_offsetmap := lval_to_offsetmap;
- Db.Value.lval_to_offsetmap_state := lval_to_offsetmap_state;
- ()
-
-
-let () = Db.Value.initial_state_only_globals := Analysis.cvalue_initial_state
-
-let () =
- let eval = (module Eval : Eval) in
- let export = (module Export ((val eval : Eval)) : Export) in
- register eval export;;
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/plugins/eva/utils/widen.ml b/src/plugins/eva/utils/widen.ml
index 2e4564b4ef0045ac2a79a43c30aacd65a2b2687f..b26bb71371f86aef95114f2fda4217a5348188b6 100644
--- a/src/plugins/eva/utils/widen.ml
+++ b/src/plugins/eva/utils/widen.ml
@@ -499,7 +499,7 @@ module Parsed_Dynamic_Hints =
let dynamic_bases_of_lval states e offset =
let lv = (Mem e, offset) in
List.fold_left (fun acc' state ->
- let location = !Db.Value.lval_to_loc_state state lv in
+ let location = Cvalue_queries.lval_to_loc state lv in
Locations.Location_Bits.fold_bases
(fun base acc'' -> Base.Hptset.add base acc'')
location.Locations.loc acc'