Frama_c_kernel.Cabshelper
Helper functions for Cabs
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 d_cabsloc : Cabs.cabsloc Pretty_utils.formatter
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_attr_annot : string -> Cabs.attribute
builds a Cabs attribute annotation