Module Wp.Conditions

module Conditions: sig .. end

Sequent

type step = private {
   mutable id : int; (*

See index

*)
   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 : condition;
}
type 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 * sequence * sequence
| Either of sequence list
| State of Wp.Mstate.state
type sequence 

List of steps

type sequent = sequence * Wp.Lang.F.pred 
val pretty : (Stdlib.Format.formatter -> sequent -> unit) Stdlib.ref
val step : ?descr:string ->
?stmt:Cil_types.stmt ->
?deps:Property.t list ->
?warn:Wp.Warning.Set.t -> condition -> step
val update_cond : ?descr:string ->
?deps:Property.t list ->
?warn:Wp.Warning.Set.t ->
step -> condition -> step

Updates the condition of a step and merges descr, deps and warn

val is_true : sequence -> bool

Only true or empty steps

val is_empty : sequence -> bool

No step at all

val vars_hyp : sequence -> Wp.Lang.F.Vars.t
val vars_seq : sequent -> Wp.Lang.F.Vars.t
val empty : sequence
val trivial : sequent
val sequence : step list -> sequence
val seq_branch : ?stmt:Cil_types.stmt ->
Wp.Lang.F.pred ->
sequence -> sequence -> sequence
val append : sequence -> sequence -> sequence
val concat : sequence list -> sequence
val iter : (step -> unit) -> sequence -> unit

Iterate only over the head steps of the sequence

val list : sequence -> step list

The internal list of steps

val size : sequence -> int
val steps : sequence -> int

Attributes unique indices to every step.id in the sequence, starting from zero. Returns the number of steps in the sequence.

val index : sequent -> unit

Compute steps' id of sequent left hand-side. Same as ignore (steps (fst s)).

val step_at : sequence -> int -> step

Retrieve a step by id in the sequence. The index function must have been called on the sequence before retrieving the index properly.

val is_trivial : sequent -> bool

Transformations

val map_condition : (Wp.Lang.F.pred -> Wp.Lang.F.pred) ->
condition -> condition
val map_step : (Wp.Lang.F.pred -> Wp.Lang.F.pred) ->
step -> step
val map_sequence : (Wp.Lang.F.pred -> Wp.Lang.F.pred) ->
sequence -> sequence
val map_sequent : (Wp.Lang.F.pred -> Wp.Lang.F.pred) ->
sequent -> sequent
val insert : ?at:int ->
step -> sequent -> sequent

Insert a step in the sequent immediately at the specified position. Parameter at can be size to insert at the end of the sequent (default).

val replace : at:int ->
step -> sequent -> sequent

replace a step in the sequent, the one at the specified position.

val subst : (Wp.Lang.F.term -> Wp.Lang.F.term) ->
sequent -> sequent

Apply the atomic substitution recursively using Lang.F.p_subst f. Function f should only transform the head of the predicate, and can assume its sub-terms have been already substituted. The atomic substitution is also applied to predicates.

val introduction : sequent -> sequent option

Performs existential, universal and hypotheses introductions

val introduction_eq : sequent -> sequent

Same as introduction but returns the same sequent is None

val lemma : Wp.Lang.F.pred -> sequent

Performs existential, universal and hypotheses introductions

val head : step -> Wp.Lang.F.pred

Predicate for Have and such, Condition for Branch, True for Either

val have : step -> Wp.Lang.F.pred

Predicate for Have and such, True for any other

val condition : sequence -> Wp.Lang.F.pred

With free variables kept.

val close : sequent -> Wp.Lang.F.pred

With free variables quantified.

val at_closure : (sequent -> sequent) -> unit

register a transformation applied just before close

Bundles

Bundles are mergeable pre-sequences. This the key structure for merging hypotheses with linear complexity during backward weakest pre-condition calculus.

type bundle 
type 'a attributed = ?descr:string ->
?stmt:Cil_types.stmt -> ?deps:Property.t list -> ?warn:Wp.Warning.Set.t -> 'a
val nil : bundle
val occurs : Wp.Lang.F.var -> bundle -> bool
val intersect : Wp.Lang.F.pred -> bundle -> bool
val merge : bundle list -> bundle
val domain : Wp.Lang.F.pred list -> bundle -> bundle
val intros : Wp.Lang.F.pred list -> bundle -> bundle
val state : ?descr:string ->
?stmt:Cil_types.stmt ->
Wp.Mstate.state -> bundle -> bundle
val assume : (?init:bool -> Wp.Lang.F.pred -> bundle -> bundle)
attributed
val branch : (Wp.Lang.F.pred ->
bundle -> bundle -> bundle)
attributed
val either : (bundle list -> bundle) attributed
val extract : bundle -> Wp.Lang.F.pred list
val bundle : bundle -> sequence

Simplifier

val clean : sequent -> sequent
val filter : sequent -> sequent
val parasite : sequent -> sequent
val simplify : ?solvers:Wp.Lang.simplifier list ->
?intros:int -> sequent -> sequent
val pruning : ?solvers:Wp.Lang.simplifier list ->
sequent -> sequent