Frama-C:
Plug-ins:
Libraries:

Frama-C API - Hcexprs

Hash-consed expressions and lvalues.

type unhashconsed_exprs = private
  1. | E of Eva_ast.exp
  2. | LV of Eva_ast.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 =
  1. | Modified
  2. | 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 HCE : sig ... end

Datatype + utilities functions for hashconsed exprsessions.

Hashconsed sets of symbolic expressions.

type lvalues = {
  1. read : HCESet.t;
  2. addr : HCESet.t;
}
val empty_lvalues : lvalues
val syntactic_lvalues : Eva_ast.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 from Base.t to set of HCE.t.