sig
  val clear_call_stack : unit -> unit
  val pop_call_stack : unit -> unit
  val push_call_stack : Cil_types.kernel_function -> Cil_types.kinstr -> unit
  val current_kf : unit -> Cil_types.kernel_function
  val call_stack : unit -> Value_types.callstack
  val pp_callstack : Stdlib.Format.formatter -> unit
  val emitter : Emitter.t
  val get_slevel : Kernel_function.t -> Value_parameters.SlevelFunction.value
  val get_subdivision : Cil_types.stmt -> int
  val pretty_actuals :
    Stdlib.Format.formatter -> (Cil_types.exp * Cvalue.V.t) list -> unit
  val pretty_current_cfunction_name : Stdlib.Format.formatter -> unit
  val warning_once_current :
    ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a
  val alarm_report : 'Log.pretty_printer
  module DegenerationPoints :
    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 = Cil_types.stmt
      type data = bool
      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 create_new_var : string -> Cil_types.typ -> Cil_types.varinfo
  val is_const_write_invalid : Cil_types.typ -> bool
  val postconditions_mention_result : Cil_types.funspec -> bool
  val conv_comp : Cil_types.binop -> Abstract_interp.Comp.t
  val conv_relation : Cil_types.relation -> Abstract_interp.Comp.t
  val normalize_as_cond : Cil_types.exp -> bool -> Cil_types.exp
  val is_value_zero : Cil_types.exp -> bool
  val lval_to_exp : Cil_types.lval -> Cil_types.exp
  val dump_garbled_mix : unit -> unit
  val zone_of_expr :
    (Cil_types.lval -> Precise_locs.precise_location) ->
    Cil_types.exp -> Locations.Zone.t
  val indirect_zone_of_lval :
    (Cil_types.lval -> Precise_locs.precise_location) ->
    Cil_types.lval -> Locations.Zone.t
  val height_expr : Cil_types.exp -> int
  val height_lval : Cil_types.lval -> int
  val skip_specifications : Cil_types.kernel_function -> bool
end