module Hcexprs:sig
..end
Hash-consed expressions and lvalues.
type
unhashconsed_exprs = private
| |
E of |
|||
| |
LV of |
(* | lvalues are never stored under a constructor | *) |
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 : |
|
addr : |
}
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
.