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

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.