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 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
      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 : 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 init_dependencies : State.t -> unit
end