Previous  Up  Next

Module Ast.Expression


module Expression: sig  end

type access_op =
| Dot
| Arrow


type assign_op =
| Assign
| AssignBitAnd
| AssignBitOr
| AssignDiv
| AssignLShift
| AssignMinus
| AssignMul
| AssignPlus
| AssignRem
| AssignRShift
| AssignXor


type unary_op =
| UnaryMinus
| Not
| BitNot
| Address
| UnaryPlus
| DestructorCall
| Assume
| Assert
| PreInc
| PreDec
| PostInc
| PostDec


type binary_op =
| BitAnd
| BitOr
| Div
| LShift
| Minus
| Mul
| Plus
| Rem
| RShift
| Xor
| Eq
| Ge
| Gt
| Le
| Lt
| Ne
| Index
| And
| Or
| Comma
| FieldOffset


type lval =
| Symbol of Ast.Symbol.symbol
| Access of access_op * expression * Ast.Symbol.symbol
| Dereference of expression
| Indexed of expression * expression


type expression =
| Lval of lval
| Chlval of lval * string
| Assignment of assign_op * lval * expression
| Binary of binary_op * expression
* expression
| Cast of Ast.ast_type * expression
| Constant of Ast.Constant.constant
| Constructor of Ast.Symbol.symbol * Ast.ast_type
| FunctionCall of expression * expression list
| Sizeof of int
| Unary of unary_op * expression


type t = expression
t and compare are added to make Expression a Set.OrderedType. With these, we can put expressions in sets. The type t is of course the same as the type expression, and compare is the system compare

val compare : t -> t -> int
val unaryOpToString : unary_op -> string
val unaryOpToVanillaString : unary_op -> string
a vanilla string is a string over the alphabet [a-zA-Z0-9] ; it is useful because the theorem provers/other backend tools dislike expressions like "|". Vanilla string for this is BitOr.
val assignOpToString : assign_op -> string
val accessOpToString : access_op -> string
val binaryOpToString : binary_op -> string
val binaryOpToVanillaString : binary_op -> string

Printers.

val print : Format.formatter -> expression -> unit
val print_lval : Format.formatter -> lval -> unit
val toString : expression -> string
val lvalToString : lval -> string

Miscellaneous utilities.

val addressOf : expression -> expression
Push all address operators to the variables. See the memory model discussions.
val replaceChlvals : expression -> expression
replace all occurrences of a Chlval by corresponding Lval
val isRelOp : binary_op -> bool
val isDeref : expression -> bool
val push_deref : lval -> lval
val derefedVar : lval -> expression
val getParents : lval list -> expression list
val allVarExps : expression -> expression list
val negateRel : expression -> expression
val fresh_lval : lval -> expression
returns a chlval that is essentially a "Fresh" version of that lval
val alpha_convert : (lval -> lval) ->
       expression -> expression
val alpha_convert_lval : (lval -> lval) ->
       lval -> lval
val deep_alpha_convert : (lval -> expression) ->
       expression -> expression
deep_alpha_convert f: lval -> expr where f: lval -> expr essentially f has the chlval information ... this substitutes the lval at the top level and then goes inside and recursively goes in and substitutes
val substituteExpression : (expression * expression) list ->
       expression -> expression
val assignments_of_expression : expression ->
       (expression * expression) list