Module E_ACSL.Smart_exp

Construct an lval expression from an lval.

Construct a dereference of an expression.

mk_subscript ~loc array idx Create an expression to access the idx'th element of the array.

ptr_sizeof ~loc ptr_typ takes the pointer typ ptr_typ that points to a typ typ and returns sizeof(typ).

lnot ~loc e creates a logical not on the given expression e.

null ~loc creates an expression to represent the NULL pointer.

mem ~loc v creates a Mem expression with an explicit index of 0