package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-wp.core/Wp/Conditions/index.html

Module `Wp.Conditions`Source

Proof Task and Simplifiers

Predicate Introduction

Sourceval 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.

Sourceval exist_intro : Lang.F.pred -> Lang.F.pred

Introduce existential quantified formulae: head exist quantifiers are instanciated to fresh variables, recursively.

Sequent

Sourcetype 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 : Warning.Set.t;
condition : condition;

}

Sourceand 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
*)
| Probe of Wp__.Probe.probe * Lang.F.term
(*
Named probes
*)

Sourceand sequence

List of steps

Sourcetype sequent = sequence * Lang.F.pred

Sourceval pretty : (Format.formatter -> sequent -> unit) ref

Sourceval equal : sequent -> sequent -> bool

Source

val step : 
  ?descr:string ->
  ?stmt:Frama_c_kernel.Cil_types.stmt ->
  ?deps:Frama_c_kernel.Property.t list ->
  ?warn:Warning.Set.t ->
  condition ->
  step

Creates a single step

Source

val update_cond : 
  ?descr:string ->
  ?deps:Frama_c_kernel.Property.t list ->
  ?warn:Warning.Set.t ->
  step ->
  condition ->
  step

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

Sourceval is_true : sequence -> bool

Contains only true or empty steps

Sourceval is_empty : sequence -> bool

No step at all

Sourceval vars_hyp : sequence -> Lang.F.Vars.t

Pre-computed and available in constant time.

Sourceval vars_seq : sequent -> Lang.F.Vars.t

At the cost of the union of hypotheses and goal.

Sourceval empty : sequence

empty sequence, equivalent to true assumption

Sourceval trivial : sequent

empty implies true

Sourceval sequence : step list -> sequence

Source

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.

Sourceval append : sequence -> sequence -> sequence

Conjunction

Sourceval concat : sequence list -> sequence

List conjunction

Sourceval iter : (step -> unit) -> sequence -> unit

Iterate only over the head steps of the sequence. Does not go deeper inside branches and disjunctions.

Sourceval list : sequence -> step list

Same domain than iter.

Sourceval 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.

Sourceval 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.

Sourceval index : sequent -> unit

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

Sourceval 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.

Sourceval is_trivial : sequent -> bool

Goal is true or hypotheses contains false.

Sourceval probes : sequence -> Lang.F.term Wp__.Probe.Map.t

Collect all probes in the sequence

Transformations

Sourceval map_condition : (Lang.F.pred -> Lang.F.pred) -> condition -> condition

Rewrite all root predicates in condition

Sourceval map_step : (Lang.F.pred -> Lang.F.pred) -> step -> step

Rewrite all root predicates in step

Sourceval map_sequence : (Lang.F.pred -> Lang.F.pred) -> sequence -> sequence

Rewrite all root predicates in sequence

Sourceval map_sequent : (Lang.F.pred -> Lang.F.pred) -> sequent -> sequent

Rewrite all root predicates in hypotheses and goal

Sourceval 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.

Sourceval 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.

Sourceval replace_by_step_list : at:int -> step list -> sequent -> sequent

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

raises Invalid_argument
if the index is out of bounds.

Sourceval 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

Sourceval introduction : sequent -> sequent option

Performs existential, universal and hypotheses introductions

Sourceval introduction_eq : sequent -> sequent

Same as introduction but returns the same sequent is None

Sourceval lemma : loc:Frama_c_kernel.Cil_types.location -> Lang.F.pred -> sequent

Performs existential, universal and hypotheses introductions

Sourceval head : step -> Lang.F.pred

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

Sourceval have : step -> Lang.F.pred

Predicate for Have and such, True for any other

Sourceval pred_cond : condition -> Lang.F.pred

Sourceval condition : sequence -> Lang.F.pred

With free variables kept.

Sourceval property : sequent -> Lang.F.pred

With free variables kept.

Sourceval 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.

Bundle are constructed in backward order with respect to program control-flow, as driven by the wp calculus.

Sourcetype bundle

Source

type 'a attributed =
  ?descr:string ->
  ?stmt:Frama_c_kernel.Cil_types.stmt ->
  ?deps:Frama_c_kernel.Property.t list ->
  ?warn:Warning.Set.t ->
  'a

Sourceval nil : bundle

Same as empty

Sourceval occurs : Lang.F.var -> bundle -> bool

Sourceval intersect : Lang.F.pred -> bundle -> bool

Variables of predicate and the bundle intersects

Sourceval merge : bundle list -> bundle

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.

Source

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.

Sourceval domain : Lang.F.pred list -> bundle -> bundle

Assumes a list of predicates in a Type section on top of the bundle.

Sourceval intros : Lang.F.pred list -> bundle -> bundle

Assumes a list of predicates in a Have section on top of the bundle.

Source

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.

Source

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.

Sourceval branch : (Lang.F.pred -> bundle -> bundle -> bundle) attributed

Construct a branch bundle, with merging of all common parts.

Sourceval either : (bundle list -> bundle) attributed

Construct a disjunction bundle, with merging of all common parts.

Sourceval extract : bundle -> Lang.F.pred list

Computes a formulae equivalent to the bundle. For debugging purpose only.

Sourceval bundle : bundle -> sequence

Closes the bundle and promote it into a well-formed sequence.

Simplifiers

Sourceval clean : sequent -> sequent

Sourceval filter : sequent -> sequent

Sourceval parasite : sequent -> sequent

Sourceval init_filter : sequent -> sequent

Source

val simplify : 
  ?solvers:Lang.simplifier list ->
  ?intros:int ->
  sequent ->
  sequent

Sourceval pruning : ?solvers:Lang.simplifier list -> sequent -> sequent

On This Page

Predicate Introduction
Sequent
Transformations
Bundles
Simplifiers

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/Conditions/index.html

Module Wp.ConditionsSource

Predicate Introduction

Sequent

Transformations

Bundles

Simplifiers

Module `Wp.Conditions`Source