AssignsCompleteness | This module is used to check the assigns specification of a given function so that if it is not precise enough to enable precise memory models hypotheses computation, the assigns specification is considered incomplete. |
Auto | |
Cache | |
CfgAnnot | |
CfgCalculus | |
CfgCompiler | |
CfgDump | |
CfgGenerator | |
CfgInfos | |
CfgInit | |
CfgWP | |
Cfloat | Floating Arithmetic Model |
Cint | Integer Arithmetic Model |
Clabels | Normalized C-labels |
Cleaning | |
Cmath | Math Operators |
CodeSemantics | |
Conditions | |
Context | Current Loc |
Cstring | |
Ctypes | C-Types |
Cvalues | |
Definitions | |
Driver | |
Dyncall | |
Factory | |
Filter_axioms | |
Filtering | Sequent Cleaning |
Footprint | Term Footprints |
Generator | Compute model setup from command line options. |
GuiComposer | |
GuiConfig | |
GuiGoal | |
GuiList | |
GuiNavigator | |
GuiPanel | |
GuiProof | |
GuiProver | |
GuiSequent | |
GuiSource | |
GuiTactic | |
Lang | |
Layout | Region Utilities |
Letify | |
LogicAssigns | |
LogicBuiltins | |
LogicCompiler | |
LogicSemantics | |
LogicUsage | |
Matrix | |
Mcfg | |
MemDebug | |
MemEmpty | |
MemLoader | Compound Loader |
MemMemory | |
MemRegion | |
MemTyped | |
MemVal | |
MemVar | |
MemZeroAlias | |
MemoryContext | |
Mstate | |
NormAtLabels | |
Passive | |
Pcfg | |
Pcond | |
Plang | |
ProofEngine | Interactive Proof Engine |
ProofScript | |
ProofSession | |
Prover | |
ProverScript | |
ProverSearch | |
ProverTask | |
ProverWhy3 | |
RefUsage | |
Region | |
RegionAccess | |
RegionAnalysis | Memoized and Projectified Region Analyzis for the given Function. |
RegionAnnot | |
RegionDump | |
Register | |
Repr | Term & Predicate Introspection |
Rformat | |
Script | |
Sigma | |
Sigs | Common Types and Signatures |
Splitter | |
StmtSemantics | |
Strategy | Term & Predicate Selection |
TacArray | Built-in Array Tactical (auto-registered) |
TacBitrange | Built-in Bit Range Tactical (auto-registered) |
TacBittest | Built-in Bit-Test Range Tactical (auto-registered) |
TacBitwised | Built-in Bitwised-Eq Tactical (auto-registered) |
TacChoice | Built-in Choice, Absurd & Contrapose Tactical (auto-registered) |
TacClear | Built-in Range Tactical (auto-registered) |
TacCompound | Built-in Compound Tactical (auto-registered) |
TacCongruence | Built-in Tactical for Product & Division Comparison (auto-registered) |
TacCut | Built-in Cut Tactical (auto-registered) |
TacFilter | Built-in Filtering Tactic (auto-registered) |
TacHavoc | Built-in Havoc Tactical (auto-registered) |
TacInduction | Built-in Range Tactical (auto-registered) |
TacInstance | Built-in Instance Tactical (auto-registered) |
TacLemma | Self registered 'Lemma' Tactical |
TacModMask | |
TacNormalForm | Built-in Normal Form Tactical (auto-registered) |
TacOverflow | Auto registered overflow tactic |
TacRange | Built-in Range Tactical (auto-registered) |
TacRewrite | Built-in Range Tactical (auto-registered) |
TacSequence | Built-in Sequence Tactical (auto-registered) |
TacShift | Built-in Shift Tactical (auto-registered) |
TacSplit | Built-in Split Tactical (auto-registered) |
TacUnfold | Built-in Unfold Tactical (auto-registered) |
Tactical | Tactical |
VC | |
VCS | Verification Condition Status |
Vlist | |
Vset | |
Warning | Contextual Errors |
Why3Provers | |
Wp | WP Public API |
WpContext | Model Registration |
WpPropId | |
WpRTE | Invoke RTE to generate missing annotations for the given function and model. |
WpReached | Reachability for Smoke Tests |
WpReport | Export Statistics. |
WpTac | |
WpTarget | This module computes the set of kernel functions that are considered by the command line options transmitted to WP. |
Wp_error | |
Wp_parameters | |
Wpo | |
Wprop | Indexed API |