Frama-C:
Plug-ins:
Libraries:

Frama-C API - Cabshelper

Helper functions for Cabs

val nextident : int Stdlib.ref
val getident : unit -> int
val cabslu : Fileloc.t
module Comments : sig ... end
val missingFieldDecl : Fileloc.t -> string * Cabs.decl_type * 'a list * Fileloc.t
val isStatic : Cabs.spec_elem list -> bool
val isExtern : Cabs.spec_elem list -> bool
val isInline : Cabs.spec_elem list -> bool
val isTypedef : Cabs.spec_elem list -> bool
val get_definitionloc : Cabs.definition -> Fileloc.t
val get_statementloc : Cabs.statement -> Fileloc.t
val explodeStringToInts : string -> int64 list
val valueOfDigit : char -> int64
  • deprecated Use Fileloc.pretty instead.
val push_attr_test : unit -> unit
val pop_attr_test : unit -> unit
val is_attr_test : unit -> bool
val mk_behavior : ?name:string -> ?assumes:Logic_ptree.lexpr list -> ?requires:Logic_ptree.toplevel_predicate list -> ?post_cond:(Cil_types.termination_kind * Logic_ptree.toplevel_predicate) list -> ?assigns:Logic_ptree.assigns -> ?allocation:Logic_ptree.allocation -> ?extended:Logic_ptree.extension list -> unit -> Logic_ptree.behavior
val mk_asm_templates : string list -> string list