C (frama-c.Frama_c_kernel.Logic

val is_loop : unit -> bool

whether the annotation we want to type is contained in a loop. Only useful when creating objects of type code_annotation.

val anonCompFieldName : string

val conditionalConversion : Cil_types.typ -> Cil_types.typ -> Cil_types.typ

val find_macro : string -> Logic_ptree.lexpr

val find_var : ?label:string -> string -> Cil_types.logic_var

val find_enum_tag : string -> Cil_types.exp * Cil_types.typ

val find_type : type_namespace -> string -> Cil_types.typ

val find_comp_field : Cil_types.compinfo -> string -> Cil_types.offset

val find_label : string -> Cil_types.stmt Stdlib.ref

val remove_logic_function : string -> unit

val remove_logic_info : Cil_types.logic_info -> unit

val remove_logic_type : string -> unit

val remove_logic_ctor : string -> unit

val add_logic_function : Cil_types.logic_info -> unit

val add_logic_type : string -> Cil_types.logic_type_info -> unit

val add_logic_ctor : string -> Cil_types.logic_ctor_info -> unit

val find_all_logic_functions : string -> Cil_types.logic_info list

val find_logic_type : string -> Cil_types.logic_type_info

val find_logic_ctor : string -> Cil_types.logic_ctor_info

val integral_cast : Cil_types.typ -> Cil_types.term -> Cil_types.term

What to do when we have a term of type Integer in a context expecting a C integral type.

val error : 
  Cil_types.location ->
  ( 'a, Stdlib.Format.formatter, unit, 'b ) Stdlib.format4 ->
  'a

raises an error at the given location and with the given message.

val on_error : 
  ( 'a -> 'b ) ->
  ( (Cil_types.location * string) -> unit ) ->
  'a ->
  'b