search

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

TypeChecker Reports Error on Wrong Lines? #81

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

In some situations, the TypeChecker is reporting errors on the wrong line numbers when used via wy compile. This is causing a range of different problems. For example, the following generates a NullPointerException:

type OpenRecord is {int x, ...}

function f(OpenRecord r) -> int:
    if r is !{int x}:
        return r.x
    else:
        return 0

Presumably, the reason this has not been detected before is that type checking generally doesn't fail when called from wy compile.

DavePearce commented 7 years ago

UPDATE there we some bugs. But, of this is related to the fact that many Whiley elements don't have proper source attributes (e.g. NameID).