Frama-C:
Plug-ins:
Libraries:

Frama-C API - SpecialPointers

type spec = {
  1. pointer : bool;
  2. freeable : bool;
  3. writeable : bool;
  4. initialized : bool;
}
val initialize : unit -> unit
val pointer_of_term : Frama_c_kernel.Cil_types.term -> spec option