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