diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java index 130434f9..ea881ad5 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" 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..151d4da2 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" 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..8830cc8a 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" 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..e6fa88dc 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -7,6 +7,7 @@ import java.nio.file.Path; import java.nio.file.Paths; import java.util.stream.Stream; +import java.util.Optional; import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.ErrorEmitter; @@ -22,27 +23,53 @@ 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 + Optional expectedError = getExpectedError(filePath); + + // If an expected error is specified in the file, check it. + if (expectedError.isPresent()) { + String expected = expectedError.get(); + String actualErrorTitle = errorEmitter.getTitleMessage(); + + if (actualErrorTitle == null || !actualErrorTitle.contains(expected)) { + System.out.println("Error in directory: " + fileName + " --- wrong error message found."); + System.out.println(" Expected to contain: \"" + expected + "\""); + System.out.println(" Actual: \"" + + (actualErrorTitle != null ? actualErrorTitle : "NULL") + "\""); + fail(); + } + } + } } + // If it's neither "Correct" nor "Error", no assertions are made. } /** @@ -87,4 +114,31 @@ public void testMultiplePaths() { fail(); } } + + /** + * Reads the given file to find an expected error message specified in a comment on the first line. The comment + * format is: // @ExpectedError: "Error Title" + * + * @param filePath + * path to the test file + * + * @return An Optional containing the expected error string, or Optional.empty() if not specified or if it's a + * directory. + * + * @throws IOException + * if an I/O error occurs + */ + private Optional getExpectedError(Path filePath) throws IOException { + if (Files.isDirectory(filePath)) { + return Optional.empty(); + } + + // Try to find the expected error comment on the first line + try (Stream lines = Files.lines(filePath)) { + return lines.findFirst() // Get only the first line + .map(String::trim).filter(line -> line.startsWith("// @ExpectedError:")) + .map(line -> line.substring(line.indexOf(":") + 1).trim()) // Get text after the colon + .map(line -> line.replace("\"", "")); // Remove quotes + } + } }