Index of modules

Generic WP calculus

Floatting Arithmetic Model

abstract type of a cfg

Integer Arithmetic Model

Normalized C-labels

None means equal to zero/null

Bundles

Current Loc

String Literal

C-Types

Int-As-Boolans

Unique

Memoized loading of drivers according to current WP options.

Returns an property identifier for the precondition.

set of edges

projectified, depend on the model, not serialized

Edit enabled provers

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.

Memory Values

Model Registration

push the Tat down to the 'data' operations.

Passive Forms

Proof Script Database

Different instance of why3ide can't be run simultanely

never fails

None if the po is trivial

Variable accesses from C code and code annotations

Paths

Do on_server_stop save why3 session

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.

Pruning strategy ; selects most occuring literals to split cases.

projectified, independent from the model, not serialized

projectified, independent from the model, not serialized

Verification Conditions Database

Usage Variable Analysis

Usage Variable Analysis

This analysis performs a classification of the variables of the input program.

Logical Sets

Contextual Errors

From the original file we kept only the reading of a session.

returns the list of XML elements from the given file.

Weakest preconditions.

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.

Export Statistics.

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

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