Add Tests For Conflicting State Names

Author: rcosta358

liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/Door.java

@@ -0,0 +1,11 @@
+package testSuite.classes.ambiguous_state_names_correct;
+
+import liquidjava.specification.StateSet;
+import liquidjava.specification.StateRefinement;
+
+@StateSet({"open", "closed"})
+public class Door {
+
+    @StateRefinement(to = "open(this)")
+    public Door() { }
+}

liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/Pipe.java

@@ -0,0 +1,11 @@
+package testSuite.classes.ambiguous_state_names_correct;
+
+import liquidjava.specification.StateSet;
+import liquidjava.specification.StateRefinement;
+
+@StateSet({"open", "closed"})
+public class Pipe {
+    
+    @StateRefinement(to = "open(this)")
+    public Pipe() { }
+}

liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/SimpleTest.java

@@ -0,0 +1,14 @@
+package testSuite.classes.ambiguous_state_names_correct;
+
+import liquidjava.specification.Refinement;
+
+public class SimpleTest {
+
+    public static void main(String[] args) {
+        Door d = new Door(); // contains 'open' and 'closed' states
+        Pipe p = new Pipe(); // unrelated type with the same state names
+        requiresOpen(d); // ok iff 'open' binds to Door.open otherwise it may bind to Pipe.open and fail
+    }
+
+    public static void requiresOpen(@Refinement("open(s)") Door s) { }
+}

liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SM1.java

@@ -0,0 +1,15 @@
+package testSuite.classes.conflicting_state_names_correct;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"uninitialized", "initialized"})
+public class SM1 {
+
+	@StateRefinement(to="uninitialized(this)")
+	public SM1() {}
+	
+
+	@StateRefinement(from="uninitialized(this)", to="initialized(this)")
+	public void initialize() {}
+}

liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SM2.java

@@ -0,0 +1,15 @@
+package testSuite.classes.conflicting_state_names_correct;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"uninitialized", "initialized"})
+public class SM2 {
+
+	@StateRefinement(to="uninitialized(this)")
+	public SM2() {}
+	
+
+	@StateRefinement(from="uninitialized(this)", to="initialized(this)")
+	public void initialize() {}
+}

liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SimpleTest.java

@@ -0,0 +1,11 @@
+package testSuite.classes.conflicting_state_names_correct;
+
+class SimpleTest {
+	public static void main(String[] args) {
+		// both classes contain the same state names
+		SM1 sm1 = new SM1();
+		SM2 sm2 = new SM2();
+		sm1.initialize();
+		sm2.initialize();
+	}
+}

liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java

@@ -1,6 +1,7 @@
 package liquidjava.processor;
 
 import liquidjava.rj_language.Predicate;
+import liquidjava.utils.Utils;
 import spoon.reflect.reference.CtTypeReference;
 
 /**
@@ -29,7 +30,7 @@ public void setNext(VCImplication c) {
     public String toString() {
         if (name != null && type != null) {
             String qualType = type.getQualifiedName();
-            String simpleType = qualType.contains(".") ? qualType.substring(qualType.lastIndexOf(".") + 1) : qualType;
+            String simpleType = qualType.contains(".") ? Utils.getSimpleName(qualType) : qualType;
             return String.format("%-20s %s %s", "∀" + name + ":" + simpleType + ",", refinement.toString(),
                     next != null ? " => \n" + next.toString() : "");
         } else

liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java

@@ -36,7 +36,7 @@ public class Utils {
     public static final String LONG = "long";
     public static final String FLOAT = "float";
 
-    private static final Set<String> defaultNames = Set.of("old", "length", "addToIndex", "getFromIndex");
+    private static final Set<String> DEFAULT_NAMES = Set.of("old", "length", "addToIndex", "getFromIndex");
 
     public static CtTypeReference<?> getType(String type, Factory factory) {
         // TODO complete
@@ -65,8 +65,8 @@ public static String getSimpleName(String qualifiedName) {
     }
 
     public static String qualifyName(String prefix, String name) {
-        if (defaultNames.contains(name))
-            return name;
+        if (DEFAULT_NAMES.contains(name))
+            return name; // dont qualify
         return String.format("%s.%s", prefix, name);
     }
 }