Wp.Conditions
Proof Task and Simplifiers
val forall_intro : Lang.F.pred -> Lang.F.pred list * Lang.F.pred
Introduce universally quantified formulae: head forall quantifiers are instanciated to fresh variables in current pool and left-implies are extracted, recursively.
val exist_intro : Lang.F.pred -> Lang.F.pred
Introduce existential quantified formulae: head exist quantifiers are instanciated to fresh variables, recursively.
type step = private {
mutable id : int;
See index
size : int;
vars : Lang.F.Vars.t;
stmt : Frama_c_kernel.Cil_types.stmt option;
descr : string option;
deps : Frama_c_kernel.Property.t list;
warn : Wp__.Warning.Set.t;
condition : condition;
}
and condition =
| Type of Lang.F.pred
Type section, not constraining for filtering
*)| Have of Lang.F.pred
Normal assumptions section
*)| When of Lang.F.pred
Assumptions introduced after simplifications
*)| Core of Lang.F.pred
Common hypotheses gather from parallel branches
*)| Init of Lang.F.pred
Initializers assumptions
*)| Branch of Lang.F.pred * sequence * sequence
If-Then-Else
*)| Either of sequence list
Disjunction
*)| State of Mstate.state
Memory Model snapshot
*)type sequent = sequence * Lang.F.pred
val pretty : (Stdlib.Format.formatter -> sequent -> unit) Stdlib.ref
val step :
?descr:string ->
?stmt:Frama_c_kernel.Cil_types.stmt ->
?deps:Frama_c_kernel.Property.t list ->
?warn:Wp__.Warning.Set.t ->
condition ->
step
Creates a single step
val update_cond :
?descr:string ->
?deps:Frama_c_kernel.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
Contains only true or empty steps
val is_empty : sequence -> bool
No step at all
val vars_hyp : sequence -> Lang.F.Vars.t
Pre-computed and available in constant time.
val vars_seq : sequent -> Lang.F.Vars.t
At the cost of the union of hypotheses and goal.
val empty : sequence
empty sequence, equivalent to true assumption
val trivial : sequent
empty implies true
val seq_branch :
?stmt:Frama_c_kernel.Cil_types.stmt ->
Lang.F.pred ->
sequence ->
sequence ->
sequence
Creates an If-Then-Else branch located at the provided stmt, if any.
Iterate only over the head steps of the sequence. Does not go deeper inside branches and disjunctions.
val size : sequence -> int
Compute the total number of steps in the sequence, including nested sequences from branches and disjunctions. Pre-computed and available in constant time.
val steps : sequence -> int
Attributes unique indices to every step.id
in the sequence, starting from zero. Recursively 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))
.
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
Goal is true or hypotheses contains false.
val probes : sequence -> Lang.F.term Wp__.Probe.Map.t
Collect all probes in the sequence
val map_condition : (Lang.F.pred -> Lang.F.pred) -> condition -> condition
Rewrite all root predicates in condition
val map_step : (Lang.F.pred -> Lang.F.pred) -> step -> step
Rewrite all root predicates in step
val map_sequence : (Lang.F.pred -> Lang.F.pred) -> sequence -> sequence
Rewrite all root predicates in sequence
val map_sequent : (Lang.F.pred -> Lang.F.pred) -> sequent -> sequent
Rewrite all root predicates in hypotheses and goal
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).
replace a step in the sequent, the one at
the specified position.
replace a step in the sequent, the one at
the specified position.
val subst : (Lang.F.term -> 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. f
should raise Not_found
on terms that must not be replaced
Performs existential, universal and hypotheses introductions
val lemma : loc:Frama_c_kernel.Cil_types.location -> Lang.F.pred -> sequent
Performs existential, universal and hypotheses introductions
val head : step -> Lang.F.pred
Predicate for Have and such, Condition for Branch, True for Either
val have : step -> Lang.F.pred
Predicate for Have and such, True for any other
val pred_cond : condition -> Lang.F.pred
val condition : sequence -> Lang.F.pred
With free variables kept.
val property : sequent -> Lang.F.pred
With free variables kept.
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 'a attributed =
?descr:string ->
?stmt:Frama_c_kernel.Cil_types.stmt ->
?deps:Frama_c_kernel.Property.t list ->
?warn:Wp__.Warning.Set.t ->
'a
val nil : bundle
Same as empty
val occurs : Lang.F.var -> bundle -> bool
val intersect : Lang.F.pred -> bundle -> bool
Variables of predicate and the bundle intersects
Performs a diff-based disjunction, introducing If-Then-Else or Either branches when possible. Linear complexity is achieved by assuming bundle ordering is consistent over the list.
val probe :
loc:Frama_c_kernel.Cil_types.location ->
?descr:string ->
?stmt:Frama_c_kernel.Cil_types.stmt ->
name:string ->
Lang.F.term ->
bundle ->
bundle
Inserts probes to a sequent.
val domain : Lang.F.pred list -> bundle -> bundle
Assumes a list of predicates in a Type
section on top of the bundle.
val intros : Lang.F.pred list -> bundle -> bundle
Assumes a list of predicates in a Have
section on top of the bundle.
val state :
?descr:string ->
?stmt:Frama_c_kernel.Cil_types.stmt ->
Mstate.state ->
bundle ->
bundle
Stack a memory model state on top of the bundle.
val assume :
(?init:bool -> ?domain:bool -> Lang.F.pred -> bundle -> bundle) attributed
Assumes a predicate in the specified section, with the specified decorations. On ~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 : (Lang.F.pred -> bundle -> bundle -> bundle) attributed
Construct a branch bundle, with merging of all common parts.
val either : (bundle list -> bundle) attributed
Construct a disjunction bundle, with merging of all common parts.
val extract : bundle -> Lang.F.pred list
Computes a formulae equivalent to the bundle. For debugging purpose only.
val simplify :
?solvers:Lang.simplifier list ->
?intros:int ->
sequent ->
sequent
val pruning : ?solvers:Lang.simplifier list -> sequent -> sequent