Module Cvalue_offsetmap

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.