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.
The following (simplified) excerpt is generated from RecursiveType_Valid_22.whiley:
assert:
forall(null|{int data} list, int item):
list is !null
list.data != item
The problem is that a NullPointerException is being generated for the record access list.data. Specifically, StdTypeInference is not able to extract a record type for list. The issues essentially boils down to the fact that this is is occurring after TypeChecker (where full flow type information is known). We need some notion of an AliasDeclaration.
BUT: on the assumption that we will move to using the new WhileyFile API then this will be resolved as there is no concept of type inference.
The following (simplified) excerpt is generated from
RecursiveType_Valid_22.whiley:The problem is that a
NullPointerExceptionis being generated for the record accesslist.data. Specifically,StdTypeInferenceis not able to extract a record type forlist. The issues essentially boils down to the fact that this is is occurring afterTypeChecker(where full flow type information is known). We need some notion of anAliasDeclaration.BUT: on the assumption that we will move to using the new
WhileyFileAPI then this will be resolved as there is no concept of type inference.