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 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 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.
Raises Not_found if the index is out of bounds.

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).
Raises Invalid_argument if the index is out of bounds.

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

replace a step in the sequent, the one at the specified position.
Raises Invalid_argument if the index is out of bounds.

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

Performs existential, universal and hypotheses introductions

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

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

exception Contradiction

class type simplifier = object .. end

val clean : sequent -> sequent

val filter : sequent -> sequent

val letify : ?solvers:simplifier list ->
       ?intros:int -> sequent -> sequent

val pruning : ?solvers:simplifier list ->
       sequent -> sequent