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 map = '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.