Module E_ACSL.Functions

val has_fundef : Frama_c_kernel.Cil_types.exp -> bool
  • returns

    true if a function whose name is given via exp is defined and false otherwise

  • returns

    true iff code must be generated for annotations of the given function.

  • returns

    true iff the given function must be instrumented.

RTL Operations on function belonging to the runtime library of E-ACSL

module RTL : sig ... end

Libc Operations on functions belonging to standard library

module Libc : sig ... end

Concurrency Operations concerning the support of concurrency

module Concurrency : sig ... end