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 External Function Call #120

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

The following is failing:

import tmp.Byte

assert:
   forall(Byte.nat i):
      Byte.f(i) == false

The error is as follows

Exception in thread "main" java.lang.RuntimeException: java.lang.IllegalArgumentException: Cannot allocate item since a descendent is already allocated to another heap
    at wyal.commands.VerifyCommand.compile(VerifyCommand.java:236)
    at wyal.commands.VerifyCommand.execute(VerifyCommand.java:188)
    at wyal.commands.VerifyCommand.execute(VerifyCommand.java:38)
    at wycc.WyMain.main(WyMain.java:75)
Caused by: java.lang.IllegalArgumentException: Cannot allocate item since a descendent is already allocated to another heap
    at wyal.heap.AbstractSyntacticHeap.internalAllocate(AbstractSyntacticHeap.java:74)
    at wyal.heap.AbstractSyntacticHeap.internalAllocate(AbstractSyntacticHeap.java:82)
    at wyal.heap.AbstractSyntacticHeap.internalAllocate(AbstractSyntacticHeap.java:82)
    at wyal.heap.AbstractSyntacticHeap.allocate(AbstractSyntacticHeap.java:66)
    at wyal.util.TypeChecker.checkInvocation(TypeChecker.java:610)
        ...

The problem is presumably that the invocation expression Byte.f() is already allocated to a different heap (namely in the file tmp/Byte.wyal).