Previous  Up  

Functor Logic_typing.Make

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.

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

see Logic_typing.typing_context.

end) -> sig .. end
Parameters:
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 : typ -> typ -> typ val find_macro : string -> Logic_ptree.lexpr val find_var : ?label:string -> string -> logic_var (** see corresponding field in {!Logic_typing.typing_context}. *) val find_enum_tag : string -> exp * typ val find_type : type_namespace -> string -> typ val find_comp_field: compinfo -> string -> offset val find_label : string -> stmt ref val remove_logic_function : string -> unit val remove_logic_info: logic_info -> unit val remove_logic_type: string -> unit val remove_logic_ctor: string -> unit val add_logic_function: logic_info -> unit val add_logic_type: string -> logic_type_info -> unit val add_logic_ctor: string -> logic_ctor_info -> unit val find_all_logic_functions : string -> Cil_types.logic_info list val find_logic_type: string -> logic_type_info val find_logic_ctor: string -> logic_ctor_info (** What to do when we have a term of type Integer in a context expecting a C integral type. @raise Failure to reject such conversion @since Nitrogen-20111001 *) val integral_cast: Cil_types.typ -> Cil_types.term -> Cil_types.term (** raises an error at the given location and with the given message. @since Magnesium-20151001 *) val error: location -> ('a,Format.formatter,unit, 'b) format4 -> 'a (** see {!Logic_typing.typing_context}. *) val on_error: ('a -> 'b) -> ((location * string) -> unit) -> 'a -> 'b end 
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 false
val 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 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.