package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Proof Task and Simplifiers

Predicate Introduction

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.

Sequent

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

    See index

    *)
  2. size : int;
  3. vars : Lang.F.Vars.t;
  4. stmt : Frama_c_kernel.Cil_types.stmt option;
  5. descr : string option;
  6. deps : Frama_c_kernel.Property.t list;
  7. warn : Wp__.Warning.Set.t;
  8. condition : condition;
}
and condition =
  1. | Type of Lang.F.pred
    (*

    Type section, not constraining for filtering

    *)
  2. | Have of Lang.F.pred
    (*

    Normal assumptions section

    *)
  3. | When of Lang.F.pred
    (*

    Assumptions introduced after simplifications

    *)
  4. | Core of Lang.F.pred
    (*

    Common hypotheses gather from parallel branches

    *)
  5. | Init of Lang.F.pred
    (*

    Initializers assumptions

    *)
  6. | Branch of Lang.F.pred * sequence * sequence
    (*

    If-Then-Else

    *)
  7. | Either of sequence list
    (*

    Disjunction

    *)
  8. | State of Mstate.state
    (*

    Memory Model snapshot

    *)
and sequence

List of steps

type sequent = sequence * Lang.F.pred
val pretty : (Stdlib.Format.formatter -> sequent -> unit) Stdlib.ref
val equal : sequent -> sequent -> bool
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 sequence : step list -> sequence

Creates an If-Then-Else branch located at the provided stmt, if any.

val append : sequence -> sequence -> sequence

Conjunction

val concat : sequence list -> sequence

List conjunction

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

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

val list : sequence -> step list

Same domain than iter.

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

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

Goal is true or hypotheses contains false.

Transformations

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

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

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

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 : 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 close : sequent -> 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.

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: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

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

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 bundle : bundle -> sequence

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

Simplifiers

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

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct