Inline Expected Warnings in Tests

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

@@ -2,7 +2,7 @@
 
 import liquidjava.specification.ExternalRefinementsFor;
 
-@ExternalRefinementsFor("non.existent.Class")
+@ExternalRefinementsFor("non.existent.Class") // Warning
 public interface WarningExtRefNonExistentClass {
     public void NonExistentClass(); 
 }

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

@@ -12,5 +12,5 @@ public interface WarningExtRefNonExistentMethod<E> {
     public void ArrayList();
 
     @StateRefinement(to = "size(this) == (size(old(this)) + 1)")
-    public boolean adddd(E e);
+    public boolean adddd(E e); // Warning
 }

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

@@ -9,7 +9,7 @@
 public interface WarningExtRefWrongConstructor<E> {
 
     @StateRefinement(to = "size(this) == 0")
-    public void ArrayList(String wrongParameter);
+    public void ArrayList(String wrongParameter); // Warning
 
     @StateRefinement(to = "size(this) == (size(old(this)) + 1)")
     public boolean add(E e);

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

@@ -12,5 +12,5 @@ public interface WarningExtRefWrongParameterType<E> {
     public void ArrayList();
 
     @StateRefinement(to = "size(this) == (size(old(this)) + 1)")
-    public boolean add(int wrongParameter);
+    public boolean add(int wrongParameter); // Warning
 }

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

@@ -12,5 +12,5 @@ public interface WarningExtRefWrongRetType<E> {
     public void ArrayList();
 
     @StateRefinement(to = "size(this) == (size(old(this)) + 1)")
-    public int add(E e); // wrong return type
+    public int add(E e); // Warning
 }

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java

@@ -8,11 +8,13 @@
 import java.nio.file.Files;
 import java.nio.file.Path;
 import java.nio.file.Paths;
+import java.util.Collection;
 import java.util.List;
 import java.util.stream.Stream;
 
 import liquidjava.api.CommandLineLauncher;
 import liquidjava.diagnostics.Diagnostics;
+import liquidjava.diagnostics.LJDiagnostic;
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.utils.Pair;
 
@@ -25,11 +27,7 @@ public class TestExamples {
     Diagnostics diagnostics = Diagnostics.getInstance();
 
     /**
-     * Test the file at the given path by launching the verifier and checking for errors. The file/directory is expected
-     * to be either correct or contain an error based on its name.
-     *
-     * @param path
-     *            path to the file to test
+     * Runs the verifier and checks the expected diagnostics
      */
     @ParameterizedTest
     @MethodSource("sourcePaths")
@@ -40,6 +38,14 @@ public void testPath(final Path path) {
         // run verification
         CommandLineLauncher.launch(path.toFile().toString());
 
+        List<Pair<String, Integer>> expectedWarnings = isDirectory ? getExpectedWarningsFromDirectory(path)
+                : getExpectedWarningsFromFile(path);
+
+        if (shouldWarn(pathName)) {
+            checkExpectedDiagnostics(pathName, diagnostics.getWarnings(), expectedWarnings,
+                    diagnostics.getWarningOutput());
+        }
+
         // verification should pass, check if any errors were found
         if (shouldPass(pathName) && diagnostics.foundError()) {
             System.out.println("Error in: " + pathName + " --- should pass but an error was found. \n"
@@ -56,64 +62,66 @@ else if (shouldFail(pathName)) {
                 // check if expected error was found
                 List<Pair<String, Integer>> expectedErrors = isDirectory ? getExpectedErrorsFromDirectory(path)
                         : getExpectedErrorsFromFile(path);
-                if (diagnostics.getErrors().size() != expectedErrors.size()) {
-                    System.out.println("Multiple errors found in: " + pathName + " --- expected exactly "
-                            + expectedErrors.size() + " errors. \n" + diagnostics.getErrorOutput());
-                    fail();
-                }
-                if (!expectedErrors.isEmpty()) {
-                    for (LJError e : diagnostics.getErrors()) {
-                        String foundError = e.getTitle();
-                        int errorPosition = e.getPosition().getLine();
-                        boolean match = expectedErrors.stream().anyMatch(
-                                expected -> expected.first().equals(foundError) && expected.second() == errorPosition);
-
-                        if (!match) {
-                            System.out.println("Error in: " + pathName + " --- expected errors: " + expectedErrors
-                                    + ", but found: " + foundError + " at " + errorPosition + ". \n"
-                                    + diagnostics.getErrorOutput());
-                            fail();
-                        }
-                    }
-                } else {
-                    System.out.println("No expected error messages found for: " + pathName);
-                    System.out.println(
-                            "Please specify each expected error in the test file as a comment on the line where the error should be reported.");
-                    fail();
-                }
+                checkExpectedDiagnostics(pathName, diagnostics.getErrors(), expectedErrors,
+                        diagnostics.getErrorOutput());
+            }
+        }
+    }
+
+    /**
+     * Checks that the found diagnostics match the expected diagnostics
+     */
+    private static void checkExpectedDiagnostics(String pathName, Collection<? extends LJDiagnostic> found,
+            List<Pair<String, Integer>> expected, String output) {
+        if (found.size() != expected.size()) {
+            System.out.println("Unexpected number of diagnostics found in: " + pathName + " --- expected exactly "
+                    + expected.size() + ". \n" + output);
+            fail();
+        }
+        if (expected.isEmpty()) {
+            System.out.println("No expected diagnostic messages found for: " + pathName);
+            System.out.println(
+                    "Please specify each expected diagnostic in the test file as a comment on the line where it should be reported.");
+            fail();
+        }
+        for (LJDiagnostic diagnostic : found) {
+            boolean match = expected.stream().anyMatch(expectedDiagnostic -> matches(diagnostic, expectedDiagnostic));
+            if (!match) {
+                System.out.println(
+                        "Unexpected diagnostic in: " + pathName + " --- expected: " + expected + ". \n" + output);
+                fail();
             }
         }
     }
 
+    private static boolean matches(LJDiagnostic diagnostic, Pair<String, Integer> expected) {
+        if (diagnostic.getPosition().getLine() != expected.second())
+            return false;
+        return !(diagnostic instanceof LJError) || diagnostic.getTitle().equals(expected.first());
+    }
+
     /**
-     * Returns a Stream of paths to test files in the testSuite directory. These include files with names starting with
-     * "Correct" or "Error", and directories containing "correct" or "error". §
-     * 
-     * @return Stream of paths to test files
-     *
-     * @throws IOException
-     *             if an I/O error occurs or the path does not exist
+     * Returns the test suite paths to verify
      */
     private static Stream<Path> sourcePaths() throws IOException {
         return Files.find(Paths.get("../liquidjava-example/src/main/java/testSuite/"), Integer.MAX_VALUE,
                 (filePath, fileAttr) -> {
                     String name = filePath.getFileName().toString();
-                    // Files that start with "Correct" or "Error"
+                    // Files that start with "Correct", "Error" or "Warning"
                     boolean isFileStartingWithCorrectOrError = fileAttr.isRegularFile()
-                            && (shouldPass(name) || shouldFail(name));
+                            && (shouldPass(name) || shouldFail(name) || shouldWarn(name));
 
-                    // Directories that contain "correct" or "error"
+                    // Directories that contain "correct", "error" or "warning"
                     boolean isDirectoryWithCorrectOrError = fileAttr.isDirectory()
-                            && (shouldPass(name) || shouldFail(name));
+                            && (shouldPass(name) || shouldFail(name) || shouldWarn(name));
 
                     // Return true if either condition matches
                     return isFileStartingWithCorrectOrError || isDirectoryWithCorrectOrError;
                 });
     }
 
     /**
-     * Test multiple paths at once, including both files and directories. This test ensures that the verifier can handle
-     * multiple inputs correctly and that no errors are found in files/directories that are expected to be correct.
+     * Verifies that multiple correct inputs can be processed together
      */
     @Test
     public void testMultiplePaths() {

liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java

@@ -16,81 +16,70 @@
 
 public class TestUtils {
 
+    private static final Pattern EXPECTED_DIAGNOSTIC = Pattern.compile("//\\s*(.*?\\b(Error|Warning)\\b)", Pattern.CASE_INSENSITIVE);
     private final static Factory factory = new Launcher().getFactory();
     private final static Context context = Context.getInstance();
 
-    /**
-     * Determines if the given path indicates that the test should pass
-     * 
-     * @param path
-     */
     public static boolean shouldPass(String path) {
         return path.toLowerCase().contains("correct");
     }
 
-    /**
-     * Determines if the given path indicates that the test should fail
-     * 
-     * @param path
-     */
     public static boolean shouldFail(String path) {
         return path.toLowerCase().contains("error");
     }
 
-    /**
-     * Reads the expected error messages from the given file by looking for a comment containing the expected error
-     * message.
-     * 
-     * @param filePath
-     * 
-     * @return list of expected error messages found in the file, or empty list if there was an error reading the file
-     *         or if there are no expected error messages in the file
-     */
+    public static boolean shouldWarn(String path) {
+        return path.toLowerCase().contains("warning");
+    }
+
     public static List<Pair<String, Integer>> getExpectedErrorsFromFile(Path filePath) {
-        List<Pair<String, Integer>> expectedErrors = new ArrayList<>();
+        return getExpectedDiagnosticsFromFile(filePath, "error");
+    }
+
+    private static List<Pair<String, Integer>> getExpectedDiagnosticsFromFile(Path filePath, String type) {
+        List<Pair<String, Integer>> expectedDiagnostics = new ArrayList<>();
         try (BufferedReader reader = Files.newBufferedReader(filePath)) {
             String line;
             int lineNumber = 0;
             while ((line = reader.readLine()) != null) {
                 lineNumber++;
-                Pattern p = Pattern.compile("//\\s*(.*?\\bError\\b)", Pattern.CASE_INSENSITIVE);
-                Matcher m = p.matcher(line);
-                if (m.find()) {
-                    expectedErrors.add(new Pair<>(m.group(1).trim(), lineNumber));
+                Matcher matcher = EXPECTED_DIAGNOSTIC.matcher(line);
+                if (matcher.find() && matcher.group(2).equalsIgnoreCase(type)) {
+                    expectedDiagnostics.add(new Pair<>(matcher.group(1).trim(), lineNumber));
                 }
             }
         } catch (IOException e) {
             return List.of();
         }
-        return expectedErrors;
+        return expectedDiagnostics;
+    }
+
+    public static List<Pair<String, Integer>> getExpectedWarningsFromFile(Path filePath) {
+        return getExpectedDiagnosticsFromFile(filePath, "warning");
     }
 
-    /**
-     * Reads the expected error messages from all files in the given directory and combines them into a single list
-     * 
-     * @param dirPath
-     * 
-     * @return list of expected error messages from all files in the directory, or empty list if there was an error
-     *         reading the directory or if there are no files in the directory
-     */
     public static List<Pair<String, Integer>> getExpectedErrorsFromDirectory(Path dirPath) {
-        List<Pair<String, Integer>> expectedErrors = new ArrayList<>();
+        return getExpectedDiagnosticsFromDirectory(dirPath, "error");
+    }
+
+    public static List<Pair<String, Integer>> getExpectedWarningsFromDirectory(Path dirPath) {
+        return getExpectedDiagnosticsFromDirectory(dirPath, "warning");
+    }
+
+    private static List<Pair<String, Integer>> getExpectedDiagnosticsFromDirectory(Path dirPath, String type) {
+        List<Pair<String, Integer>> expectedDiagnostics = new ArrayList<>();
         try {
             List<Path> files = Files.list(dirPath).filter(Files::isRegularFile).toList();
             for (Path file : files) {
-                expectedErrors.addAll(getExpectedErrorsFromFile(file));
+                expectedDiagnostics.addAll(getExpectedDiagnosticsFromFile(file, type));
             }
         } catch (IOException e) {
             return List.of();
         }
-        return expectedErrors;
+        return expectedDiagnostics;
     }
 
-    /**
-     * Helper method to add an integer variable to the context
-     */
     public static void addIntVariableToContext(String name) {
-        context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, new Predicate(),
-                factory.Code().createCodeSnippetStatement(""));
+        context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, new Predicate(), factory.Code().createCodeSnippetStatement(""));
     }
 }