sig
val type_rel : Logic_ptree.relation -> Cil_types.relation
val type_binop : Logic_ptree.binop -> Cil_types.binop
val unescape : string -> string
val wcharlist_of_string : string -> int64 list
val is_arithmetic_type : Cil_types.logic_type -> bool
val is_integral_type : Cil_types.logic_type -> bool
val is_set_type : Cil_types.logic_type -> bool
val is_array_type : Cil_types.logic_type -> bool
val is_pointer_type : Cil_types.logic_type -> bool
val type_of_pointed : Cil_types.logic_type -> Cil_types.logic_type
val type_of_array_elem : Cil_types.logic_type -> Cil_types.logic_type
val type_of_set_elem : Cil_types.logic_type -> Cil_types.logic_type
val ctype_of_pointed : Cil_types.logic_type -> Cil_types.typ
val ctype_of_array_elem : Cil_types.logic_type -> Cil_types.typ
val add_offset_lval :
Cil_types.term_offset -> Cil_types.term_lval -> Cil_types.term_lval
val arithmetic_conversion :
Cil_types.logic_type -> Cil_types.logic_type -> Cil_types.logic_type
module Lenv : sig type t val empty : unit -> Logic_typing.Lenv.t end
type type_namespace = Typedef | Struct | Union | Enum
module Type_namespace :
sig
type t = type_namespace
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
type typing_context = {
is_loop : unit -> bool;
anonCompFieldName : string;
conditionalConversion : Cil_types.typ -> Cil_types.typ -> Cil_types.typ;
find_macro : string -> Logic_ptree.lexpr;
find_var : string -> Cil_types.logic_var;
find_enum_tag : string -> Cil_types.exp * Cil_types.typ;
find_comp_field : Cil_types.compinfo -> string -> Cil_types.offset;
find_type : Logic_typing.type_namespace -> string -> Cil_types.typ;
find_label : string -> Cil_types.stmt Pervasives.ref;
remove_logic_function : string -> unit;
remove_logic_type : string -> unit;
remove_logic_ctor : string -> unit;
add_logic_function : Cil_types.logic_info -> unit;
add_logic_type : string -> Cil_types.logic_type_info -> unit;
add_logic_ctor : string -> Cil_types.logic_ctor_info -> unit;
find_all_logic_functions : string -> Cil_types.logic_info list;
find_logic_type : string -> Cil_types.logic_type_info;
find_logic_ctor : string -> Cil_types.logic_ctor_info;
pre_state : Logic_typing.Lenv.t;
post_state : Cil_types.termination_kind list -> Logic_typing.Lenv.t;
assigns_env : Logic_typing.Lenv.t;
type_predicate :
Logic_typing.Lenv.t ->
Logic_ptree.lexpr -> Cil_types.predicate Cil_types.named;
type_term : Logic_typing.Lenv.t -> Logic_ptree.lexpr -> Cil_types.term;
type_assigns :
accept_formal:bool ->
Logic_typing.Lenv.t ->
Logic_ptree.lexpr Cil_types.assigns ->
Cil_types.identified_term Cil_types.assigns;
error :
'a.
Cil_types.location ->
('a, Format.formatter, unit) Pervasives.format -> 'a;
}
val register_behavior_extension :
string ->
(typing_context:Logic_typing.typing_context ->
loc:Cil_types.location ->
Cil_types.funbehavior -> Logic_ptree.lexpr list -> unit) ->
unit
module Make :
functor
(C : sig
val is_loop : unit -> bool
val anonCompFieldName : string
val conditionalConversion :
Cil_types.typ -> Cil_types.typ -> Cil_types.typ
val find_macro : string -> Logic_ptree.lexpr
val find_var : string -> Cil_types.logic_var
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 Pervasives.ref
val remove_logic_function : string -> 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
end) ->
sig
val type_of_field :
Cil_types.location ->
string ->
Cil_types.logic_type ->
Cil_types.term_offset * Cil_types.logic_type
val mk_cast :
Cil_types.term -> Cil_types.logic_type -> Cil_types.term
val term : Logic_typing.Lenv.t -> Logic_ptree.lexpr -> Cil_types.term
val predicate :
Logic_typing.Lenv.t ->
Logic_ptree.lexpr -> Cil_types.predicate Cil_types.named
val code_annot :
Cil_types.location ->
string list ->
Cil_types.logic_type ->
Logic_ptree.code_annot -> Cil_types.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
end
val append_old_and_post_labels : Logic_typing.Lenv.t -> Logic_typing.Lenv.t
val append_here_label : Logic_typing.Lenv.t -> Logic_typing.Lenv.t
val append_pre_label : Logic_typing.Lenv.t -> Logic_typing.Lenv.t
val append_init_label : Logic_typing.Lenv.t -> Logic_typing.Lenv.t
val add_var :
string ->
Cil_types.logic_var -> Logic_typing.Lenv.t -> Logic_typing.Lenv.t
val add_result :
Logic_typing.Lenv.t -> Cil_types.logic_type -> Logic_typing.Lenv.t
val enter_post_state :
Logic_typing.Lenv.t -> Cil_types.termination_kind -> Logic_typing.Lenv.t
val post_state_env :
Cil_types.termination_kind -> Cil_types.logic_type -> Logic_typing.Lenv.t
end