Support Reference Lifetimes

Whiley / WhileyTheoremProver

The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.

Apache License 2.0

8 stars 2 forks source link

Support Reference Lifetimes #102

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

Unfortunately, WyTP does not currently support reference lifetimes. Since (for whatever reason) function overloading takes into account reference lifetimes, it follows that any test cases which depend on this are doomed.

DavePearce commented 7 years ago

UPDATED WyalFile.Type.Reference with getLifetime() and WyalFile.Type.Method with getContextLifetimes() and getLifetimeParameters(). However, the following items remains:

[x] Update WyalFileParser to parse lifetime arguments on types (e.g. &this:int, etc).
[ ] Update WyalFileParser to support in operator for comparing lifetimes.
[ ] Update CoerciveSubtypeOperator to properly handle lifetime arguments.