sig
  module Interp :
    sig
      val term_lval :
        (Cil_types.kernel_function ->
         ?loc:Cil_types.location ->
         ?env:Logic_typing.Lenv.t -> string -> Cil_types.term_lval)
        Pervasives.ref
      val term :
        (Cil_types.kernel_function ->
         ?loc:Cil_types.location ->
         ?env:Logic_typing.Lenv.t -> string -> Cil_types.term)
        Pervasives.ref
      val predicate :
        (Cil_types.kernel_function ->
         ?loc:Cil_types.location ->
         ?env:Logic_typing.Lenv.t ->
         string -> Cil_types.predicate Cil_types.named)
        Pervasives.ref
      val code_annot :
        (Cil_types.kernel_function ->
         Cil_types.stmt -> string -> Cil_types.code_annotation)
        Pervasives.ref
      exception No_conversion
      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_loc_under_over :
        (result:Cil_types.varinfo option ->
         Db.Value.state ->
         Cil_types.term ->
         Locations.location * Locations.location * 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
    end
  val add_assert :
    Emitter.t ->
    Cil_types.kernel_function -> Cil_types.stmt -> string -> unit
end