Keep the values expected depends on in the counterexample

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleAliasedArgument.java

@@ -0,0 +1,15 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleAliasedArgument {
+
+    static void connect(@Refinement("_ >= 0") int timeout) {}
+
+    static void probe(int port, int configured) {
+        if (port < 0 || port > 65535)
+            return;
+        int timeout = configured;
+        connect(timeout); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleArrayArgument.java

@@ -0,0 +1,14 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleArrayArgument {
+
+    static void get(int[] a, @Refinement("_ >= 0 && _ < length(a)") int i) {}
+
+    static void probe(int port, int[] a) {
+        if (port < 0)
+            return;
+        get(a, 3); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleArrayIndex.java

@@ -0,0 +1,15 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleArrayIndex {
+
+    static void get(int[] a, @Refinement("_ >= 0 && _ < length(a)") int i) {}
+
+    static void probe(int port, int k) {
+        if (port < 0)
+            return;
+        int[] a = new int[4];
+        get(a, k); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleBranchArgument.java

@@ -0,0 +1,17 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleBranchArgument {
+
+    static void connect(@Refinement("_ >= 0") int timeout) {}
+
+    static void probe(boolean secure, int port, int timeout) {
+        if (secure) {
+            connect(0);
+        } else {
+            if (port > 1024)
+                connect(timeout); // Expect: Refinement Error
+        }
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleCallArgument.java

@@ -0,0 +1,18 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleCallArgument {
+
+    static void connect(@Refinement("_ >= 0") int timeout) {}
+
+    static int read(int key) {
+        return key;
+    }
+
+    static void probe(int port, int key) {
+        if (port < 0)
+            return;
+        connect(read(key) - 1); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleCombinedGuard.java

@@ -0,0 +1,14 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleCombinedGuard {
+
+    static void connect(@Refinement("_ >= 0") int timeout) {}
+
+    static void probe(int port, int retries, int backoff, int window, int timeout) {
+        if (port < 0 || port > 65535 || retries < 0 || backoff < 0 || window < 1 || timeout > 60000)
+            return;
+        connect(timeout); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleFieldArgument.java

@@ -0,0 +1,16 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleFieldArgument {
+
+    int timeout;
+
+    static void connect(@Refinement("_ >= 0") int timeout) {}
+
+    void probe(int port) {
+        if (port < 0)
+            return;
+        connect(this.timeout); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleGhostArgument.java

@@ -0,0 +1,22 @@
+package testSuite;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("int size")
+class CounterexampleBag {
+    @StateRefinement(to = "size(this) == 0")
+    CounterexampleBag() {}
+}
+
+public class ErrorCounterexampleGhostArgument {
+
+    static void take(@Refinement("size(b) > 0") CounterexampleBag b) {}
+
+    static void probe(int port, CounterexampleBag bag) {
+        if (port < 0)
+            return;
+        take(bag); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleGuardRelatesArguments.java

@@ -0,0 +1,14 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleGuardRelatesArguments {
+
+    static void connect(@Refinement("_ >= 0") int timeout) {}
+
+    static void probe(int port, int retries, int timeout) {
+        if (port < 0 || retries > timeout + 5)
+            return;
+        connect(timeout); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleGuardedArgument.java

@@ -0,0 +1,16 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleGuardedArgument {
+
+    static void connect(@Refinement("_ >= 0") int timeout) {}
+
+    static void probe(int port, int timeout) {
+        if (timeout > 100)
+            return;
+        if (port < 0)
+            return;
+        connect(timeout); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownAliasedArgument.java

@@ -0,0 +1,15 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleKnownAliasedArgument {
+
+    static void take(@Refinement("_ > 1") int value) {}
+
+    static void probe(int port) {
+        int base = 0;
+        int value = base;
+        if (port > 0)
+            take(value); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownArgument.java

@@ -0,0 +1,14 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleKnownArgument {
+
+    static void window(@Refinement("_ > size") int capacity, int size) {}
+
+    static void probe(int port, int capacity) {
+        if (port < 0)
+            return;
+        window(capacity, 10); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownEnum.java

@@ -0,0 +1,17 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleKnownEnum {
+
+    enum Format {
+        JPG, PNG
+    }
+
+    static void onlyPng(@Refinement("f == Format.PNG") Format f) {}
+
+    static void probe(Format format) {
+        if (format == Format.JPG)
+            onlyPng(format); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownGhost.java

@@ -0,0 +1,27 @@
+package testSuite;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("int size")
+class CounterexampleStack {
+    @StateRefinement(to = "size(this) == 0")
+    CounterexampleStack() {}
+
+    @StateRefinement(to = "size(this) == size(old(this)) + 1")
+    void push() {}
+}
+
+public class ErrorCounterexampleKnownGhost {
+
+    static void take(@Refinement("size(s) > 1") CounterexampleStack s) {}
+
+    static void probe(int port) {
+        CounterexampleStack s = new CounterexampleStack();
+        if (port < 0)
+            return;
+        s.push();
+        take(s); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownGuardedArgument.java

@@ -0,0 +1,14 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleKnownGuardedArgument {
+
+    static void take(@Refinement("_ > 1") int value) {}
+
+    static void probe(int port) {
+        int value = 0;
+        if (port > 0)
+            take(value); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownTwiceGuardedArgument.java

@@ -0,0 +1,15 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleKnownTwiceGuardedArgument {
+
+    static void take(@Refinement("_ > 1") int value) {}
+
+    static void probe(int port, int retries) {
+        int value = 0;
+        if (port > 0)
+            if (retries < 3)
+                take(value); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleLinkedPathCondition.java

@@ -0,0 +1,16 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleLinkedPathCondition {
+
+    static void connect(@Refinement("_ >= 0") int timeout) {}
+
+    static void probe(int port, int retries) {
+        if (retries > 3)
+            return;
+        if (port < 0)
+            return;
+        connect(port - 1); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleMixedGuard.java

@@ -0,0 +1,14 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleMixedGuard {
+
+    static void connect(@Refinement("_ >= 0") int timeout) {}
+
+    static void probe(int port, int retries, int backoff, int timeout) {
+        if (port < 0 || (retries > 3 && backoff > 10) || timeout > 60000)
+            return;
+        connect(timeout); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleNothingKnown.java

@@ -0,0 +1,12 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleNothingKnown {
+
+    static void sleep(@Refinement("_ >= 0") int millis) {}
+
+    static void probe(int millis) {
+        sleep(millis); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleRefinementAlias.java

@@ -0,0 +1,16 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+import liquidjava.specification.RefinementAlias;
+
+@RefinementAlias("NonNegative(int v) { v >= 0 }")
+public class ErrorCounterexampleRefinementAlias {
+
+    static void connect(@Refinement("NonNegative(_)") int timeout) {}
+
+    static void probe(int port, int timeout) {
+        if (port < 0)
+            return;
+        connect(timeout); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleReturnConstant.java

@@ -0,0 +1,13 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleReturnConstant {
+
+    @Refinement("_ > 10")
+    static int ten(int port) {
+        if (port < 0)
+            return 0; // Expect: Refinement Error
+        return 11;
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleReturnFromPath.java

@@ -0,0 +1,13 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleReturnFromPath {
+
+    @Refinement("_ > 10")
+    static int ten(int port) {
+        if (port < 0)
+            return port + 1; // Expect: Refinement Error
+        return 11;
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleReturnPath.java

@@ -0,0 +1,13 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleReturnPath {
+
+    @Refinement("_ >= 0")
+    static int timeoutOf(int port, int configured) {
+        if (port < 0)
+            return 0;
+        return configured; // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCounterexampleSeveralArguments.java

@@ -0,0 +1,16 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorCounterexampleSeveralArguments {
+
+    static void range(@Refinement("_ >= 0") int from, @Refinement("_ >= from") int to) {}
+
+    static void probe(int port, int lo, int hi) {
+        if (port < 0)
+            return;
+        if (lo < 0)
+            return;
+        range(lo, hi); // Expect: Refinement Error
+    }
+}