IR.Exp
The Smallfoot Intermediate Language: Expressions
NOTE: For doing substitutionson expressions, there are some functions in Sil
.
type closure = {
name : Procname.t;
captured_vars : (t * Pvar.t * Typ.t * CapturedVar.capture_mode) list;
}
This records information about a sizeof(typ)
expression.
nbytes
represents the result of the evaluation of sizeof(typ)
if it is statically known.
If typ
is of the form Tarray elt (Some static_length)
, then dynamic_length
is the number of elements of type elt
in the array. The dynamic_length
, tracked by symbolic execution, may differ from the static_length
obtained from the type definition, e.g. when an array is over-allocated.
If typ
is a struct type, the dynamic_length
is that of the final extensible array, if any.
and t =
| Var of Ident.t
Pure variable: it is not an lvalue
*)| UnOp of Unop.t * t * Typ.t option
Unary operator with type of the result if known
*)| BinOp of Binop.t * t * t
Binary operator
*)| Exn of t
Exception
*)| Closure of closure
Anonymous function
*)| Const of Const.t
Constants
*)| Cast of Typ.t * t
Type cast
*)| Lvar of Pvar.t
The address of a program variable
*)| Lfield of t * Fieldname.t * Typ.t
A field offset, the type is the surrounding struct type
*)| Lindex of t * t
An array index offset: exp1[exp2]
| Sizeof of sizeof_data
Program expressions.
val compare_sizeof_data : sizeof_data -> sizeof_data -> int
val hash_fold_closure :
Ppx_hash_lib.Std.Hash.state ->
closure ->
Ppx_hash_lib.Std.Hash.state
val hash_closure : closure -> Ppx_hash_lib.Std.Hash.hash_value
val hash_fold_sizeof_data :
Ppx_hash_lib.Std.Hash.state ->
sizeof_data ->
Ppx_hash_lib.Std.Hash.state
val hash_sizeof_data : sizeof_data -> Ppx_hash_lib.Std.Hash.hash_value
val hash_fold_t :
Ppx_hash_lib.Std.Hash.state ->
t ->
Ppx_hash_lib.Std.Hash.state
val hash : t -> Ppx_hash_lib.Std.Hash.hash_value
val hash_normalize_sizeof_data : sizeof_data -> sizeof_data
val hash_normalize_sizeof_data_opt : sizeof_data option -> sizeof_data option
val hash_normalize_sizeof_data_list : sizeof_data list -> sizeof_data list
val is_null_literal : t -> bool
val is_this : t -> bool
return true if exp
is the special this/self expression
val is_zero : t -> bool
val is_const : t -> bool
Turn an expression representing a type into the type it represents If not a sizeof, return the default type if given, otherwise raise an exception
val get_undefined : bool -> t
Get an expression "undefined", the boolean indicates whether the undefined value goest into the footprint
val pointer_arith : t -> bool
Checks whether an expression denotes a location using pointer arithmetic. Currently, catches array - indexing expressions such as ai
only.
val has_local_addr : t -> bool
returns true if the expression operates on address of local variable
val zero : t
Integer constant 0
val null : t
Null constant
val one : t
Integer constant 1
val minus_one : t
Integer constant -1
val float : float -> t
Create float constant
val bool : bool -> t
Create integer constant corresponding to the boolean value
all the program variables appearing in the expression
Fold over the expressions captured by this expression.
val pp_diff : ?print_types:bool -> IStdlib.Pp.env -> F.formatter -> t -> unit
val pp : F.formatter -> t -> unit
val pp_closure : F.formatter -> closure -> unit
val to_string : t -> string
val d_exp : t -> unit
dump an expression.
val pp_texp : IStdlib.Pp.env -> F.formatter -> t -> unit
Pretty print a type.
val pp_texp_full : IStdlib.Pp.env -> F.formatter -> t -> unit
Pretty print a type with all the details.
val d_texp_full : t -> unit
Dump a type expression with all the details.
val d_list : t list -> unit
Dump a list of expressions.
val is_cpp_closure : t -> bool
val get_java_class_initializer :
Tenv.t ->
t ->
(Procname.t * Pvar.t * Fieldname.t * Typ.t) option
Returns the class initializer of the given expression in Java