E_ACSL.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