Add Tests

rcosta358 · rcosta358 · commit c2ae323ac476 · 2026-02-07T22:04:49.000Z
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectNullChecks.java b/liquidjava-example/src/main/java/testSuite/CorrectNullChecks.java
@@ -0,0 +1,123 @@
+package testSuite;
+
+import java.util.ArrayList;
+import java.util.Date;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class CorrectNullChecks {
+
+    void testNullInteger() {
+        Integer i = null;
+
+        @Refinement("_ == null")
+        Integer i1 = i;
+
+        i = 123;
+
+        @Refinement("_ != null")
+        Integer i2 = i;
+    }
+
+    void testNullString() {
+        String s = null;
+
+        @Refinement("_ == null")
+        String s1 = s;
+
+        s = "hello";
+
+        @Refinement("_ != null")
+        String s2 = s;
+    }
+
+    void testNulls() {
+        @Refinement("_ == null")
+        String s = null;
+
+        @Refinement("_ == null")
+        Integer i = null;
+
+        @Refinement("_ == null")
+        Boolean b = null;
+
+        @Refinement("_ == null")
+        Double d = null;
+
+        @Refinement("_ == null")
+        Long l = null;
+
+        @Refinement("_ == null")
+        Float f = null;
+
+        @Refinement("_ == null")
+        Date dt = null;
+
+        @Refinement("_ == null")
+        ArrayList<String> lst = null;        
+    }
+
+    void testNonNulls() {
+        @Refinement("_ != null")
+        String s = "hello";
+
+        @Refinement("_ != null")
+        Integer i = 123;
+
+        @Refinement("_ != null")
+        Boolean b = true;
+
+        @Refinement("_ != null")
+        Double d = 1.0;
+
+        @Refinement("_ != null")
+        Long l = 2L;
+
+        @Refinement("_ != null")
+        Float f = 1.0f;
+
+        @Refinement("_ != null")
+        Date dt = new Date();
+
+        @Refinement("_ != null")
+        ArrayList<String> lst = new ArrayList<>();
+    }
+
+    void testNullChecksInMethods() {
+        @Refinement("_ != null")
+        String x = returnNotNullIf(null);
+
+        @Refinement("_ != null")
+        String y = returnNotNullTernary(null);
+
+        @Refinement("_ != null")
+        String z = returnNotNullParam("not null");
+
+        @Refinement("_ == null")
+        String w = returnNull();
+    }
+
+    @Refinement("_ != null")
+    String returnNotNullIf(String s) {
+        if (s == null)
+            s = "default";
+    
+        return s;
+    }
+
+    @Refinement("_ != null")
+    String returnNotNullTernary(String s) {
+        return s != null ? s : "default";
+    }
+
+    @Refinement("_ != null")
+    String returnNotNullParam(@Refinement("_ != null") String s) {
+        return s;
+    }
+
+    @Refinement("_ == null")
+    String returnNull() {
+        return null;
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java
@@ -3,6 +3,7 @@
 
 import liquidjava.specification.Refinement;
 
+@SuppressWarnings("unused")
 public class ErrorAliasNotFound {
 
     public static void main(String[] args) {
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java
@@ -0,0 +1,12 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorBoxedBoolean {
+    public static void main(String[] args) {
+        @Refinement("_ == true")
+        Boolean b = false;
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java
@@ -0,0 +1,12 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorBoxedDouble {
+    public static void main(String[] args) {
+        @Refinement("_ > 0")
+        Double d = -1.0;
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java
@@ -0,0 +1,12 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorBoxedInteger {
+    public static void main(String[] args) {
+        @Refinement("_ > 0")
+        Integer j = -1;
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java
@@ -3,6 +3,7 @@
 
 import liquidjava.specification.Refinement;
 
+@SuppressWarnings("unused")
 public class ErrorGhostNotFound {
 
     public void test() {
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java
@@ -3,6 +3,7 @@
 
 import liquidjava.specification.Refinement;
 
+@SuppressWarnings("unused")
 public class ErrorLongUsagePredicates1 {
     void testUUID(){
         @Refinement("((v/4096) % 16) == 2")
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java
@@ -3,6 +3,7 @@
 
 import liquidjava.specification.Refinement;
 
+@SuppressWarnings("unused")
 public class ErrorLongUsagePredicates2 {
       void testLargeSubtractionWrong() {                                                                                                                    
       @Refinement("v - 9007199254740992 == 2")                                                                                                          
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java
@@ -3,6 +3,7 @@
 
 import liquidjava.specification.Refinement;
 
+@SuppressWarnings("unused")
 public class ErrorLongUsagePredicates3 {
     void testWrongSign() {                                                                                                                                
       @Refinement("v < 0")                                                                                                                              
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNonNull.java b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNonNull.java
@@ -0,0 +1,12 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorNullCheckAssignNonNull {
+    public static void main(String[] args) {
+        @Refinement("_ == null")
+        String s = "not null";
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNull.java b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNull.java
@@ -0,0 +1,12 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorNullCheckAssignNull {
+    public static void main(String[] args) {
+        @Refinement("_ != null")
+        String s = null;
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNullAfter.java b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNullAfter.java
@@ -0,0 +1,13 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorNullCheckAssignNullAfter {
+    public static void main(String[] args) {
+        @Refinement("_ != null")
+        String s = "not null";
+        s = null; // error
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNullObject.java b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNullObject.java
@@ -0,0 +1,14 @@
+// Refinement Error
+package testSuite;
+
+import java.util.Date;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorNullCheckAssignNullObject {
+    public static void main(String[] args) {
+        @Refinement("_ != null")
+        Date date = null;
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNullCheckMethod.java b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckMethod.java
@@ -0,0 +1,12 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorNullCheckMethod {
+
+    @Refinement("_ != null")
+    String returnNotNull(String s) {
+        return s; // error: s can be null
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_correct/AtomicReferenceRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_correct/AtomicReferenceRefinements.java
@@ -0,0 +1,19 @@
+package testSuite.classes.atomic_reference_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"empty", "holding"})
+@ExternalRefinementsFor("java.util.concurrent.atomic.AtomicReference")
+public interface AtomicReferenceRefinements<V> {
+
+    @StateRefinement(to="initialValue == null ? empty(this) : holding(this)")
+    public void AtomicReference(V initialValue);
+
+    @StateRefinement(from="holding(this)")
+    public V get();
+    
+    @StateRefinement(to="newValue == null ? empty(this) : holding(this)")
+    public void set(V newValue);
+}
diff --git a/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_correct/AtomicReferenceTest.java b/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_correct/AtomicReferenceTest.java
@@ -0,0 +1,15 @@
+package testSuite.classes.atomic_reference_correct;
+
+import java.util.concurrent.atomic.AtomicReference;
+
+@SuppressWarnings("unused")
+public class AtomicReferenceTest {
+    
+    public void testOk() {
+        AtomicReference<String> ref = new AtomicReference<>("hello");
+        String s = ref.get();
+
+        ref.set("world");
+        String s2 = ref.get();
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/AtomicReferenceRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/AtomicReferenceRefinements.java
@@ -0,0 +1,19 @@
+package testSuite.classes.atomic_reference_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"empty", "holding"})
+@ExternalRefinementsFor("java.util.concurrent.atomic.AtomicReference")
+public interface AtomicReferenceRefinements<V> {
+
+    @StateRefinement(to="initialValue == null ? empty(this) : holding(this)")
+    public void AtomicReference(V initialValue);
+
+    @StateRefinement(from="holding(this)")
+    public V get();
+    
+    @StateRefinement(to="newValue == null ? empty(this) : holding(this)")
+    public void set(V newValue);
+}
diff --git a/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/AtomicReferenceTest.java b/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/AtomicReferenceTest.java
@@ -0,0 +1,13 @@
+package testSuite.classes.atomic_reference_error;
+
+import java.util.concurrent.atomic.AtomicReference;
+
+@SuppressWarnings("unused")
+public class AtomicReferenceTest {
+    
+    public void testError() {
+        AtomicReference<String> ref = new AtomicReference<>(null);
+        String s = ref.get(); // error
+    }
+}
+
