Check Expected Errors in Tests

README.md

@@ -78,8 +78,6 @@ To run LiquidJava, use the Maven command below, replacing `/path/to/your/project
 ```bash
 mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLineLauncher" -Dexec.args="/path/to/your/project"
 ```
-*Warning: Any change to LiquidJava requires rebuilding the jar.*
-
 
 If you're on Linux/macOS, you can use the `liquidjava` script (from the repository root) to simplify the process.
 
@@ -105,10 +103,14 @@ The starter test file is `TestExamples.java`, which runs the test suite under th
 
 The test suite considers test cases:
 1. Files that start with `Correct` or `Error` (e.g., `CorrectRecursion.java`)
-2. Packages or folders that contain the word `correct` or `error` (e.g., `arraylist_correct`)
+2. Directories that contain the word `correct` or `error` (e.g., `arraylist_correct`)
 
 Therefore, the files and folders that do not follow this pattern are ignored.
 
+For failing test cases, the expected error must be specified as follows:
+1. In singular test files, the expected error (title) should be written in the first line of the file as a comment
+2. In test directories, a `.expected` file should be included in that directory with the expected error (title)
+
 ## Project Structure
 
 * **docs**: Contains documents used for the design of the language. This folder includes a [README](./docs/design/README.md) with the link to the full artifact used in the design process. It also contains initial documents used to prepare the design of the refinements language during its evaluation

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;
             }
         }