package frama-c

  1. Overview
  2. Docs

doc/frama-c-e-acsl.core/E_ACSL/Smart_exp/index.html

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

OCaml

Innovation. Community. Security.