package frama-c

  1. Overview
  2. Docs

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

Module Memory_tracking.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
OCaml

Innovation. Community. Security.