sig
val is_extension : string -> bool
val is_extension_block : string -> bool
val extension_category : string -> Cil_types.ext_category
val preprocess_extension :
string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list
val preprocess_extension_block :
string ->
string * Logic_ptree.extended_decl list ->
string * Logic_ptree.extended_decl list
module Logic_info :
sig
val self : State.t
val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit
val is_computed : ?project:Project.t -> unit -> bool
module Datatype : Datatype.S
val add_hook_on_update : (Datatype.t -> unit) -> unit
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
type key = string
type data = Cil_types.logic_info list
val replace : key -> data -> unit
val add : key -> data -> unit
val clear : unit -> unit
val length : unit -> int
val iter : (key -> data -> unit) -> unit
val iter_sorted :
?cmp:(key -> key -> int) -> (key -> data -> unit) -> unit
val fold : (key -> data -> 'a -> 'a) -> 'a -> 'a
val fold_sorted :
?cmp:(key -> key -> int) -> (key -> data -> 'a -> 'a) -> 'a -> 'a
val memo : ?change:(data -> data) -> (key -> data) -> key -> data
val find : key -> data
val find_all : key -> data list
val mem : key -> bool
val remove : key -> unit
end
module Logic_type_info :
sig
val self : State.t
val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit
val is_computed : ?project:Project.t -> unit -> bool
module Datatype : Datatype.S
val add_hook_on_update : (Datatype.t -> unit) -> unit
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
type key = string
type data = Cil_types.logic_type_info
val replace : key -> data -> unit
val add : key -> data -> unit
val clear : unit -> unit
val length : unit -> int
val iter : (key -> data -> unit) -> unit
val iter_sorted :
?cmp:(key -> key -> int) -> (key -> data -> unit) -> unit
val fold : (key -> data -> 'a -> 'a) -> 'a -> 'a
val fold_sorted :
?cmp:(key -> key -> int) -> (key -> data -> 'a -> 'a) -> 'a -> 'a
val memo : ?change:(data -> data) -> (key -> data) -> key -> data
val find : key -> data
val find_all : key -> data list
val mem : key -> bool
val remove : key -> unit
end
module Logic_ctor_info :
sig
val self : State.t
val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit
val is_computed : ?project:Project.t -> unit -> bool
module Datatype : Datatype.S
val add_hook_on_update : (Datatype.t -> unit) -> unit
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
type key = string
type data = Cil_types.logic_ctor_info
val replace : key -> data -> unit
val add : key -> data -> unit
val clear : unit -> unit
val length : unit -> int
val iter : (key -> data -> unit) -> unit
val iter_sorted :
?cmp:(key -> key -> int) -> (key -> data -> unit) -> unit
val fold : (key -> data -> 'a -> 'a) -> 'a -> 'a
val fold_sorted :
?cmp:(key -> key -> int) -> (key -> data -> 'a -> 'a) -> 'a -> 'a
val memo : ?change:(data -> data) -> (key -> data) -> key -> data
val find : key -> data
val find_all : key -> data list
val mem : key -> bool
val remove : key -> unit
end
module Model_info :
sig
val self : State.t
val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit
val is_computed : ?project:Project.t -> unit -> bool
module Datatype : Datatype.S
val add_hook_on_update : (Datatype.t -> unit) -> unit
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
type key = string
type data = Cil_types.model_info
val replace : key -> data -> unit
val add : key -> data -> unit
val clear : unit -> unit
val length : unit -> int
val iter : (key -> data -> unit) -> unit
val iter_sorted :
?cmp:(key -> key -> int) -> (key -> data -> unit) -> unit
val fold : (key -> data -> 'a -> 'a) -> 'a -> 'a
val fold_sorted :
?cmp:(key -> key -> int) -> (key -> data -> 'a -> 'a) -> 'a -> 'a
val memo : ?change:(data -> data) -> (key -> data) -> key -> data
val find : key -> data
val find_all : key -> data list
val mem : key -> bool
val remove : key -> unit
end
module Lemmas :
sig
val self : State.t
val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit
val is_computed : ?project:Project.t -> unit -> bool
module Datatype : Datatype.S
val add_hook_on_update : (Datatype.t -> unit) -> unit
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
type key = string
type data = Cil_types.global_annotation
val replace : key -> data -> unit
val add : key -> data -> unit
val clear : unit -> unit
val length : unit -> int
val iter : (key -> data -> unit) -> unit
val iter_sorted :
?cmp:(key -> key -> int) -> (key -> data -> unit) -> unit
val fold : (key -> data -> 'a -> 'a) -> 'a -> 'a
val fold_sorted :
?cmp:(key -> key -> int) -> (key -> data -> 'a -> 'a) -> 'a -> 'a
val memo : ?change:(data -> data) -> (key -> data) -> key -> data
val find : key -> data
val find_all : key -> data list
val mem : key -> bool
val remove : key -> unit
end
val builtin_states : State.t list
val prepare_tables : unit -> unit
val add_logic_function_gen :
(Cil_types.logic_info -> Cil_types.logic_info -> bool) ->
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 add_model_field : Cil_types.model_info -> unit
module Builtins :
sig val apply : unit -> unit val extend : (unit -> unit) -> unit end
module Logic_builtin_used :
sig
val add : string -> Cil_types.logic_info list -> unit
val mem : string -> bool
val iter : (string -> Cil_types.logic_info list -> unit) -> unit
val self : State.t
end
val add_builtin_logic_function_gen :
(Cil_types.builtin_logic_info -> Cil_types.builtin_logic_info -> bool) ->
Cil_types.builtin_logic_info -> unit
val add_builtin_logic_type : string -> Cil_types.logic_type_info -> unit
val add_builtin_logic_ctor : string -> Cil_types.logic_ctor_info -> unit
val is_builtin_logic_function : string -> bool
val is_builtin_logic_type : string -> bool
val is_builtin_logic_ctor : string -> bool
val iter_builtin_logic_function :
(Cil_types.builtin_logic_info -> unit) -> unit
val iter_builtin_logic_type : (Cil_types.logic_type_info -> unit) -> unit
val iter_builtin_logic_ctor : (Cil_types.logic_ctor_info -> unit) -> unit
val find_all_logic_functions : string -> Cil_types.logic_info list
val find_all_model_fields : string -> Cil_types.model_info list
val find_model_field : string -> Cil_types.typ -> Cil_types.model_info
val find_logic_cons : Cil_types.logic_var -> Cil_types.logic_info
val find_logic_type : string -> Cil_types.logic_type_info
val find_logic_ctor : string -> Cil_types.logic_ctor_info
val is_logic_function : string -> bool
val is_logic_type : string -> bool
val is_logic_ctor : string -> bool
val is_model_field : string -> bool
val remove_logic_function : string -> unit
val remove_logic_info_gen :
(Cil_types.logic_info -> Cil_types.logic_info -> bool) ->
Cil_types.logic_info -> unit
val remove_logic_type : string -> unit
val remove_logic_ctor : string -> unit
val remove_model_field : string -> unit
val add_typename : string -> unit
val hide_typename : string -> unit
val remove_typename : string -> unit
val reset_typenames : unit -> unit
val typename_status : string -> bool
val builtin_types_as_typenames : unit -> unit
val set_extension_handler :
category:(string -> Cil_types.ext_category) ->
is_extension:(string -> bool) ->
preprocess:(string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list) ->
is_extension_block:(string -> bool) ->
preprocess_block:(string ->
string * Logic_ptree.extended_decl list ->
string * Logic_ptree.extended_decl list) ->
unit
val init_dependencies : State.t -> unit
end