module Cvalue_offsetmap: sig
.. end
Auxiliary functions on cvalue offsetmaps, used by the cvalue domain.
val warn_right_imprecision : Cil_types.lval -> Locations.location -> Cvalue.V_Offsetmap.t -> unit
warn_right_imprecision lval loc offsm
is used for the assignment of the
lvalue lval
pointing to the location loc
; it warns if the offsetmap
offsm
contains a garbled mix.
val offsetmap_of_lval : Cvalue.Model.t ->
Cil_types.lval -> Precise_locs.precise_location -> Cvalue.V_Offsetmap.t
offsetmap_of_lval state lval loc
extracts from state state
the offsetmap
at location loc
, corresponding to the lvalue lval
. Warns if this
offsetmap contains a garbled mix.
val offsetmap_of_assignment : Cvalue.Model.t ->
Cil_types.exp ->
(Precise_locs.precise_location, Cvalue.V.t) Eval.assigned ->
Cvalue.V_Offsetmap.t
Computes the offsetmap for an assignment:
- in case of a copy, extracts the offsetmap from the state;
- otherwise, translates the value assigned into an offsetmap.