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