Index of modules

Registered Strategies It is always safe to apply strategies to any goal.

Generic WP calculus

Floating Arithmetic Model

abstract type of a cfg

Integer Arithmetic Model

Normalized C-labels

None means equal to zero/null

Sequent

Current Loc

String Literal

C-Types

Int-As-Booleans

Unique

Memoized loading of drivers according to current WP options.

Returns an property identifier for the precondition.

set of edges

"Var,Typed,Nat,Real" memory model.

Sequent Cleaning

Term Footprints

projectified, depend on the model, not serialized

projectified, depend on the model, not serialized

request-for-update event

Edit enabled provers

Requires filter prover.

projectified, depend on the model, not serialized

projectified, depend on the model, not serialized

Datatype for the keys of the hashtbl.

Datatype for the keys of the map.

Logic Language based on Qed

bind sigma defs xs select definitions in defs targeting variables xs.

integer

Definitions

Debug

Trims the original name

Build a datatype of the hashtbl according to the datatype of values in the hashtbl.

Build a datatype of the map according to the datatype of values in the map.

unique w.r.t equal

This is what is really needed to propagate something through the CFG.

describe the content of literal strings

Memory Values

Model Registration

push the Tat down to the 'data' operations.

Passive Forms

current state

All-in-one printers

Lang Pretty-Printer

Proof Script Database

Interactive Proof Engine

With number of pending goals

Play provers with valid result (default: true)

never fails

None if the po is trivial

Variable accesses from C code and code annotations

Paths

Do on_server_stop save why3 session

Term & Predicate Introspection

get_time T t returns k such that T[k-1] <= t <= T[k], T is extended with T[-1]=0 and T[N]=+oo.

Elementary regions

Pruning strategy ; selects most occurring literals to split cases.

projectified, independent from the model, not serialized

projectified, independent from the model, not serialized

projectified, independent from the model, not serialized

projectified, independent from the model, not serialized

Term & Predicate Selection

Built-in Array Tactical (auto-registered)

Built-in Choice, Absurd & Contrapose Tactical (auto-registered)

Built-in Compound Tactical (auto-registered)

Built-in Cut Tactical (auto-registered)

Built-in Filtering Tactic (auto-registered)

Built-in Havoc Tactical (auto-registered)

Built-in Instance Tactical (auto-registered)

Self registered 'Lemma' Tactical

Built-in Normal Form Tactical (auto-registered)

Built-in Range Tactical (auto-registered)

Built-in Range Tactical (auto-registered)

Built-in Split Tactical (auto-registered)

Built-in Unfold Tactical (auto-registered)

Tactical

Proof Obligations

Verification Condition Status

VList Theory Builtins

Logical Sets

Contextual Errors

returns the list of XML elements from the given file.

C-Types

Every access to annotations have to go through here, so this is the place where we decide what the computation is allowed to use.

Beside the property identification, it can be found in different contexts depending on which part of the computation is involved.

Returns true is call pre-conditions have been already generated by RTE.

Export Statistics.

This file provide all the functions to build a strategy that can then be used by the main generic calculus.

Term manipulation for Tacticals

To be raised a feature of C/ACSL cannot be supported by a memory model or is not implemented, or ...

Goal Selection

Proof Obligations

Indexed API