diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentClass.java b/liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentClass.java new file mode 100644 index 00000000..800ee7c0 --- /dev/null +++ b/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(); +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentMethod.java b/liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentMethod.java new file mode 100644 index 00000000..ac3db0d0 --- /dev/null +++ b/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 { + + @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); +} diff --git a/liquidjava-example/src/main/java/testSuite/math/correctInvocation/MathRefinements.java b/liquidjava-example/src/main/java/testSuite/math/correctInvocation/MathRefinements.java index 925b746e..95577d65 100644 --- a/liquidjava-example/src/main/java/testSuite/math/correctInvocation/MathRefinements.java +++ b/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); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 1be4493a..1b5543a3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/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 void visitCtInterface(CtInterface intrface) { Optional 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 void visitCtMethod(CtMethod 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; + } }