Add Existence Checks to Classes & Methods in External Refinements

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

@@ -0,0 +1,8 @@
+package testSuite;
+
+import liquidjava.specification.ExternalRefinementsFor;
+
+@ExternalRefinementsFor("non.existent.Class")
+public interface ErrorExtRefNonExistentClass {
+    public void NonExistentClass(); 
+}

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

@@ -0,0 +1,16 @@
+package testSuite;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.RefinementPredicate;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+public interface ErrorExtRefNonExistentMethod<E> {
+
+    @RefinementPredicate("int size(ArrayList l)")
+    @StateRefinement(to = "size(this) == 0")
+    public void ArrayList();
+
+    @StateRefinement(to = "size(this) == (size(old(this)) + 1)")
+    public void adddd(E e);
+}

liquidjava-example/src/main/java/testSuite/math/correctInvocation/MathRefinements.java

@@ -57,9 +57,6 @@ public interface MathRefinements {
     @Refinement("(a > b)? (_ == b):(_ == a)")
     public int min(int a, int b);
 
-    @Refinement(" _ > 0.0 && _ < 1.0")
-    public long random(long a, long b);
-
     @Refinement("((sig > 0)?(_ > 0):(_ < 0)) && (( _ == arg)||(_ == -arg))")
     public float copySign(float arg, float sig);
 }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java

@@ -18,6 +18,8 @@
 import spoon.reflect.declaration.CtField;
 import spoon.reflect.declaration.CtInterface;
 import spoon.reflect.declaration.CtMethod;
+import spoon.reflect.declaration.CtType;
+import spoon.reflect.declaration.CtTypeParameter;
 import spoon.reflect.factory.Factory;
 import spoon.reflect.reference.CtTypeReference;
 
@@ -42,6 +44,10 @@ public <T> void visitCtInterface(CtInterface<T> intrface) {
         Optional<String> externalRefinements = getExternalRefinement(intrface);
         if (externalRefinements.isPresent()) {
             this.prefix = externalRefinements.get();
+            if (!classExists(prefix)) {
+                ErrorHandler.printCostumeError(intrface, "Could not find class '" + prefix + "'", errorEmitter);
+                return;
+            }
             try {
                 getRefinementFromAnnotation(intrface);
             } catch (ParsingException e) {
@@ -72,6 +78,11 @@ public <R> void visitCtMethod(CtMethod<R> method) {
         if (errorEmitter.foundError())
             return;
 
+        if (!methodExists(method)) {
+            ErrorHandler.printCostumeError(method,
+                    "Could not find method '" + method.getSignature() + "' in class '" + prefix + "'", errorEmitter);
+            return;
+        }
         MethodsFunctionsChecker mfc = new MethodsFunctionsChecker(this);
         try {
             mfc.getMethodRefinements(method, prefix);
@@ -123,4 +134,23 @@ protected String getQualifiedClassName(CtElement elem) {
     protected String getSimpleClassName(CtElement elem) {
         return Utils.getSimpleName(prefix);
     }
+
+    private boolean classExists(String className) {
+        return factory.Type().createReference(className).getTypeDeclaration() != null;
+    }
+
+    private boolean methodExists(CtMethod<?> method) {
+        CtType<?> targetType = factory.Type().createReference(prefix).getTypeDeclaration();
+
+        // find a method with matching name and parameter count
+        boolean methodFound = targetType.getMethods().stream()
+                .anyMatch(m -> m.getSimpleName().equals(method.getSimpleName())
+                        && m.getParameters().size() == method.getParameters().size());
+
+        if (!methodFound) {
+            // check if constructor method
+            return method.getSimpleName().equals(targetType.getSimpleName());
+        }
+        return true;
+    }
 }