module Hcexprs: sig
.. end
Hash-consed expressions and lvalues.
type
unhashconsed_exprs = private
exception NonExchangeable
Raised when the replacement of an lvalue in an expression is impossible.
type
kill_type =
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
.