Module Hcexprs

module Hcexprs: sig .. end
Hash-consed expressions and lvalues.

type unhashconsed_exprs = private 
| E of Cil_types.exp
| LV of Cil_types.lval (*
lvalues are never stored under a constructor E, only LV
*)
exception NonExchangeable
Raised when the replacement of an lvalue in an expression is impossible.
type kill_type = 
| Modified
| Deleted
Reason of the replacement of an lvalue lval: Modified means that the value of lval has been modified (in which case &lval is unchanged), and Deleted means that lval is no longer in scope (in which case &lval raises the NonExchangeable error).
module E: Datatype.S  with type t = unhashconsed_exprs
module HCE: sig .. end
Datatype + utilities functions for hashconsed exprsessions.
module HCESet: Hptset.S  with type elt = HCE.t
                         and type 'a shape = 'a Hptmap.Shape(HCE).t
Hashconsed sets of symbolic expressions.
type lvalues = {
   read : HCESet.t;
   addr : HCESet.t;
}
val empty_lvalues : lvalues
val syntactic_lvalues : Cil_types.exp -> lvalues
syntactic_lvalues e returns the set of lvalues that appear in the expression e. This is used by the equality domain: the expression e will be removed from an equality if a lvalue from syntactic_lvalues e is removed. This function only computes the first lvalues of the expression, and does not go through the lvalues (for the expression ti+1, only the lvalue ti is returned).
module HCEToZone: sig .. end
Maps from symbolic expressions to their memory dependencies, expressed as a Locations.Zone.t.
module BaseToHCESet: sig .. end
Maps froms Base.t to set of HCE.t.