From a8d1393e1798c4b178e3948c726079f2417be8a0 Mon Sep 17 00:00:00 2001 From: subha0319 Date: Sat, 8 Nov 2025 23:53:23 +0530 Subject: [PATCH 1/2] feat(tests): Check for specific error messages in test suite Implements #105. The `TestExamples.java` test suite will now read a `// @ExpectedError: "Error Title"` comment from any "Error" file and fail the test if the error title does not match. --- .../java/testSuite/ErrorSimpleAssignment.java | 1 + .../liquidjava/api/tests/TestExamples.java | 78 +++++++++++++++---- 2 files changed, 66 insertions(+), 13 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java b/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java index a00d4069..f313b486 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java @@ -1,3 +1,4 @@ +// @ExpectedError: "Type expected:(#c_0 > 2)" package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java index 7f216a32..66cbd673 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -22,27 +22,51 @@ public class TestExamples { * * @param filePath * path to the file to test + * + * @throws IOException + * if an I/O error occurs reading the test file */ @ParameterizedTest @MethodSource("fileNameSource") - public void testFile(final Path filePath) { + public void testFile(final Path filePath) throws IOException { String fileName = filePath.getFileName().toString(); + boolean isErrorFile = fileName.startsWith("Error") || fileName.contains("error"); + boolean isCorrectFile = fileName.startsWith("Correct") || fileName.contains("correct"); - // 1. Run the verifier on the file or package + // Run the verifier on the file or package ErrorEmitter errorEmitter = CommandLineLauncher.launch(filePath.toAbsolutePath().toString()); - // 2. Check if the file is correct or contains an error - if ((fileName.startsWith("Correct") && errorEmitter.foundError()) - || (fileName.contains("correct") && errorEmitter.foundError())) { - System.out.println("Error in directory: " + fileName + " --- should be correct but an error was found"); - fail(); - } - // 3. Check if the file has an error but passed verification - if ((fileName.startsWith("Error") && !errorEmitter.foundError()) - || (fileName.contains("error") && !errorEmitter.foundError())) { - System.out.println("Error in directory: " + fileName + " --- should be an error but passed verification"); - fail(); + if (isCorrectFile) { + // A "Correct" file should NOT have an error + if (errorEmitter.foundError()) { + System.out.println("Error in directory: " + fileName + " --- should be correct but an error was found"); + System.out.println("Error: " + errorEmitter.getTitleMessage() + " - " + errorEmitter.getFullMessage()); + fail(); + } + } else if (isErrorFile) { + // An "Error" file SHOULD have an error + if (!errorEmitter.foundError()) { + System.out + .println("Error in directory: " + fileName + " --- should be an error but passed verification"); + fail(); + } else { + // NEW: Check if it's the *correct* error + String expectedError = getExpectedError(filePath); + + // If an expected error is specified in the file, check it. + // We check the 'title' for a match. + if (expectedError != null) { + String actualErrorTitle = errorEmitter.getTitleMessage(); // + if (actualErrorTitle == null || !actualErrorTitle.equals(expectedError)) { + System.out.println("Error in directory: " + fileName + " --- wrong error message found."); + System.out.println(" Expected: " + expectedError); + System.out.println(" Actual: " + (actualErrorTitle != null ? actualErrorTitle : "NULL")); + fail(); + } + } + } } + // If it's neither "Correct" nor "Error", no assertions are made. } /** @@ -87,4 +111,32 @@ public void testMultiplePaths() { fail(); } } + + /** + * Reads the given file to find an expected error message specified in a comment. The comment format is: // + * + * @ExpectedError: "Error Title" + * + * @param filePath + * path to the test file + * + * @return The expected error title, or null if not specified. + * + * @throws IOException + * if an I/O error occurs + */ + private String getExpectedError(Path filePath) throws IOException { + if (Files.isDirectory(filePath)) { + // Currently, we don't support expected errors for entire directories. + return null; + } + + // Try to find the expected error comment in the first 10 lines + try (Stream lines = Files.lines(filePath).limit(10)) { + return lines.map(String::trim).filter(line -> line.startsWith("// @ExpectedError:")).findFirst() + .map(line -> line.substring(line.indexOf(":") + 1).trim()) // Get text after the colon + .map(line -> line.replace("\"", "")) // Remove quotes + .orElse(null); // No expected error specified + } + } } From 3d4bd2f9750b65749b138616d10f5d4703bd1351 Mon Sep 17 00:00:00 2001 From: subha0319 Date: Sat, 8 Nov 2025 23:53:23 +0530 Subject: [PATCH 2/2] feat(tests): Check for specific error messages in test suite Implements #105. The `TestExamples.java` test suite will now read a `// @ExpectedError: "Error Title"` comment from any "Error" file and fail the test if the error title does not match. --- .../src/main/java/testSuite/ErrorAfterIf.java | 1 + .../ErrorArithmeticBinaryOperations.java | 1 + .../java/testSuite/ErrorSimpleAssignment.java | 1 + .../liquidjava/api/tests/TestExamples.java | 78 +++++++++++++++---- 4 files changed, 68 insertions(+), 13 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java index 130434f9..c1988120 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java @@ -1,3 +1,4 @@ +// @ExpectedError: "Type expected:(#r_26 == a || #r_26 == b)" package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java index 9556fea0..5e80d4b3 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java @@ -1,3 +1,4 @@ +// @ExpectedError: "Type expected:(#z_2 > 0)" package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java b/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java index a00d4069..f313b486 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java @@ -1,3 +1,4 @@ +// @ExpectedError: "Type expected:(#c_0 > 2)" package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java index 7f216a32..66cbd673 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -22,27 +22,51 @@ public class TestExamples { * * @param filePath * path to the file to test + * + * @throws IOException + * if an I/O error occurs reading the test file */ @ParameterizedTest @MethodSource("fileNameSource") - public void testFile(final Path filePath) { + public void testFile(final Path filePath) throws IOException { String fileName = filePath.getFileName().toString(); + boolean isErrorFile = fileName.startsWith("Error") || fileName.contains("error"); + boolean isCorrectFile = fileName.startsWith("Correct") || fileName.contains("correct"); - // 1. Run the verifier on the file or package + // Run the verifier on the file or package ErrorEmitter errorEmitter = CommandLineLauncher.launch(filePath.toAbsolutePath().toString()); - // 2. Check if the file is correct or contains an error - if ((fileName.startsWith("Correct") && errorEmitter.foundError()) - || (fileName.contains("correct") && errorEmitter.foundError())) { - System.out.println("Error in directory: " + fileName + " --- should be correct but an error was found"); - fail(); - } - // 3. Check if the file has an error but passed verification - if ((fileName.startsWith("Error") && !errorEmitter.foundError()) - || (fileName.contains("error") && !errorEmitter.foundError())) { - System.out.println("Error in directory: " + fileName + " --- should be an error but passed verification"); - fail(); + if (isCorrectFile) { + // A "Correct" file should NOT have an error + if (errorEmitter.foundError()) { + System.out.println("Error in directory: " + fileName + " --- should be correct but an error was found"); + System.out.println("Error: " + errorEmitter.getTitleMessage() + " - " + errorEmitter.getFullMessage()); + fail(); + } + } else if (isErrorFile) { + // An "Error" file SHOULD have an error + if (!errorEmitter.foundError()) { + System.out + .println("Error in directory: " + fileName + " --- should be an error but passed verification"); + fail(); + } else { + // NEW: Check if it's the *correct* error + String expectedError = getExpectedError(filePath); + + // If an expected error is specified in the file, check it. + // We check the 'title' for a match. + if (expectedError != null) { + String actualErrorTitle = errorEmitter.getTitleMessage(); // + if (actualErrorTitle == null || !actualErrorTitle.equals(expectedError)) { + System.out.println("Error in directory: " + fileName + " --- wrong error message found."); + System.out.println(" Expected: " + expectedError); + System.out.println(" Actual: " + (actualErrorTitle != null ? actualErrorTitle : "NULL")); + fail(); + } + } + } } + // If it's neither "Correct" nor "Error", no assertions are made. } /** @@ -87,4 +111,32 @@ public void testMultiplePaths() { fail(); } } + + /** + * Reads the given file to find an expected error message specified in a comment. The comment format is: // + * + * @ExpectedError: "Error Title" + * + * @param filePath + * path to the test file + * + * @return The expected error title, or null if not specified. + * + * @throws IOException + * if an I/O error occurs + */ + private String getExpectedError(Path filePath) throws IOException { + if (Files.isDirectory(filePath)) { + // Currently, we don't support expected errors for entire directories. + return null; + } + + // Try to find the expected error comment in the first 10 lines + try (Stream lines = Files.lines(filePath).limit(10)) { + return lines.map(String::trim).filter(line -> line.startsWith("// @ExpectedError:")).findFirst() + .map(line -> line.substring(line.indexOf(":") + 1).trim()) // Get text after the colon + .map(line -> line.replace("\"", "")) // Remove quotes + .orElse(null); // No expected error specified + } + } }