Absint.HilExp
type t =
| AccessExpression of access_expression
access path (e.g., x.f.g or xi
)
| UnaryOperator of IR.Unop.t * t * IR.Typ.t option
Unary operator with type of the result if known
*)| BinaryOperator of IR.Binop.t * t * t
Binary operator
*)| Exception of t
Exception
*)| Closure of IR.Procname.t * (AccessPath.base * t) list
Name of function + environment
*)| Constant of IR.Const.t
Constants
*)| Cast of IR.Typ.t * t
Type cast
*)| Sizeof of IR.Typ.t * t option
C-style sizeof(), and also used to treate a type as an expression. Refer to Exp
module for canonical documentation
and access_expression = private
| Base of AccessPath.base
| FieldOffset of access_expression * IR.Fieldname.t
field access
*)| ArrayOffset of access_expression * IR.Typ.t * t option
array access
*)| AddressOf of access_expression
"address of" operator &
| Dereference of access_expression
"dereference" operator *
val compare_access_expression : access_expression -> access_expression -> int
val equal_access_expression : access_expression -> access_expression -> bool
module AccessExpression : sig ... end
val pp : F.formatter -> t -> unit
val of_sil :
include_array_indexes:bool ->
f_resolve_id:(IR.Var.t -> AccessExpression.t option) ->
add_deref:bool ->
IR.Exp.t ->
IR.Typ.t ->
t
Convert SIL expression to HIL expression
val get_access_exprs : t -> AccessExpression.t list
Get all the access paths used in the given HIL expression, including duplicates if a path is used more than once.
val is_null_literal : t -> bool
val is_int_zero : t -> bool
val eval_boolean_exp : AccessExpression.t -> t -> bool option
eval_boolean_exp var exp
returns Some bool_value
if the given boolean expression exp
evaluates to bool_value
when var
is set to true. Return None if it has free variables that stop us from evaluating it, or is not a boolean expression.
val access_expr_of_exp :
include_array_indexes:bool ->
f_resolve_id:(IR.Var.t -> AccessExpression.t option) ->
IR.Exp.t ->
IR.Typ.t ->
access_expression option
best effort translating a SIL expression to an access path, not semantics preserving in particular in the presence of pointer arithmetic