module Conditions:sig
..end
val forall_intro : Wp.Lang.F.pred -> Wp.Lang.F.pred list * Wp.Lang.F.pred
val exist_intro : Wp.Lang.F.pred -> Wp.Lang.F.pred
type
step = private {
|
mutable id : |
(* |
See
index | *) |
|
size : |
|||
|
vars : |
|||
|
stmt : |
|||
|
descr : |
|||
|
deps : |
|||
|
warn : |
|||
|
condition : |
type
condition =
| |
Type of |
(* |
Type section, not constraining for filtering
| *) |
| |
Have of |
(* |
Normal assumptions section
| *) |
| |
When of |
(* |
Assumptions introduced after simplifications
| *) |
| |
Core of |
(* |
Common hypotheses gather from parallel branches
| *) |
| |
Init of |
(* |
Initializers assumptions
| *) |
| |
Branch of |
(* |
If-Then-Else
| *) |
| |
Either of |
(* |
Disjunction
| *) |
| |
State of |
(* |
Memory Model snapshot
| *) |
type
sequence
typesequent =
sequence * Wp.Lang.F.pred
val pretty : (Format.formatter -> sequent -> unit) Pervasives.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
descr
, deps
and warn
val is_true : sequence -> bool
val is_empty : sequence -> bool
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
val list : sequence -> step list
iter
.val size : sequence -> int
val steps : sequence -> int
step.id
in the sequence,
starting from zero. Recursively
Returns the number of steps in the sequence.val index : sequent -> unit
ignore (steps (fst s))
.val step_at : sequence -> int -> step
id
in the sequence.
The index
function must have been called on the sequence before
retrieving the index properly.Not_found
if the index is out of bounds.val is_trivial : sequent -> bool
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
at
the specified position.
Parameter at
can be size
to insert at the end of the sequent (default).Invalid_argument
if the index is out of bounds.val replace : at:int ->
step -> sequent -> sequent
at
the specified position.Invalid_argument
if the index is out of bounds.val subst : (Wp.Lang.F.term -> Wp.Lang.F.term) ->
sequent -> sequent
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.
f
should raise Not_found
on terms that must not be replacedval introduction : sequent -> sequent option
val introduction_eq : sequent -> sequent
introduction
but returns the same sequent is Noneval lemma : Wp.Lang.F.pred -> sequent
val head : step -> Wp.Lang.F.pred
val have : step -> Wp.Lang.F.pred
val condition : sequence -> Wp.Lang.F.pred
val close : sequent -> Wp.Lang.F.pred
val at_closure : (sequent -> sequent) -> unit
Bundles are mergeable pre-sequences. This the key structure for merging hypotheses with linear complexity during backward weakest pre-condition calculus.
Bundle are constructed in backward order with respect to program
control-flow, as driven by the wp 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
Type
section on top of the bundle.val intros : Wp.Lang.F.pred list -> bundle -> bundle
Have
section on top of the bundle.val state : ?descr:string ->
?stmt:Cil_types.stmt ->
Wp.Mstate.state -> bundle -> bundle
val assume : (?init:bool ->
?domain:bool ->
Wp.Lang.F.pred -> bundle -> bundle)
attributed
~init:true
, the predicate is placed
in an Init
section. On ~domain:true
, the predicate is placed in a Type
section. Otherwized, it is placed in a standard Have
section.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
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