sig
type step = private {
size : int;
vars : Wp.Lang.F.Vars.t;
stmt : Cil_types.stmt option;
descr : string option;
deps : Property.t list;
warn : Wp.Warning.Set.t;
condition : Wp.Conditions.condition;
}
and condition =
Type of Wp.Lang.F.pred
| Have of Wp.Lang.F.pred
| When of Wp.Lang.F.pred
| Core of Wp.Lang.F.pred
| Init of Wp.Lang.F.pred
| Branch of Wp.Lang.F.pred * Wp.Conditions.sequence *
Wp.Conditions.sequence
| Either of Wp.Conditions.sequence list
and sequence
type sequent = Wp.Conditions.sequence * Wp.Lang.F.pred
val step :
?descr:string ->
?stmt:Cil_types.stmt ->
?deps:Property.t list ->
?warn:Wp.Warning.Set.t -> Wp.Conditions.condition -> Wp.Conditions.step
val is_empty : Wp.Conditions.sequence -> bool
val vars_hyp : Wp.Conditions.sequence -> Wp.Lang.F.Vars.t
val vars_seq : Wp.Conditions.sequent -> Wp.Lang.F.Vars.t
val empty : Wp.Conditions.sequence
val seq_list : Wp.Conditions.step list -> Wp.Conditions.sequence
val seq_branch :
?stmt:Cil_types.stmt ->
Wp.Lang.F.pred ->
Wp.Conditions.sequence ->
Wp.Conditions.sequence -> Wp.Conditions.sequence
val append :
Wp.Conditions.sequence ->
Wp.Conditions.sequence -> Wp.Conditions.sequence
val concat : Wp.Conditions.sequence list -> Wp.Conditions.sequence
val iter : (Wp.Conditions.step -> unit) -> Wp.Conditions.sequence -> unit
val iteri :
?from:int ->
(int -> Wp.Conditions.step -> unit) -> Wp.Conditions.sequence -> unit
val condition : Wp.Conditions.sequence -> Wp.Lang.F.pred
val close : Wp.Conditions.sequent -> Wp.Lang.F.pred
type bundle
type 'a attributed =
?descr:string ->
?stmt:Cil_types.stmt ->
?deps:Property.t list -> ?warn:Wp.Warning.Set.t -> 'a
val nil : Wp.Conditions.bundle
val occurs : Wp.Lang.F.var -> Wp.Conditions.bundle -> bool
val intersect : Wp.Lang.F.pred -> Wp.Conditions.bundle -> bool
val merge : Wp.Conditions.bundle list -> Wp.Conditions.bundle
val domain :
Wp.Lang.F.pred list -> Wp.Conditions.bundle -> Wp.Conditions.bundle
val intros :
Wp.Lang.F.pred list -> Wp.Conditions.bundle -> Wp.Conditions.bundle
val assume :
(?init:bool ->
Wp.Lang.F.pred -> Wp.Conditions.bundle -> Wp.Conditions.bundle)
Wp.Conditions.attributed
val branch :
(Wp.Lang.F.pred ->
Wp.Conditions.bundle -> Wp.Conditions.bundle -> Wp.Conditions.bundle)
Wp.Conditions.attributed
val either :
(Wp.Conditions.bundle list -> Wp.Conditions.bundle)
Wp.Conditions.attributed
val extract : Wp.Conditions.bundle -> Wp.Lang.F.pred list
val sequence : Wp.Conditions.bundle -> Wp.Conditions.sequence
exception Contradiction
class type simplifier =
object
method assume : Wp.Lang.F.pred -> unit
method copy : Wp.Conditions.simplifier
method fixpoint : unit
method infer : Wp.Lang.F.pred list
method name : string
method simplify_branch : Wp.Lang.F.pred -> Wp.Lang.F.pred
method simplify_goal : Wp.Lang.F.pred -> Wp.Lang.F.pred
method simplify_hyp : Wp.Lang.F.pred -> Wp.Lang.F.pred
method target : Wp.Lang.F.pred -> unit
end
val clean : Wp.Conditions.sequent -> Wp.Conditions.sequent
val filter : Wp.Conditions.sequent -> Wp.Conditions.sequent
val letify :
?solvers:Wp.Conditions.simplifier list ->
Wp.Conditions.sequent -> Wp.Conditions.sequent
val pruning :
?solvers:Wp.Conditions.simplifier list ->
Wp.Conditions.sequent -> Wp.Conditions.sequent
end