module Make:functor (
C
:
sig
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 :Logic_typing.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.
- Since Nitrogen-20111001
- Raises
Failure
to reject such conversionval error :Cil_types.location ->
('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'araises an error at the given location and with the given message.
- Since Magnesium-20151001
val on_error :('a -> 'b) -> (unit -> unit) -> 'a -> 'b
see
Logic_typing.typing_context
.end
) ->
sig
..end
Parameters: |
|
val type_of_field : Cil_types.location ->
string ->
Cil_types.logic_type -> Cil_types.term_offset * Cil_types.logic_type
val mk_cast : ?explicit:bool -> Cil_types.term -> Cil_types.logic_type -> Cil_types.term
explicit
: true if the cast is present in original source.
defaults to falseval term : Logic_typing.Lenv.t -> Logic_ptree.lexpr -> Cil_types.term
type-checks a term.
val predicate : Logic_typing.Lenv.t -> Logic_ptree.lexpr -> Cil_types.predicate
val code_annot : Cil_types.location ->
string list ->
Cil_types.logic_type -> Logic_ptree.code_annot -> Cil_types.code_annotation
code_annot loc behaviors rt annot
type-checks an in-code annotation.
val type_annot : Cil_types.location -> Logic_ptree.type_annot -> Cil_types.logic_info
val model_annot : Cil_types.location -> Logic_ptree.model_annot -> Cil_types.model_info
val annot : Logic_ptree.decl -> Cil_types.global_annotation
val custom : Logic_ptree.custom_tree -> Cil_types.custom_tree
val funspec : string list ->
Cil_types.varinfo ->
Cil_types.varinfo list option ->
Cil_types.typ -> Logic_ptree.spec -> Cil_types.funspec
funspec behaviors f prms typ spec
type-checks a function contract.