Check Expected Errors in Tests

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Not Found Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
@@ -8,7 +9,7 @@
 public class ErrorAliasArgumentSize {
 
     public static void main(String[] args) {
-        @Refinement("InRange( _, 10)")
+        @Refinement("InRange(j, 10)")
         int j = 15;
     }
 }

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Syntax Error
 package testSuite;
 
 import liquidjava.specification.RefinementAlias;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Syntax Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// State Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java

@@ -1,3 +1,4 @@
+// Error
 package testSuite.classes;
 
 import liquidjava.specification.Ghost;

liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/.expected

@@ -0,0 +1 @@
+State Refinement Error

liquidjava-example/src/main/java/testSuite/classes/email_error/.expected

@@ -0,0 +1 @@
+State Refinement Error

liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/.expected

@@ -0,0 +1 @@
+Refinement Error

liquidjava-example/src/main/java/testSuite/classes/input_reader_error/.expected

@@ -0,0 +1 @@
+State Refinement Error

liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/.expected

@@ -0,0 +1 @@
+State Refinement Error

liquidjava-example/src/main/java/testSuite/classes/iterator_error/.expected

@@ -0,0 +1 @@
+State Refinement Error

liquidjava-example/src/main/java/testSuite/classes/method_overload_error/.expected

@@ -0,0 +1 @@
+Refinement Error

liquidjava-example/src/main/java/testSuite/classes/order_gift_error/.expected

@@ -0,0 +1 @@
+State Refinement Error

liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/.expected

@@ -0,0 +1 @@
+Refinement Error

liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/.expected

@@ -0,0 +1 @@
+Refinement Error

liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/.expected

@@ -0,0 +1 @@
+State Refinement Error

liquidjava-example/src/main/java/testSuite/classes/socket_error/.expected

@@ -0,0 +1 @@
+State Refinement Error

liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/.expected

@@ -0,0 +1 @@
+State Conflict Error

liquidjava-example/src/main/java/testSuite/field_updates/ErrorFieldUpdate.java

@@ -1,3 +1,4 @@
+// State Refinement Error
 package testSuite.field_updates;
 
 import liquidjava.specification.StateRefinement;

liquidjava-example/src/main/java/testSuite/math/errorAbs/.expected

@@ -0,0 +1 @@
+Refinement Error

liquidjava-example/src/main/java/testSuite/math/errorMax/.expected

@@ -0,0 +1 @@
+Refinement Error

liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/.expected

@@ -0,0 +1 @@
+Refinement Error

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

@@ -71,16 +71,16 @@ public <R> void visitCtMethod(CtMethod<R> method) {
                 String message = String.format("Could not find constructor '%s' for '%s'", method.getSignature(),
                         prefix);
                 String[] overloads = getOverloads(targetType, method);
-                diagnostics.add(
-                        new ExternalMethodNotFoundWarning(method.getPosition(), message, method.getSignature(), prefix, overloads));
+                diagnostics.add(new ExternalMethodNotFoundWarning(method.getPosition(), message, method.getSignature(),
+                        prefix, overloads));
             }
         } else {
             if (!methodExists(targetType, method)) {
                 String message = String.format("Could not find method '%s %s' for '%s'",
                         method.getType().getSimpleName(), method.getSignature(), prefix);
                 String[] overloads = getOverloads(targetType, method);
-                diagnostics.add(
-                        new ExternalMethodNotFoundWarning(method.getPosition(), message, method.getSignature(), prefix, overloads));
+                diagnostics.add(new ExternalMethodNotFoundWarning(method.getPosition(), message, method.getSignature(),
+                        prefix, overloads));
                 return;
             }
         }