Frama-C API - Smart_exp
val lval : loc:Frama_c_kernel.Cil_types.location -> Frama_c_kernel.Cil_types.lval -> Frama_c_kernel.Cil_types.exp
Construct an lval expression from an lval.
val deref : loc:Frama_c_kernel.Cil_types.location -> Frama_c_kernel.Cil_types.exp -> Frama_c_kernel.Cil_types.exp
Construct a dereference of an expression.
val subscript : loc:Frama_c_kernel.Cil_types.location -> Frama_c_kernel.Cil_types.exp -> Frama_c_kernel.Cil_types.exp -> Frama_c_kernel.Cil_types.exp
mk_subscript ~loc array idx
Create an expression to access the idx
'th element of the array
.
val ptr_sizeof : loc:Frama_c_kernel.Cil_types.location -> Frama_c_kernel.Cil_types.typ -> Frama_c_kernel.Cil_types.exp
ptr_sizeof ~loc ptr_typ
takes the pointer typ ptr_typ
that points to a typ
typ and returns sizeof(typ)
.
val lnot : loc:Frama_c_kernel.Cil_types.location -> Frama_c_kernel.Cil_types.exp -> Frama_c_kernel.Cil_types.exp
lnot ~loc e
creates a logical not on the given expression e
.
val null : loc:Frama_c_kernel.Cil_types.location -> Frama_c_kernel.Cil_types.exp
null ~loc
creates an expression to represent the NULL pointer.
val mem : loc:Frama_c_kernel.Cil_types.location -> Frama_c_kernel.Cil_types.varinfo -> Frama_c_kernel.Cil_types.exp
mem ~loc v
creates a Mem expression with an explicit index of 0