Whiley / WhileyCompiler

The Whiley Compiler (WyC)
http://whiley.org
Apache License 2.0
219 stars 36 forks source link

QuickCheck Counterexample Messages #1045

Closed DavePearce closed 3 years ago

DavePearce commented 3 years ago

The following:

method f(&int x, &int y):
    assert *x != *y

Generates the following output:

Check configuration has ints (0..1), array lengths (max 1), type depths (max 3), sampling (1, limits 1000..10000000)  [0ms]
Failed method main::f(&int,&int)->void (36.0/36.0=100.0%, 2ms) ...................... [4ms]
================================================================================
./src/main.whiley:2: assertion failed
--> main::f(null,null)
    assert *x != *y
           ^^^^^^^^
Stack Trace:
--> main::f(null,null)
Internal failure: Index: 0, Size: 0
java.lang.IndexOutOfBoundsException: Index: 0, Size: 0
        at java.util.ArrayList.rangeCheck(ArrayList.java:657)
        at java.util.ArrayList.get(ArrayList.java:433)
        at wybs.util.AbstractSyntacticHeap.getSyntacticItem(AbstractSyntacticHeap.java:72)
        at wybs.util.AbstractSyntacticHeap.getRootItem(AbstractSyntacticHeap.java:62)
        at wybs.util.AbstractSyntacticHeap.findAll(AbstractSyntacticHeap.java:175)
        at wycli.commands.Build.extractSyntacticMarkers(Build.java:205)
        at wyc.cmd.QuickCheck.printSyntacticMarkers(QuickCheck.java:344)
        at wyc.cmd.QuickCheck.execute(QuickCheck.java:320)
        at wycli.util.AbstractWorkspace$1$1.execute(AbstractWorkspace.java:122)
        at wycli.WyMain.main(WyMain.java:162)
DavePearce commented 3 years ago

This stems from the following in ConcreteSemantics.Reference.toValue():

// FIXME: need to implement this
return new Value.Null();

The problem is that Value is defined in AbstractCompilationUnit but there is no instance for representing references (unfortunately).