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

NegativeArraySizeException in CoerciveSubtypeOperator #85

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

(This may be related to #84)

function f(int|null x, int|null y) -> (int r)
ensures r == 0 || r == y:
    //
    x = y
    //
    if x is int && x >= 0:
        return x
    else:
        return 0

public export method test():
    assume f(-1,-1)   == 0
    assume f(0,-1)    == 0
    assume f(1,-1)    == 0
    assume f(2,-1)    == 0
    assume f(null,-1) == 0

    assume f(-1,0)   == 0
    assume f(0,0)    == 0
    assume f(1,0)    == 0
    assume f(2,0)    == 0
    assume f(null,0) == 0

    assume f(-1,1)   == 1
    assume f(0,1)    == 1
    assume f(1,1)    == 1
    assume f(2,1)    == 1
    assume f(null,1) == 1

This leads to a NegativeArraySizeException which looks like some kind of integer overflow.

DavePearce commented 7 years ago

UPDATE This fails only when called from WyC. Perhaps related to #88?

UPDATE a bunch of other tests are failing with this. Like, Byte_Valid_2.whiley and Byte_Valid_3.whiley.