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