chc.proof package

Proof obligations and their proofs.

There are two types of proof obligations:

primary proof obligations (ppo’s)
supporting proof obligations (spo’s)

All proof obligations are expressed as assertions over program variables using a set of custom predicates.

Primary proof obligations are generated on the source for all constructs that can possibly result in undefined behavior. An example is:

*p = 0;

would generate the primary proof obligation

not-null(p)

Primary proof obligations are generated up front and the set of primary proof obligations remains fixed after that.

Supporting proof obligations are generated in support of assumptions generated (or added by the user) to discharge primary proof obligations (or other supporting proof obligations). Consider for example:

f(int *p){ *p = 0; }

The only way (without changing the code) to discharge the not-null(p) proof obligation is to assume that the parameter p is not null. Thus this assumption is (automatically) generated on api of the function f. This, in turn, results in supporting proof obligations being generated for each call site, e.g., the call

f(q);

will cause the supporting proof obligation:

not-null(q)

to be (automatically) generated.

The set of supporting proof obligations grows over the course of the analysis as new assumptions are introduced, new supporting proof obligations to justify these assumptions may have to be generated, which in turn need to be discharged themselves, providing thus a bottom-up context-sensitivity.

`chc.proof.AssumptionType`	External assumption on a function.
`chc.proof.CFilePredicateDictionary`	Dictionary for proof obligation predicates.
`chc.proof.CFilePredicateRecord`	Object representation of OCaml po_predicate_t.
`chc.proof.CFunPODictionary`	Dictionary of proof obligation types at function level.
`chc.proof.CFunPODictionaryRecord`	Base class for objects in the function-level proof obligation dictionary.
`chc.proof.CFunctionCallsiteSPO`	Supporting proof obligation for a call site.
`chc.proof.CFunctionCallsiteSPOs`	Supporting proof obligations related to a single call site.
`chc.proof.CFunctionLocalSPO`	Support proof obligation for a local assumption made.
`chc.proof.CFunctionPO`	Super class of all (primary and supporting) proof obligations.
`chc.proof.CFunctionPPO`	Primary proof obligation.
`chc.proof.CFunctionPPOs`	The collection of all primary proof obligations in a function.
`chc.proof.CFunctionProofs`	Main access point for a function's primary and supporting proof obligations.
`chc.proof.CFunctionReturnsiteSPO`	Supporting proof obligation for a return site.
`chc.proof.CFunctionReturnsiteSPOs`	All supporting proof obligations associated with a single return site.
`chc.proof.CFunctionSPOs`	Container for all supporting proof obligations in a function.
`chc.proof.CPOPredicate`	Proof obligation predicate.
`chc.proof.CProofDependencies`	Dependencies of proof on assumptions and invariants.
`chc.proof.CProofDiagnostic`	Diagnostic messages related to an open proof obligation.
`chc.proof.PPOType`	Primary proof obligation as generated.
`chc.proof.SPOType`	Supporting proof obligation as generated to provide evidence for assumptions.

chc.proof package

Submodules