Frama-C:
Plug-ins:
Libraries:

Frama-C API - _

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

see corresponding field in Logic_typing.typing_context.

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.

  • raises Failure

    to reject such conversion

  • since Nitrogen-20111001
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.

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

see Logic_typing.typing_context.