sig   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) -> ('-> Datatype.t) -> unit       type key = string       type data = Cil_types.logic_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       val fold_sorted :         ?cmp:(key -> key -> int) -> (key -> data -> '-> '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) -> ('-> 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       val fold_sorted :         ?cmp:(key -> key -> int) -> (key -> data -> '-> '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) -> ('-> 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       val fold_sorted :         ?cmp:(key -> key -> int) -> (key -> data -> '-> '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) -> ('-> 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       val fold_sorted :         ?cmp:(key -> key -> int) -> (key -> data -> '-> '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) -> ('-> 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       val fold_sorted :         ?cmp:(key -> key -> int) -> (key -> data -> '-> '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 : Cil_types.logic_info -> unit       val mem : Cil_types.logic_info -> bool       val iter : (Cil_types.logic_info -> 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_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 init_dependencies : State.t -> unit end