From 49c674da4b4d3d83c896383e232e38afa11a64ea Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 8 Mar 2024 23:19:36 +0100
Subject: [PATCH] [Eva] remove types from records and arguments for lvalues
---
src/plugins/eva/domains/abstract_domain.ml | 10 +--
src/plugins/eva/domains/apron/apron_domain.ml | 11 +--
.../eva/domains/cvalue/cvalue_domain.ml | 8 +--
.../eva/domains/cvalue/cvalue_queries.ml | 30 ++++-----
.../eva/domains/cvalue/cvalue_transfer.ml | 30 ++++-----
src/plugins/eva/domains/domain_builder.ml | 18 ++---
src/plugins/eva/domains/domain_builder.mli | 2 +-
src/plugins/eva/domains/domain_lift.ml | 9 ++-
src/plugins/eva/domains/domain_product.ml | 12 ++--
.../eva/domains/equality/equality_domain.ml | 2 +-
.../eva/domains/gauges/gauges_domain.ml | 13 ++--
src/plugins/eva/domains/inout_domain.ml | 2 +-
.../eva/domains/multidim/multidim_domain.ml | 8 +--
src/plugins/eva/domains/octagons.ml | 4 +-
src/plugins/eva/domains/offsm_domain.ml | 6 +-
src/plugins/eva/domains/printer_domain.ml | 2 +-
src/plugins/eva/domains/simple_memory.ml | 16 ++---
src/plugins/eva/domains/simpler_domains.ml | 2 +-
src/plugins/eva/domains/symbolic_locs.ml | 4 +-
src/plugins/eva/domains/taint_domain.ml | 2 +-
src/plugins/eva/domains/traces_domain.ml | 4 +-
src/plugins/eva/domains/unit_domain.ml | 2 +-
src/plugins/eva/engine/analysis.ml | 2 +-
src/plugins/eva/engine/evaluation.ml | 67 ++++++++++---------
src/plugins/eva/engine/evaluation_sig.ml | 3 +-
src/plugins/eva/engine/initialization.ml | 2 +-
.../eva/engine/subdivided_evaluation.ml | 10 ++-
src/plugins/eva/engine/transfer_stmt.ml | 26 +++----
src/plugins/eva/eval.ml | 2 -
src/plugins/eva/eval.mli | 2 -
src/plugins/eva/utils/results.ml | 4 +-
31 files changed, 155 insertions(+), 160 deletions(-)
diff --git a/src/plugins/eva/domains/abstract_domain.ml b/src/plugins/eva/domains/abstract_domain.ml
index 6dbc334ca20..99782c18153 100644
--- a/src/plugins/eva/domains/abstract_domain.ml
+++ b/src/plugins/eva/domains/abstract_domain.ml
@@ -174,22 +174,22 @@ module type Queries = sig
state -> exp -> (value * origin option) evaluated
(** Query function for lvalues:
- [extract_lval ~oracle context t lval typ loc] returns the known value
- stored at the location [loc] of the left value [lval] of type [typ].
+ [extract_lval ~oracle context t lval loc] returns the known value
+ stored at the location [loc] of the left value [lval].
See above for more details on queries. *)
val extract_lval :
oracle:(exp -> value evaluated) -> evaluation_context ->
- state -> lval -> typ -> location -> (value * origin option) evaluated
+ state -> lval -> location -> (value * origin option) evaluated
(** [backward_location state lval typ loc v] reduces the location [loc] of the
- lvalue [lval] of type [typ], so that only the locations that may have value
+ lvalue [lval], so that only the locations that may have value
[v] are kept.
The returned location must be included in [loc], but it is always sound
to return [loc] itself.
Also returns the value that may have the returned location, if not bottom.
Defined by {!Domain_builder.Complete} with no reduction. *)
val backward_location :
- state -> lval -> typ -> location -> value -> (location * value) or_bottom
+ state -> lval -> location -> value -> (location * value) or_bottom
(** Given a reduction [expr] = [value], provides more reductions that may
be performed.
diff --git a/src/plugins/eva/domains/apron/apron_domain.ml b/src/plugins/eva/domains/apron/apron_domain.ml
index 751103832d6..6f654989a77 100644
--- a/src/plugins/eva/domains/apron/apron_domain.ml
+++ b/src/plugins/eva/domains/apron/apron_domain.ml
@@ -469,7 +469,7 @@ module Make (Man : Input) = struct
let dummy_oracle _ exn = raise exn
- let compute state expr typ =
+ let compute state expr =
let top = `Value (None, None), Alarmset.all in
if not (is_relevant expr)
then top
@@ -477,6 +477,7 @@ module Make (Man : Input) = struct
try
let eval = make_eval state in
let oracle = dummy_oracle in
+ let typ = expr.typ in
let exp = coerce eval typ (translate_expr_linearize eval oracle expr) in
let interval = eval exp in
let interval = truncate_interval typ interval in
@@ -495,11 +496,11 @@ module Make (Man : Input) = struct
| Z.Overflow | Failure _ -> top
let extract_expr ~oracle:_ _context state expr =
- compute state expr expr.typ
+ compute state expr
- let extract_lval ~oracle:_ _context state lval typ _loc =
+ let extract_lval ~oracle:_ _context state lval _loc =
let expr = Evast_builder.lval lval in
- compute state expr typ
+ compute state expr
let maybe_bottom state =
if Abstract1.is_bottom man state
@@ -606,7 +607,7 @@ module Make (Man : Input) = struct
let var = translate_lval lvalue.lval in
let expr = expr in
let exp = translate_expr_linearize eval oracle expr in
- let exp = coerce eval lvalue.ltyp exp in
+ let exp = coerce eval lvalue.lval.typ exp in
let exp = Texpr1.of_expr (Abstract1.env state) exp in
(* TODO: currently, all variables are present in the environment
at all times. Change to a dynamic environment, in which new
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 4a28b113809..3cb92596251 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -77,11 +77,11 @@ module State = struct
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_lval ~oracle context (state, _) lval loc =
+ Cvalue_queries.extract_lval ~oracle context state lval loc
- let backward_location (state, _) lval typ precise_loc value =
- Cvalue_queries.backward_location state lval typ precise_loc value
+ let backward_location (state, _) lval precise_loc value =
+ Cvalue_queries.backward_location state lval precise_loc value
let reduce_further (state, _) expr value =
Cvalue_queries.reduce_further state expr value
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.ml b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
index dc29f792434..132dd760ff5 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_queries.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
@@ -56,7 +56,7 @@ module Queries = struct
| C_init_noesc _ -> Alarmset.none
- let eval_one_loc state lval typ =
+ let eval_one_loc state lval =
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
@@ -70,7 +70,7 @@ module Queries = struct
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
+ let result = Cvalue_forward.make_volatile ~typ:lval.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
@@ -82,8 +82,8 @@ module Queries = struct
| Cvalue.V.Top (bases, origin) -> Origin.register_read bases origin
| _ -> ()
- let extract_scalar_lval state lval typ loc =
- let process_one_loc = eval_one_loc state lval typ in
+ let extract_scalar_lval state lval loc =
+ let process_one_loc = eval_one_loc state lval 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
@@ -91,9 +91,9 @@ module Queries = struct
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 incompatible_type = is_float value <> Cil.isFloatingType lval.typ in
let origin = if incompatible_type then Some value else None in
- let value = Cvalue_forward.reinterpret typ value in
+ let value = Cvalue_forward.reinterpret lval.typ value in
read_garbled_mix value;
if Cvalue.V.is_bottom value
then `Bottom, alarms
@@ -101,7 +101,7 @@ module Queries = struct
(* 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 extract_aggregate_lval state lval ploc =
let loc = Precise_locs.imprecise_location ploc in
match loc.Locations.size with
| Int_Base.Top -> `Value (Cvalue.V.top, None), Alarmset.all
@@ -117,19 +117,19 @@ module Queries = struct
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 extract_lval ~oracle:_ _context state lval loc =
+ if Cil.isArithmeticOrPointerType lval.Evast.typ
+ then extract_scalar_lval state lval loc
+ else extract_aggregate_lval state lval loc
- let backward_location state _lval typ precise_loc value =
+ let backward_location state lval 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
+ let v = Cvalue_forward.make_volatile ~typ:lval.Evast.typ v in
+ Cvalue_forward.reinterpret lval.typ v
in
let process_ival base ival (acc_loc, acc_val as acc) =
let loc_bits = Locations.Location_Bits.inject base ival in
@@ -190,4 +190,4 @@ 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
+ | `Value (_valuation, ploc) -> Precise_locs.imprecise_location ploc
diff --git a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
index b77e15acd93..938b3b82daf 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
@@ -118,11 +118,11 @@ let update valuation t =
(* Assignments *)
(* ---------------------------------------------------------------------- *)
-let write_abstract_value state (lval, loc, typ) assigned_value =
+let write_abstract_value state (lval, loc) assigned_value =
let {v; initialized; escaping} = assigned_value in
let value = unbottomize v in
let value =
- if Cil.typeHasQualifier "volatile" typ
+ if Cil.typeHasQualifier "volatile" lval.typ
then Cvalue_forward.make_volatile value
else value
in
@@ -134,16 +134,16 @@ let write_abstract_value state (lval, loc, typ) assigned_value =
exception Do_assign_imprecise_copy
let copy_one_loc state left_lv right_lv =
- let left_lval, left_loc, left_typ = left_lv
- and _right_lval, right_loc, right_typ = right_lv in
+ let left_lval, left_loc = left_lv
+ and right_lval, right_loc = right_lv in
(* top size is tested before this function is called, in which case
the imprecise copy mode is used. *)
let size = Int_Base.project right_loc.Locations.size in
let right_loc = right_loc.Locations.loc in
let offsetmap = Cvalue.Model.copy_offsetmap right_loc size state in
let make_volatile =
- Cil.typeHasQualifier "volatile" left_typ ||
- Cil.typeHasQualifier "volatile" right_typ
+ Cil.typeHasQualifier "volatile" left_lval.typ ||
+ Cil.typeHasQualifier "volatile" right_lval.typ
in
match offsetmap with
| `Bottom -> `Bottom
@@ -156,7 +156,7 @@ let copy_one_loc state left_lv right_lv =
(Cvalue.V_Or_Uninitialized.map Cvalue_forward.make_volatile) offsm
else offsm
in
- if not (Eval_typ.offsetmap_matches_type left_typ offsetmap) then
+ if not (Eval_typ.offsetmap_matches_type left_lval.typ offsetmap) then
raise Do_assign_imprecise_copy;
warn_imprecise_offsm_write left_lval offsetmap;
`Value
@@ -167,20 +167,20 @@ let make_determinate value =
{ v = `Value value; initialized = true; escaping = false }
let copy_right_lval state left_lv right_lv copied_value =
- let lval, loc, typ = left_lv in
+ let lval, loc = left_lv in
(* Size mismatch between left and right size, or imprecise size.
This cannot be done by copies, but require a conversion *)
let right_size = Main_locations.PLoc.size right_lv.lloc
and left_size = Main_locations.PLoc.size loc in
if not (Int_Base.equal left_size right_size) || Int_Base.is_top right_size
then
- fun loc -> write_abstract_value state (lval, loc, typ) copied_value
+ fun loc -> write_abstract_value state (lval, loc) copied_value
else
fun loc ->
try
let process right_loc acc =
- let left_lv = lval, loc, typ
- and right_lv = right_lv.lval, right_loc, right_lv.ltyp in
+ let left_lv = lval, loc
+ and right_lv = right_lv.lval, right_loc in
match copy_one_loc state left_lv right_lv with
| `Bottom -> acc
| `Value state -> Cvalue.Model.join acc state
@@ -188,17 +188,17 @@ let copy_right_lval state left_lv right_lv copied_value =
Precise_locs.fold process right_lv.lloc Cvalue.Model.bottom
with
Do_assign_imprecise_copy ->
- write_abstract_value state (lval, loc, typ) copied_value
+ write_abstract_value state (lval, loc) copied_value
-let assign _stmt { lval; ltyp; lloc } _expr assigned valuation state =
+let assign _stmt { lval; lloc } _expr assigned valuation state =
let state = update valuation state in
let assign_one_loc =
match assigned with
| Assign value ->
let assigned_value = make_determinate value in
- fun loc -> write_abstract_value state (lval, loc, ltyp) assigned_value
+ fun loc -> write_abstract_value state (lval, loc) assigned_value
| Copy (right_lv, copied_value) ->
- copy_right_lval state (lval, lloc, ltyp) right_lv copied_value
+ copy_right_lval state (lval, lloc) right_lv copied_value
in
let aux_loc loc acc_state =
let s = assign_one_loc loc in
diff --git a/src/plugins/eva/domains/domain_builder.ml b/src/plugins/eva/domains/domain_builder.ml
index 5f717fd6f54..846e1cb5b5e 100644
--- a/src/plugins/eva/domains/domain_builder.ml
+++ b/src/plugins/eva/domains/domain_builder.ml
@@ -40,7 +40,7 @@ module type LeafDomain = sig
val context_dependencies: context Abstract_context.dependencies
val build_context: t -> context or_bottom
- val backward_location: t -> lval -> typ -> 'loc -> 'v -> ('loc * 'v) or_bottom
+ val backward_location: t -> lval -> 'loc -> 'v -> ('loc * 'v) or_bottom
val reduce_further: t -> exp -> 'v -> (exp * 'v) list
val evaluate_predicate:
@@ -76,7 +76,7 @@ module Complete (Domain: InputDomain) = struct
let context_dependencies = Abstract_context.Leaf (module Unit_context)
let build_context _ = `Value ()
- let backward_location _state _lval _typ loc value = `Value (loc, value)
+ let backward_location _state _lval loc value = `Value (loc, value)
let reduce_further _state _expr _value = []
let evaluate_predicate _env _state _predicate = Alarmset.Unknown
@@ -139,7 +139,7 @@ module Make_Minimal
let top_answer = `Value (Value.top, None), Alarmset.all
let extract_expr ~oracle:_ _context _state _expr = top_answer
- let extract_lval ~oracle:_ _context _state _lval _typ _location = top_answer
+ let extract_lval ~oracle:_ _context _state _lval _location = top_answer
let update _valuation state = `Value state
@@ -256,8 +256,8 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
let v = Domain.extract_expr state expr >>-: fun v -> v, None in
v, Alarmset.all
- let extract_lval ~oracle:_ _context state lval typ location =
- let v = Domain.extract_lval state lval typ location >>-: fun v -> v, None in
+ let extract_lval ~oracle:_ _context state lval location =
+ let v = Domain.extract_lval state lval location >>-: fun v -> v, None in
v, Alarmset.all
let find valuation expr =
@@ -448,16 +448,16 @@ module Restrict
make_query default_query
(fun s -> Domain.extract_expr ~oracle context s expr) state
- let extract_lval ~oracle context state lval typ location =
+ let extract_lval ~oracle context state lval location =
make_query
default_query
- (fun s -> Domain.extract_lval ~oracle context s lval typ location)
+ (fun s -> Domain.extract_lval ~oracle context s lval location)
state
- let backward_location state lval typ location value =
+ let backward_location state lval location value =
make_query
(`Value (location, value))
- (fun s -> Domain.backward_location s lval typ location value)
+ (fun s -> Domain.backward_location s lval location value)
state
let reduce_further state expr value =
diff --git a/src/plugins/eva/domains/domain_builder.mli b/src/plugins/eva/domains/domain_builder.mli
index a78eeeee220..b7d44a0cf73 100644
--- a/src/plugins/eva/domains/domain_builder.mli
+++ b/src/plugins/eva/domains/domain_builder.mli
@@ -44,7 +44,7 @@ module type LeafDomain = sig
val context_dependencies: context Abstract_context.dependencies
val build_context: t -> context or_bottom
- val backward_location: t -> lval -> typ -> 'loc -> 'v -> ('loc * 'v) or_bottom
+ val backward_location: t -> lval -> 'loc -> 'v -> ('loc * 'v) or_bottom
val reduce_further: t -> exp -> 'v -> (exp * 'v) list
val evaluate_predicate:
diff --git a/src/plugins/eva/domains/domain_lift.ml b/src/plugins/eva/domains/domain_lift.ml
index 90f11ac2bca..9f09c83beec 100644
--- a/src/plugins/eva/domains/domain_lift.ml
+++ b/src/plugins/eva/domains/domain_lift.ml
@@ -58,16 +58,15 @@ module Make
Domain.extract_expr ~oracle context state exp >>=: fun (value, origin) ->
Val.extend value, origin
- let extract_lval ~oracle context state lval typ loc =
+ let extract_lval ~oracle context state lval loc =
let oracle exp = oracle exp >>=: Val.restrict in
let loc = Loc.restrict loc in
- Domain.extract_lval ~oracle context state lval typ loc
+ Domain.extract_lval ~oracle context state lval loc
>>=: fun (value, origin) ->
Val.extend value, origin
- let backward_location state lval typ loc value =
- Domain.backward_location
- state lval typ (Loc.restrict loc) (Val.restrict value)
+ let backward_location state lval loc value =
+ Domain.backward_location state lval (Loc.restrict loc) (Val.restrict value)
>>-: fun (loc, value) ->
Loc.extend loc, Val.extend value
diff --git a/src/plugins/eva/domains/domain_product.ml b/src/plugins/eva/domains/domain_product.ml
index fdf4ab1eeea..db19d576453 100644
--- a/src/plugins/eva/domains/domain_product.ml
+++ b/src/plugins/eva/domains/domain_product.ml
@@ -103,15 +103,15 @@ module Make
(Left.extract_expr ~oracle context left expr)
(Right.extract_expr ~oracle context right expr)
- let extract_lval ~oracle context (left, right) lval typ location =
+ let extract_lval ~oracle context (left, right) lval location =
merge
- (Left.extract_lval ~oracle context left lval typ location)
- (Right.extract_lval ~oracle context right lval typ location)
+ (Left.extract_lval ~oracle context left lval location)
+ (Right.extract_lval ~oracle context right lval location)
- let backward_location (left, right) lval typ loc value =
+ let backward_location (left, right) lval loc value =
(* TODO: Loc.narrow *)
- Left.backward_location left lval typ loc value >>- fun (loc, value1) ->
- Right.backward_location right lval typ loc value >>- fun (loc, value2) ->
+ Left.backward_location left lval loc value >>- fun (loc, value1) ->
+ Right.backward_location right lval loc value >>- fun (loc, value2) ->
Value.narrow value1 value2 >>-: fun value ->
loc, value
diff --git a/src/plugins/eva/domains/equality/equality_domain.ml b/src/plugins/eva/domains/equality/equality_domain.ml
index ede5722da83..cc6cd8afeee 100644
--- a/src/plugins/eva/domains/equality/equality_domain.ml
+++ b/src/plugins/eva/domains/equality/equality_domain.ml
@@ -244,7 +244,7 @@ struct
let atom_e = HCE.of_exp expr in
coop_eval oracle equalities atom_e
- let extract_lval ~oracle _context (equalities, _, _) lval _typ _location =
+ let extract_lval ~oracle _context (equalities, _, _) lval _location =
let atom_lv = HCE.of_lval lval in
coop_eval oracle equalities atom_lv
diff --git a/src/plugins/eva/domains/gauges/gauges_domain.ml b/src/plugins/eva/domains/gauges/gauges_domain.ml
index 6715362e591..0fc87c677e8 100644
--- a/src/plugins/eva/domains/gauges/gauges_domain.ml
+++ b/src/plugins/eva/domains/gauges/gauges_domain.ml
@@ -20,6 +20,7 @@
(* *)
(**************************************************************************)
+open Evast
open Eval
type function_calls =
@@ -991,7 +992,7 @@ module G = struct
with Not_found -> raise Untranslatable
let translate_exp state to_loc to_v e =
- let ptr_size (e : Evast.exp) =
+ let ptr_size e =
let typ_pointed = Cil.typeOf_pointed e.typ in
try Integer.of_int (Cil.bytesSizeOf typ_pointed)
with Cil.SizeOfError _ -> raise Untranslatable
@@ -999,7 +1000,7 @@ module G = struct
(* This function translates the expression as a precise gauge. For any
expression that cannot be handled, [Untranslatable] is raised. *)
let rec aux_gauge e =
- match (e : Evast.exp).node with
+ match e.node with
| Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
| AddrOf _ | StartOf _ ->
raise Untranslatable (* constant: using linearization directly *)
@@ -1096,7 +1097,7 @@ module G = struct
let assign to_loc to_v lv e state =
let loc = to_loc lv in
try
- let b = loc_to_base loc lv.Evast.typ in
+ let b = loc_to_base loc lv.typ in
let g = translate_exp state to_loc to_v e in
store_gauge b g state
with Untranslatable ->
@@ -1154,7 +1155,7 @@ module D : Abstract_domain.Leaf
let assume_exp valuation e r state =
if r.reductness = Created || r.reductness = Reduced then
- match (e : Evast.exp).node with
+ match e.node with
| Lval lv -> begin
match valuation.Abstract_domain.find_loc lv with
| `Top -> `Value state
@@ -1257,10 +1258,10 @@ module D : Abstract_domain.Leaf
let extract_expr ~oracle:_ _context _state _exp =
`Value (Cvalue.V.top, None), Alarmset.all
- let extract_lval ~oracle:_ _context state _lv typ loc =
+ let extract_lval ~oracle:_ _context state lv loc =
let v =
try
- let b = loc_to_base (Precise_locs.imprecise_location loc) typ in
+ let b = loc_to_base (Precise_locs.imprecise_location loc) lv.typ in
match extract_gauge state b with
| Some g -> eval_gauge state g
| None -> Cvalue.V.top
diff --git a/src/plugins/eva/domains/inout_domain.ml b/src/plugins/eva/domains/inout_domain.ml
index 65b07d9a920..cc971d86b03 100644
--- a/src/plugins/eva/domains/inout_domain.ml
+++ b/src/plugins/eva/domains/inout_domain.ml
@@ -263,7 +263,7 @@ module Domain = struct
let top_query = `Value (Cvalue.V.top, None), Alarmset.all
let extract_expr ~oracle:_ _context _state _expr = top_query
- let extract_lval ~oracle:_ _context _state _lv _typ _locs = top_query
+ let extract_lval ~oracle:_ _context _state _lv _locs = top_query
end
include Domain
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index 0564edd184e..94b7bc20a69 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -672,8 +672,8 @@ struct
let extract_expr ~oracle:_ _context _state _expr =
`Value (Value.top, None), Alarmset.all
- let extract_lval ~oracle _context state lv typ _loc =
- if Cil.isScalarType typ then
+ let extract_lval ~oracle _context state lv _loc =
+ if Cil.isScalarType lv.Evast.typ then
let oracle = fun exp ->
match oracle exp with
| `Value v, alarms when Alarmset.is_empty alarms -> v (* only use values safely evaluated *)
@@ -752,8 +752,8 @@ struct
| `Value src ->
overwrite ~oracle state dst src
- let assign _kinstr { lval=dst; ltyp } src assigned_value valuation state =
- if Int_Base.is_zero (Bit_utils.sizeof ltyp)
+ let assign _kinstr { lval=dst } src assigned_value valuation state =
+ if Int_Base.is_zero (Bit_utils.sizeof dst.typ)
then `Value state
else
let+ state = assume_valuation valuation state in
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index 500b474bb92..d6be2506a3a 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -1654,7 +1654,7 @@ module Domain = struct
then `Bottom, Alarmset.all
else `Value (Cvalue.V.inject_ival ival, None), alarms
- let extract_lval ~oracle:_ _context _t _lval _typ _loc = top_value
+ let extract_lval ~oracle:_ _context _t _lval _loc = top_value
let reduce_further state expr value =
match expr.node with
@@ -1801,7 +1801,7 @@ module Domain = struct
let assign kinstr left_value expr assigned valuation state =
if kinstr <> Cil_types.Kglobal
- && Cil.isIntegralOrPointerType left_value.ltyp
+ && Cil.isIntegralOrPointerType left_value.lval.typ
&& not (Evast_utils.lval_contains_volatile left_value.lval)
then assign_variable left_value.lval expr assigned valuation state
else
diff --git a/src/plugins/eva/domains/offsm_domain.ml b/src/plugins/eva/domains/offsm_domain.ml
index 806d306d6f7..3c845092e20 100644
--- a/src/plugins/eva/domains/offsm_domain.ml
+++ b/src/plugins/eva/domains/offsm_domain.ml
@@ -183,10 +183,10 @@ module D : Abstract_domain.Leaf
then Offsm_value.Offsm.top
else O o
- let extract_lval ~oracle:_ _context state _lv typ locs =
+ let extract_lval ~oracle:_ _context state lv locs =
let o =
- if Cil.typeHasQualifier "volatile" typ ||
- not (Cil.isArithmeticOrPointerType typ)
+ if Cil.typeHasQualifier "volatile" lv.Evast.typ ||
+ not (Cil.isArithmeticOrPointerType lv.Evast.typ)
then
`Value (Top, None)
else
diff --git a/src/plugins/eva/domains/printer_domain.ml b/src/plugins/eva/domains/printer_domain.ml
index 3dc5d69b088..d36a5b867e0 100644
--- a/src/plugins/eva/domains/printer_domain.ml
+++ b/src/plugins/eva/domains/printer_domain.ml
@@ -56,7 +56,7 @@ module Simple : Simpler_domains.Simple_Cvalue = struct
let extract_expr _state _exp =
`Value (Cvalue.V.top)
- let extract_lval _state _lval _typ _loc =
+ let extract_lval _state _lval _loc =
`Value (Cvalue.V.top)
(* --- Transfer functions --- *)
diff --git a/src/plugins/eva/domains/simple_memory.ml b/src/plugins/eva/domains/simple_memory.ml
index f094fd433cd..3c3719544c8 100644
--- a/src/plugins/eva/domains/simple_memory.ml
+++ b/src/plugins/eva/domains/simple_memory.ml
@@ -203,15 +203,15 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
(* This function returns the information known about the location
corresponding to [_lv], so that it may be used by the engine during
evaluation. *)
- let extract_lval ~oracle:_ _context state _lv typ loc =
- let v = find loc typ state in
+ let extract_lval ~oracle:_ _context state lv loc =
+ let v = find loc lv.Evast.typ state in
`Value (v, None), Alarmset.all
let extract_expr ~oracle:_ _context _state _expr =
`Value (Value.top, None), Alarmset.all
- let backward_location state _lval typ loc _value =
- let new_value = find loc typ state in
+ let backward_location state lval loc _value =
+ let new_value = find loc lval.Evast.typ state in
`Value (loc, new_value)
(* This function binds [loc] to [v], of type [typ], in [state].
@@ -233,9 +233,9 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
| Lval lv -> begin
match valuation.Abstract_domain.find_loc lv with
| `Top -> state
- | `Value {loc; typ} ->
+ | `Value {loc} ->
if Precise_locs.cardinal_zero_or_one loc
- then bind_loc loc typ record.value.v state
+ then bind_loc loc lv.typ record.value.v state
else state
end
| _ -> state
@@ -254,7 +254,7 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
(* Extract the abstract value *)
let value = Eval.value_assigned value in
(* Store the information [lv = e;] in the state *)
- let state = bind_loc lv.lloc lv.ltyp value state in
+ let state = bind_loc lv.lloc lv.lval.typ value state in
`Value state
let update valuation state = `Value (assume_valuation valuation state)
@@ -313,7 +313,7 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
begin
match valuation.Abstract_domain.find_loc lval with
| `Top -> ()
- | `Value {loc; typ} -> Value.pretty fmt (find loc typ state)
+ | `Value {loc} -> Value.pretty fmt (find loc lval.typ state)
end
| _ -> ()
diff --git a/src/plugins/eva/domains/simpler_domains.ml b/src/plugins/eva/domains/simpler_domains.ml
index 26228363be6..d207e51e5f6 100644
--- a/src/plugins/eva/domains/simpler_domains.ml
+++ b/src/plugins/eva/domains/simpler_domains.ml
@@ -116,7 +116,7 @@ module type Simple_Cvalue = sig
(** Query functions. *)
val extract_expr: t -> exp -> cvalue or_bottom
- val extract_lval: t -> lval -> typ -> precise_loc -> cvalue or_bottom
+ val extract_lval: t -> lval -> precise_loc -> cvalue or_bottom
(** Transfer functions. *)
diff --git a/src/plugins/eva/domains/symbolic_locs.ml b/src/plugins/eva/domains/symbolic_locs.ml
index 4a6fe9d0095..b972cb0a1ed 100644
--- a/src/plugins/eva/domains/symbolic_locs.ml
+++ b/src/plugins/eva/domains/symbolic_locs.ml
@@ -546,7 +546,7 @@ module D : Abstract_domain.Leaf
`Value (Memory.kill loc state)
let store_copy valuation lv loc state fv =
- if Cil.isArithmeticOrPointerType lv.ltyp then
+ if Cil.isArithmeticOrPointerType lv.lval.typ then
match fv.v, fv.initialized, fv.escaping with
| `Value v, true, false -> store_value valuation lv.lval loc state v
| _ -> store_indeterminate state loc
@@ -585,7 +585,7 @@ module D : Abstract_domain.Leaf
| None -> top_query
| Some v -> `Value (v, None), Alarmset.none
- let extract_lval ~oracle:_ _context state lv _typ _locs =
+ let extract_lval ~oracle:_ _context state lv _locs =
match Memory.find_lval lv state with
| None -> top_query
| Some v -> `Value (v, None), Alarmset.none
diff --git a/src/plugins/eva/domains/taint_domain.ml b/src/plugins/eva/domains/taint_domain.ml
index d55ffdc6050..00cc78a0807 100644
--- a/src/plugins/eva/domains/taint_domain.ml
+++ b/src/plugins/eva/domains/taint_domain.ml
@@ -290,7 +290,7 @@ module QueriesTaint = struct
let top_query = `Value (Cvalue.V.top, None), Alarmset.all
let extract_expr ~oracle:_ _context _state _expr = top_query
- let extract_lval ~oracle:_ _context _state _lv _typ _locs = top_query
+ let extract_lval ~oracle:_ _context _state _lv _locs = top_query
end
diff --git a/src/plugins/eva/domains/traces_domain.ml b/src/plugins/eva/domains/traces_domain.ml
index b427c440de0..3d471e0104a 100644
--- a/src/plugins/eva/domains/traces_domain.ml
+++ b/src/plugins/eva/domains/traces_domain.ml
@@ -1104,7 +1104,7 @@ module D = struct
let assign ki lv e _v _valuation state =
let cil_lval = Evast_utils.to_cil_lval lv.Eval.lval in
let cil_exp = Evast_utils.to_cil_exp e in
- let trans = Assign (ki, cil_lval, lv.Eval.ltyp, cil_exp) in
+ let trans = Assign (ki, cil_lval, lv.lval.typ, cil_exp) in
`Value (Traces.add_trans state trans)
let assume stmt e pos _valuation state =
@@ -1180,7 +1180,7 @@ module D = struct
let top_query = `Value (Cvalue.V.top, None), Alarmset.all
let extract_expr ~oracle:_ _context _state _expr = top_query
- let extract_lval ~oracle:_ _context _state _lv _typ _locs = top_query
+ let extract_lval ~oracle:_ _context _state _lv _locs = top_query
let enter_loop stmt state =
let state = Traces.add_trans state (Msg "enter_loop") in
diff --git a/src/plugins/eva/domains/unit_domain.ml b/src/plugins/eva/domains/unit_domain.ml
index 0d05955f190..caba1937bd9 100644
--- a/src/plugins/eva/domains/unit_domain.ml
+++ b/src/plugins/eva/domains/unit_domain.ml
@@ -59,7 +59,7 @@ module Make
let eval_top = `Value (Value.top, None), Alarmset.all
let extract_expr ~oracle:_ _ _ _ = eval_top
- let extract_lval ~oracle:_ _ _ _ _ _ = eval_top
+ let extract_lval ~oracle:_ _ _ _ _ = eval_top
let update _ _ = `Value ()
let assign _ _ _ _ _ _ = `Value ()
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index d680a534eb4..35c262f48a1 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -139,7 +139,7 @@ module Make (Abstract: Abstractions.S) = struct
let copy_lvalue state expr = Eval.copy_lvalue state expr >>=: snd
let eval_lval_to_loc state lv =
- let get_loc (_, loc, _) = loc in
+ let get_loc (_, loc) = loc in
let for_writing = false in
Eval.lvaluate ~for_writing state lv >>=: get_loc
diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml
index 43fa00b6e1b..b93a129e6cb 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -480,10 +480,10 @@ module Make
(* Assumes that [res] is a valid result for the lvalue [lval] of type [typ].
Removes NaN and infinite floats and trap representations of bool values. *)
- let assume_valid_value context typ lval res =
+ let assume_valid_value context lval res =
let open Evaluated.Operators in
let* value, origin = res in
- match typ with
+ match lval.typ with
| TFloat (fkind, _) ->
let expr = Evast_builder.lval lval in
let+ new_value = remove_special_float expr fkind value in
@@ -885,7 +885,7 @@ module Make
| Lval _lval -> assert false
| AddrOf v | StartOf v ->
- let* loc, _, _ = lval_to_loc env ~for_writing:false ~reduction:false v in
+ let* loc, _ = lval_to_loc env ~for_writing:false ~reduction:false v in
let* value = Loc.to_value loc, Alarmset.none in
let v = assume_pointer env.context expr value in
compute_reduction v false
@@ -953,13 +953,13 @@ module Make
let compute () =
let res, alarms = reduced_lval_to_loc env ~for_writing ~reduction lval in
let res =
- let+ loc, typ_offs, red, volatile = res in
+ let+ loc, red, volatile = res in
let fuel = env.remaining_fuel in
- let record = { loc; typ = typ_offs; loc_alarms = alarms }
+ let record = { loc; loc_alarms = alarms }
and report = { fuel = Finite fuel; reduction = red; volatile }
and loc_report = { for_writing; with_reduction = reduction } in
cache := Cache.add_loc' !cache lval (record, (report, loc_report));
- (loc, typ_offs, volatile)
+ (loc, volatile)
in
res, alarms
in
@@ -968,7 +968,7 @@ module Make
match Cache.find_loc' !cache lval with
| `Value (record, (report, loc_report)) ->
if already_precise loc_report && not_enough_fuel report.fuel
- then `Value (record.loc, record.typ, report.volatile), record.loc_alarms
+ then `Value (record.loc, report.volatile), record.loc_alarms
else compute ()
| `Top -> compute ()
@@ -977,7 +977,7 @@ module Make
and reduced_lval_to_loc env ~for_writing ~reduction lval =
let open Evaluated.Operators in
let lval_to_loc = internal_lval_to_loc env ~for_writing ~reduction in
- let* loc, typ, volatile = lval_to_loc lval in
+ let* loc, volatile = lval_to_loc lval in
if reduction then
let bitfield = Evast_utils.is_bitfield lval in
let truth = Loc.assume_valid_location ~for_writing ~bitfield loc in
@@ -986,8 +986,8 @@ module Make
let alarm () = Alarms.Memory_access (cil_lval, access) in
let+ valid_loc = interpret_truth ~alarm loc truth in
let reduction = if Loc.equal_loc valid_loc loc then Neither else Forward in
- valid_loc, typ, reduction, volatile
- else `Value (loc, typ, Neither, volatile), Alarmset.none
+ valid_loc, reduction, volatile
+ else `Value (loc, Neither, volatile), Alarmset.none
(* Internal evaluation of a lvalue to an abstract location.
Combination of the evaluation of the right part of an lval (an host) with
@@ -995,16 +995,17 @@ module Make
and internal_lval_to_loc env ~for_writing ~reduction lval =
let open Evaluated.Operators in
let host, offset = lval.node in
- let typ = Evast_typing.type_of_lhost host in
- let evaluated = eval_offset env ~reduce_valid_index:reduction typ offset in
- let* (offs, typ_offs, offset_volatile) = evaluated in
- if for_writing && Eva_utils.is_const_write_invalid typ_offs then
+ let basetyp = Evast_typing.type_of_lhost host in
+ let reduce_valid_index = reduction in
+ let evaluated = eval_offset env ~reduce_valid_index basetyp offset in
+ let* (offs, offset_volatile) = evaluated in
+ if for_writing && Eva_utils.is_const_write_invalid lval.typ then
let cil_lval = Evast_utils.to_cil_lval lval in
let alarm = Alarms.(Memory_access (cil_lval, For_writing)) in
`Bottom, Alarmset.singleton ~status:Alarmset.False alarm
else
- let+ loc, host_volatile = eval_host env typ_offs offs host in
- loc, typ_offs, offset_volatile || host_volatile
+ let+ loc, host_volatile = eval_host env lval.typ offs host in
+ loc, offset_volatile || host_volatile
(* Host evaluation. Also returns a boolean which is true if the host
contains a volatile sub-expression. *)
@@ -1022,7 +1023,7 @@ module Make
(* Offset evaluation. Also returns a boolean which is true if the offset
contains a volatile sub-expression. *)
and eval_offset env ~reduce_valid_index typ = function
- | NoOffset -> return (Loc.no_offset, typ, false)
+ | NoOffset -> return (Loc.no_offset, false)
| Index (index_expr, remaining) ->
let open Evaluated.Operators in
let typ_pointed, array_size =
@@ -1031,7 +1032,7 @@ module Make
| t -> Self.fatal ~current:true "Got type '%a'" Printer.pp_typ t
in
let eval = eval_offset env ~reduce_valid_index typ_pointed remaining in
- let* roffset, typ_offs, remaining_volatile = eval in
+ let* roffset, remaining_volatile = eval in
let* index, volatile = root_forward_eval env index_expr in
let valid_index =
if not (Kernel.SafeArrays.get ()) || not reduce_valid_index
@@ -1050,16 +1051,16 @@ module Make
with Cil.LenOfArray _ -> `Value index, Alarmset.none (* unknown array size *)
in
let+ index = valid_index in
- Loc.forward_index typ_pointed index roffset, typ_offs,
+ Loc.forward_index typ_pointed index roffset,
remaining_volatile || volatile
| Field (fi, remaining) ->
let open Evaluated.Operators in
let attrs = Cil.filter_qualifier_attributes (Cil.typeAttrs typ) in
let typ_fi = Cil.typeAddAttributes attrs fi.ftype in
let evaluated = eval_offset env ~reduce_valid_index typ_fi remaining in
- let+ r, typ_res, volatile = evaluated in
+ let+ r, volatile = evaluated in
let off = Loc.forward_field typ fi r in
- off, typ_res, volatile
+ off, volatile
and eval_lval ?(indeterminate=false) env lval =
let open Evaluated.Operators in
@@ -1067,23 +1068,22 @@ module Make
let env = { env with root = false } in
(* Computes the location of [lval]. *)
let evaluated = lval_to_loc env ~for_writing:false ~reduction:true lval in
- let* loc, typ_lv, volatile_expr = evaluated in
- let typ_lv = Cil.unrollType typ_lv in
+ let* loc, volatile_expr = evaluated in
(* the lvalue is volatile:
- if it has qualifier volatile (lval_to_loc propagates qualifiers
in the proper way through offsets)
- if it contains a sub-expression which is volatile (volatile_expr)
*)
- let volatile = volatile_expr || Cil.typeHasQualifier "volatile" typ_lv in
+ let volatile = volatile_expr || Cil.typeHasQualifier "volatile" lval.typ in
let cil_lval = Evast_utils.to_cil_lval lval in
(* Find the value of the location, if not bottom. *)
- let v, alarms = domain_query lval typ_lv loc in
+ let v, alarms = domain_query lval loc in
let alarms = close_dereference_alarms cil_lval alarms in
if indeterminate then
let record, alarms = indeterminate_copy cil_lval v alarms in
`Value (record, Neither, volatile), alarms
else
- let v, alarms = assume_valid_value env.context typ_lv lval (v, alarms) in
+ let v, alarms = assume_valid_value env.context lval (v, alarms) in
let+ value, origin = v, alarms in
let value = define_value value in
let reductness, reduction =
@@ -1363,8 +1363,9 @@ module Make
match find_loc_for_reduction lval with
| None -> `Value None
| Some (record, report) ->
- let backward_location = Domain.backward_location state lval in
- let* loc, new_value = backward_location record.typ record.loc value in
+ let* loc, new_value =
+ Domain.backward_location state lval record.loc value
+ in
let+ value = Value.narrow new_value value in
let b = not (Loc.equal_loc record.loc loc) in
(* Avoids useless reductions and reductions of volatile expressions. *)
@@ -1392,7 +1393,7 @@ module Make
let typ_lval = Cil.typeOf_pointed expr.typ in
let* env = fast_eval_environment state in
let eval = eval_offset env ~reduce_valid_index typ_lval offset in
- let* loc_offset, _, _ = fst eval in
+ let* loc_offset, _ = fst eval in
let* value = find_val expr in
let pointer = Loc.backward_pointer value loc_offset location in
let* pointer_value, loc_offset = pointer in
@@ -1409,7 +1410,7 @@ module Make
let* v = find_val exp in
let typ_pointed = Cil.typeOf_array_elem typ in
let* env = fast_eval_environment state in
- let* rem, _, _ =
+ let* rem, _ =
eval_offset env ~reduce_valid_index:true typ_pointed remaining |> fst
in
let* v', rem' =
@@ -1472,7 +1473,7 @@ module Make
let* () =
if (fst report).reduction = Backward then
let for_writing = false and reduction = true in
- let+ loc, _, _, _ =
+ let+ loc, _, _ =
reduced_lval_to_loc ~for_writing ~reduction env lval |> fst
in
(* TODO: Loc.narrow *)
@@ -1587,11 +1588,11 @@ module Make
let* valuation = evaluate_offsets valuation ?subdivnb state offset in
cache := valuation;
let* env = root_environment ?subdivnb state, Alarmset.none in
- let& _, typ, _ = lval_to_loc env ~for_writing ~reduction:true lval in
+ let& _ = lval_to_loc env ~for_writing ~reduction:true lval in
let open Bottom.Operators in
let+ () = backward_lval (backward_fuel ()) env.context state lval in
match Cache.find_loc !cache lval with
- | `Value record -> !cache, record.loc, typ
+ | `Value record -> !cache, record.loc
| `Top -> assert false
let reduce ?valuation:(valuation=Cache.empty) state expr positive =
diff --git a/src/plugins/eva/engine/evaluation_sig.ml b/src/plugins/eva/engine/evaluation_sig.ml
index 7fc600378d2..b03cb64217e 100644
--- a/src/plugins/eva/engine/evaluation_sig.ml
+++ b/src/plugins/eva/engine/evaluation_sig.ml
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
-open Cil_types
open Eval
(** Generic evaluation and reduction of expressions and left values. *)
@@ -97,7 +96,7 @@ module type S = sig
expressions (including the possible pointer and offset of the lvalue). *)
val lvaluate :
?valuation:Valuation.t -> ?subdivnb:int -> for_writing:bool ->
- state -> lval -> (Valuation.t * loc * typ) evaluated
+ state -> lval -> (Valuation.t * loc) evaluated
(** [reduce ~valuation state expr positive] evaluates the expression [expr]
in the state [state], and then reduces the [valuation] such that
diff --git a/src/plugins/eva/engine/initialization.ml b/src/plugins/eva/engine/initialization.ml
index a996a9922b1..71f118040cb 100644
--- a/src/plugins/eva/engine/initialization.ml
+++ b/src/plugins/eva/engine/initialization.ml
@@ -93,7 +93,7 @@ module Make
other globals. *)
let lval_to_loc lval =
fst (Eva.lvaluate ~for_writing:false Domain.top lval)
- >>> fun (_valuation, loc, _typ) -> loc
+ >>> fun (_valuation, loc) -> loc
include Cvalue_domain.Getters (Domain)
diff --git a/src/plugins/eva/engine/subdivided_evaluation.ml b/src/plugins/eva/engine/subdivided_evaluation.ml
index da6b0966ac9..43f39db787e 100644
--- a/src/plugins/eva/engine/subdivided_evaluation.ml
+++ b/src/plugins/eva/engine/subdivided_evaluation.ml
@@ -393,7 +393,7 @@ module Make
| `Value record -> record
| `Top -> assert false
- let find_loc valuation lval = match Valuation.find_loc valuation lval with
+ let _find_loc valuation lval = match Valuation.find_loc valuation lval with
| `Value record -> record
| `Top -> assert false
@@ -497,11 +497,9 @@ module Make
(* Makes the split function for a list of lvalues. The split function depends
on the size of each lvalue, computed from their type. *)
- let make_split valuation (lvals: 'l sub_lvals) : 'l split =
+ let make_split (lvals: 'l sub_lvals) : 'l split =
let compute_size info =
- (* The size is defined, as [lv] is a scalar *)
- let record = find_loc valuation info.lval in
- Int_Base.project (Eval_typ.sizeof_lval_typ record.typ)
+ Int_Base.project (Eval_typ.sizeof_lval_typ info.lval.typ)
in
let sizes = Hypotheses.map compute_size lvals in
Hypotheses.split sizes
@@ -651,7 +649,7 @@ module Make
let subdivide_lvals env valuation subdivnb ~expr ~subexpr lvals =
let Hypotheses.L variables = Hypotheses.from_list lvals in
(* Split function for the subvalues of [lvals]. *)
- let split = make_split valuation variables in
+ let split = make_split variables in
(* Clear the valuation to force the evaluation on top of [lvals]. *)
let clear lv_info valuation =
Clear.clear_englobing_exprs valuation ~expr ~subexpr:lv_info.lv_expr
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index bb9502367c3..50804523203 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -189,10 +189,10 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
Assign value, valuation
(* Assignment by copying the value of a right lvalue. *)
- let assign_by_copy ~subdivnb state valuation lval lloc ltyp =
+ let assign_by_copy ~subdivnb state valuation lval lloc =
copy_lvalue_and_check ~valuation ~subdivnb state lval
>>=: fun (valuation, value) ->
- Copy ({lval; lloc; ltyp}, value), valuation
+ Copy ({lval; lloc}, value), valuation
(* For an initialization, use for_writing:false for the evaluation of
the left location, as the written variable could be const. This is only
@@ -243,12 +243,12 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
"@[<v>@[all target addresses were invalid. This path is \
assumed to be dead.@]%t@]" Eva_utils.pp_callstack;
`Bottom
- | `Value (valuation, lloc, ltyp) ->
+ | `Value (valuation, lloc) ->
(* Tries to interpret the assignment as a copy for the returned value
of a function call, on struct and union types, and when
-eva-warn-copy-indeterminate is disabled. *)
let lval_copy =
- if is_ret || Cil.isStructOrUnionType ltyp || do_copy_at kinstr
+ if is_ret || Cil.isStructOrUnionType lval.typ || do_copy_at kinstr
then find_lval expr
else None
in
@@ -261,18 +261,18 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* In case of a copy, checks that the left and right locations are
compatible and that they do not overlap. *)
lvaluate_and_check ~for_writing ~subdivnb ~valuation state right_lval
- >>= fun (valuation, rloc, rtyp) ->
- check_overlap ltyp (lval, lloc) (right_lval, rloc)
+ >>= fun (valuation, rloc) ->
+ check_overlap lval.typ (lval, lloc) (right_lval, rloc)
>>= fun (lloc, rloc) ->
if are_compatible lloc rloc
- then assign_by_copy ~subdivnb state valuation right_lval rloc rtyp
+ then assign_by_copy ~subdivnb state valuation right_lval rloc
else assign_by_eval ~subdivnb state valuation expr
in
if is_ret then assert (Alarmset.is_empty alarms);
Alarmset.emit kinstr alarms;
let* assigned, valuation = eval in
let domain_valuation = Eval.to_domain_valuation valuation in
- let lvalue = { lval; ltyp; lloc } in
+ let lvalue = { lval; lloc } in
Domain.assign kinstr lvalue expr assigned domain_valuation state
let assign = assign_lv_or_ret ~is_ret:false
@@ -491,7 +491,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
match (expr : Evast.exp).node with
| Lval lv ->
lvaluate_and_check ~for_writing:false ~subdivnb ~valuation state lv
- >>= fun (valuation, loc, typ) ->
+ >>= fun (valuation, loc) ->
if Int_Base.is_top (Location.size loc)
then
Self.abort ~current:true
@@ -499,7 +499,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
Evast_printer.pp_exp expr;
if determinate && Cil.isArithmeticOrPointerType lv.typ
then assign_by_eval ~subdivnb state valuation expr
- else assign_by_copy ~subdivnb state valuation lv loc typ
+ else assign_by_copy ~subdivnb state valuation lv loc
| _ -> assign_by_eval ~subdivnb state valuation expr
(* Evaluates the list of the actual arguments of a call. Returns the list
@@ -542,7 +542,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let flagged = { flagged with v } in
let lloc = Location.replace_base substitution loc.lloc in
let lval = Evast_visitor.Rewrite.visit_lval visitor loc.lval in
- let loc = { loc with lval; lloc } in
+ let loc = { lval; lloc } in
Copy (loc, flagged)
let replace_recursive_call recursion call =
@@ -626,7 +626,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
fun fmt subdivnb lval state ->
try
let offsm =
- let* (_, loc, _) =
+ let* (_, loc) =
fst (Eval.lvaluate ~for_writing:false ~subdivnb state lval) in
Eval_op.offsetmap_of_loc (get_ploc loc) (get_cvalue state)
in
@@ -788,7 +788,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let eval_loc (acc, valuation) lval =
match lvaluate ~valuation lval with
| `Bottom -> acc, valuation
- | `Value (valuation, loc, _) -> (lval, loc) :: acc, valuation
+ | `Value (valuation, loc) -> (lval, loc) :: acc, valuation
in
let eval_list valuation lvs =
List.fold_left eval_loc ([], valuation) lvs
diff --git a/src/plugins/eva/eval.ml b/src/plugins/eva/eval.ml
index 090d6861db8..6c46b61b70f 100644
--- a/src/plugins/eva/eval.ml
+++ b/src/plugins/eva/eval.ml
@@ -126,7 +126,6 @@ type ('a, 'origin) record_val = {
(* Data record associated to each evaluated left-value. *)
type 'a record_loc = {
loc: 'a; (* The location of the left-value. *)
- typ: typ; (* *)
loc_alarms: Alarmset.t (* The emitted alarms during the evaluation. *)
}
@@ -219,7 +218,6 @@ end
type 'loc left_value = {
lval: lval;
lloc: 'loc;
- ltyp: typ;
}
(* Assigned values. *)
diff --git a/src/plugins/eva/eval.mli b/src/plugins/eva/eval.mli
index a31535df4ed..936ccdae4f8 100644
--- a/src/plugins/eva/eval.mli
+++ b/src/plugins/eva/eval.mli
@@ -146,7 +146,6 @@ type ('a, 'origin) record_val = {
(** Data record associated to each evaluated left-value. *)
type 'a record_loc = {
loc: 'a; (** The location of the left-value. *)
- typ: typ; (** *)
loc_alarms: Alarmset.t (** The emitted alarms during the evaluation. *)
}
@@ -190,7 +189,6 @@ end
type 'loc left_value = {
lval: lval;
lloc: 'loc;
- ltyp: typ;
}
(** Assigned values. *)
diff --git a/src/plugins/eva/utils/results.ml b/src/plugins/eva/utils/results.ml
index d1bad3190eb..2e352cf740f 100644
--- a/src/plugins/eva/utils/results.ml
+++ b/src/plugins/eva/utils/results.ml
@@ -212,7 +212,7 @@ struct
type valuation = A.Eval.Valuation.t
type exp = (valuation * A.Val.t) Eval.evaluated
type lval = (valuation * A.Val.t Eval.flagged_value) Eval.evaluated
- type loc = (valuation * A.Loc.location * Cil_types.typ) Eval.evaluated
+ type loc = (valuation * A.Loc.location) Eval.evaluated
end
type ('a,'c) evaluation =
@@ -398,7 +398,7 @@ struct
| Address (r, access) ->
let extract (x, _alarms) =
let open Bottom.Operators in
- let+ _valuation,loc,_typ = x in loc
+ let+ _valuation,loc = x in loc
in
Response.map extract r, access
--
GitLab