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