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)         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 ->              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 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 -> bool) Pervasives.ref     end   val add_assert :     Emitter.t ->     Cil_types.kernel_function -> Cil_types.stmt -> string -> unit end