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 is_list_type : Cil_types.logic_type -> bool
val type_of_list_elem : Cil_types.logic_type -> Cil_types.logic_type
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
val add_var :
string ->
Cil_types.logic_var -> Logic_typing.Lenv.t -> Logic_typing.Lenv.t
val add_type_var :
string ->
Cil_types.logic_type -> Logic_typing.Lenv.t -> Logic_typing.Lenv.t
val add_logic_info :
string ->
Cil_types.logic_info -> Logic_typing.Lenv.t -> Logic_typing.Lenv.t
val add_logic_label :
string ->
Cil_types.logic_label -> Logic_typing.Lenv.t -> Logic_typing.Lenv.t
val find_var : string -> Logic_typing.Lenv.t -> Cil_types.logic_var
val find_type_var :
string -> Logic_typing.Lenv.t -> Cil_types.logic_type
val find_logic_info :
string -> Logic_typing.Lenv.t -> Cil_types.logic_info
val find_logic_label :
string -> Logic_typing.Lenv.t -> Cil_types.logic_label
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 : ?label:string -> 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 Stdlib.ref;
remove_logic_function : string -> unit;
remove_logic_info : Cil_types.logic_info -> 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;
silent : bool;
logic_type :
Logic_typing.typing_context ->
Cil_types.location ->
Logic_typing.Lenv.t -> Logic_ptree.logic_type -> Cil_types.logic_type;
type_predicate :
Logic_typing.typing_context ->
Logic_typing.Lenv.t -> Logic_ptree.lexpr -> Cil_types.predicate;
type_term :
Logic_typing.typing_context ->
Logic_typing.Lenv.t -> Logic_ptree.lexpr -> Cil_types.term;
type_assigns :
Logic_typing.typing_context ->
accept_formal:bool ->
Logic_typing.Lenv.t -> Logic_ptree.assigns -> Cil_types.assigns;
error :
'a 'b.
Cil_types.location ->
('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a;
on_error : 'a 'b. ('a -> 'b) -> (unit -> unit) -> 'a -> 'b;
}
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 : ?label:string -> 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 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
val error :
Cil_types.location ->
('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a
val on_error : ('a -> 'b) -> (unit -> unit) -> 'a -> 'b
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 :
?explicit:bool ->
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
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
val set_extension_handler :
is_extension:(string -> bool) ->
typer:(string ->
Logic_typing.typing_context ->
Cil_types.location ->
Logic_ptree.lexpr list -> bool * Cil_types.acsl_extension_kind) ->
typer_block:(string ->
Logic_typing.typing_context ->
Filepath.position * Filepath.position ->
string * Logic_ptree.extended_decl list ->
bool * Cil_types.acsl_extension_kind) ->
unit
val get_typer :
string ->
typing_context:Logic_typing.typing_context ->
loc:Filepath.position * Filepath.position ->
Logic_ptree.lexpr list -> bool * Cil_types.acsl_extension_kind
val get_typer_block :
string ->
typing_context:Logic_typing.typing_context ->
loc:Logic_ptree.location ->
string * Logic_ptree.extended_decl list ->
bool * Cil_types.acsl_extension_kind
end