Module `Frama_c_kernel.Cabshelper`

Helper functions for Cabs

val nextident : int Stdlib.ref

val getident : unit -> int

val cabslu : Cabs.cabsloc

module Comments : sig ... end

val missingFieldDecl : string * Cabs.decl_type * 'a list * Cabs.cabsloc

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 -> Cabs.cabsloc

val get_statementloc : Cabs.statement -> Cabs.cabsloc

val explodeStringToInts : string -> int64 list

val valueOfDigit : char -> int64

val d_cabsloc : Cabs.cabsloc Pretty_utils.formatter

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c.kernel/Frama_c_kernel/Cabshelper/index.html

Module `Frama_c_kernel.Cabshelper`

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c.kernel/Frama_c_kernel/Cabshelper/index.html

Module Frama_c_kernel.Cabshelper

Module `Frama_c_kernel.Cabshelper`