sig
  val lval :
    (Cil_types.kernel_function ->
     Cil_types.stmt -> string -> Cil_types.term_lval)
    Pervasives.ref
  val expr :
    (Cil_types.kernel_function -> Cil_types.stmt -> string -> Cil_types.term)
    Pervasives.ref
  val term_lval_to_lval :
    (result:Cil_types.varinfo option -> Cil_types.term_lval -> Cil_types.lval)
    Pervasives.ref
  val term_to_lval :
    (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.lval)
    Pervasives.ref
  val term_to_exp :
    (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.exp)
    Pervasives.ref
  val loc_to_exp :
    (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.exp list)
    Pervasives.ref
  val loc_to_lval :
    (result:Cil_types.varinfo option -> Cil_types.term -> Cil_types.lval list)
    Pervasives.ref
  val term_offset_to_offset :
    (result:Cil_types.varinfo option ->
     Cil_types.term_offset -> Cil_types.offset)
    Pervasives.ref
  val loc_to_offset :
    (result:Cil_types.varinfo option ->
     Cil_types.term -> Cil_types.offset list)
    Pervasives.ref
  val loc_to_loc :
    (result:Cil_types.varinfo option ->
     Db.Value.state -> Cil_types.term -> Locations.location)
    Pervasives.ref
  val loc_to_locs :
    (result:Cil_types.varinfo option ->
     Db.Value.state ->
     Cil_types.term -> Locations.location list * Locations.Zone.t)
    Pervasives.ref
  module To_zone :
    sig
      type t_ctx = {
        state_opt : bool option;
        ki_opt : (Cil_types.stmt * bool) option;
        kf : Kernel_function.t;
      }
      val mk_ctx_func_contrat :
        (Cil_types.kernel_function ->
         state_opt:bool option -> Db.Properties.Interp.To_zone.t_ctx)
        Pervasives.ref
      val mk_ctx_stmt_contrat :
        (Cil_types.kernel_function ->
         Cil_types.stmt ->
         state_opt:bool option -> Db.Properties.Interp.To_zone.t_ctx)
        Pervasives.ref
      val mk_ctx_stmt_annot :
        (Cil_types.kernel_function ->
         Cil_types.stmt -> Db.Properties.Interp.To_zone.t_ctx)
        Pervasives.ref
      type t = {
        before : bool;
        ki : Cil_types.stmt;
        zone : Locations.Zone.t;
      }
      type t_zone_info = Db.Properties.Interp.To_zone.t list option
      type t_decl = {
        var : Cil_datatype.Varinfo.Set.t;
        lbl : Cil_datatype.Logic_label.Set.t;
      }
      type t_pragmas = {
        ctrl : Cil_datatype.Stmt.Set.t;
        stmt : Cil_datatype.Stmt.Set.t;
      }
      val from_term :
        (Cil_types.term ->
         Db.Properties.Interp.To_zone.t_ctx ->
         Db.Properties.Interp.To_zone.t_zone_info *
         Db.Properties.Interp.To_zone.t_decl)
        Pervasives.ref
      val from_terms :
        (Cil_types.term list ->
         Db.Properties.Interp.To_zone.t_ctx ->
         Db.Properties.Interp.To_zone.t_zone_info *
         Db.Properties.Interp.To_zone.t_decl)
        Pervasives.ref
      val from_pred :
        (Cil_types.predicate Cil_types.named ->
         Db.Properties.Interp.To_zone.t_ctx ->
         Db.Properties.Interp.To_zone.t_zone_info *
         Db.Properties.Interp.To_zone.t_decl)
        Pervasives.ref
      val from_preds :
        (Cil_types.predicate Cil_types.named list ->
         Db.Properties.Interp.To_zone.t_ctx ->
         Db.Properties.Interp.To_zone.t_zone_info *
         Db.Properties.Interp.To_zone.t_decl)
        Pervasives.ref
      val from_zone :
        (Cil_types.identified_term ->
         Db.Properties.Interp.To_zone.t_ctx ->
         Db.Properties.Interp.To_zone.t_zone_info *
         Db.Properties.Interp.To_zone.t_decl)
        Pervasives.ref
      val from_stmt_annot :
        (Cil_types.code_annotation ->
         Cil_types.stmt * Cil_types.kernel_function ->
         (Db.Properties.Interp.To_zone.t_zone_info *
          Db.Properties.Interp.To_zone.t_decl) *
         Db.Properties.Interp.To_zone.t_pragmas)
        Pervasives.ref
      val from_stmt_annots :
        ((Cil_types.code_annotation -> bool) option ->
         Cil_types.stmt * Cil_types.kernel_function ->
         (Db.Properties.Interp.To_zone.t_zone_info *
          Db.Properties.Interp.To_zone.t_decl) *
         Db.Properties.Interp.To_zone.t_pragmas)
        Pervasives.ref
      val from_func_annots :
        (((Cil_types.stmt -> unit) -> Cil_types.kernel_function -> unit) ->
         (Cil_types.code_annotation -> bool) option ->
         Cil_types.kernel_function ->
         (Db.Properties.Interp.To_zone.t_zone_info *
          Db.Properties.Interp.To_zone.t_decl) *
         Db.Properties.Interp.To_zone.t_pragmas)
        Pervasives.ref
      val code_annot_filter :
        (Cil_types.code_annotation ->
         threat:bool ->
         user_assert:bool ->
         slicing_pragma:bool ->
         loop_inv:bool -> loop_var:bool -> others:bool -> bool)
        Pervasives.ref
    end
  val to_result_from_pred :
    (Cil_types.predicate Cil_types.named -> bool) Pervasives.ref
  val code_annot :
    (Cil_types.kernel_function ->
     Cil_types.stmt -> string -> Cil_types.code_annotation)
    Pervasives.ref
end