|
| 1 | +package liquidjava.api.tests; |
| 2 | + |
| 3 | +import static org.junit.jupiter.api.Assertions.*; |
| 4 | + |
| 5 | +import java.io.IOException; |
| 6 | +import java.nio.file.Files; |
| 7 | +import java.nio.file.Path; |
| 8 | +import java.util.Comparator; |
| 9 | +import java.util.List; |
| 10 | + |
| 11 | +import org.junit.jupiter.api.Test; |
| 12 | + |
| 13 | +import liquidjava.api.CommandLineLauncher; |
| 14 | +import liquidjava.diagnostics.Diagnostics; |
| 15 | +import liquidjava.diagnostics.errors.LJError; |
| 16 | +import spoon.reflect.cu.SourcePosition; |
| 17 | + |
| 18 | +class TestDeclarationPositions { |
| 19 | + @Test |
| 20 | + void smtUnknownPointsToReturnPredicate() throws IOException { |
| 21 | + assertDeclarations("ErrorSMTUnknown.java", "SMT Unknown Error", "_ > 2.0"); |
| 22 | + } |
| 23 | + |
| 24 | + @Test |
| 25 | + void refinementErrorPointsToReturnPredicate() throws IOException { |
| 26 | + assertDeclarations("ErrorIdentity.java", "Refinement Error", "_ > 0"); |
| 27 | + } |
| 28 | + |
| 29 | + @Test |
| 30 | + void smtUnknownPointsToStatePredicate() throws IOException { |
| 31 | + assertDeclarations("ErrorSMTUnknownState.java", "SMT Unknown Error", "amount(this) < limit"); |
| 32 | + } |
| 33 | + |
| 34 | + @Test |
| 35 | + void stateErrorPointsToStatePredicate() throws IOException { |
| 36 | + assertDeclarations("ErrorUnconstrainedStateRefinement.java", "State Refinement Error", "ready(this)"); |
| 37 | + } |
| 38 | + |
| 39 | + @Test |
| 40 | + void declarationsCoverReturnsParametersLocalsAndFields() throws IOException { |
| 41 | + assertDeclarations("ErrorRefinementDeclarationPositions.java", "Refinement Error", "_ > 20", "_ > 30", "_ > 40", |
| 42 | + "_ > 10"); |
| 43 | + } |
| 44 | + |
| 45 | + private static void assertDeclarations(String file, String title, String... predicates) throws IOException { |
| 46 | + Path path = Path.of("../liquidjava-example/src/main/java/testSuite/", file).toRealPath(); |
| 47 | + String source = Files.readString(path); |
| 48 | + CommandLineLauncher.launch(path.toString()); |
| 49 | + List<LJError> errors = Diagnostics.getInstance().getErrors().stream() |
| 50 | + .sorted(Comparator.comparingInt(error -> error.getPosition().getSourceStart())).toList(); |
| 51 | + |
| 52 | + assertEquals(predicates.length, errors.size()); |
| 53 | + for (int i = 0; i < predicates.length; i++) { |
| 54 | + LJError error = errors.get(i); |
| 55 | + assertEquals(title, error.getTitle()); |
| 56 | + assertPredicatePosition(error.getDeclarationPosition(), path, source, predicates[i]); |
| 57 | + assertPredicateUnderline(error, predicates[i]); |
| 58 | + } |
| 59 | + } |
| 60 | + |
| 61 | + private static void assertPredicatePosition(SourcePosition position, Path file, String source, String predicate) |
| 62 | + throws IOException { |
| 63 | + assertNotNull(position, "Missing refinement declaration position"); |
| 64 | + int start = source.indexOf("\"" + predicate + "\"") + 1; |
| 65 | + assertTrue(start > 0, "Predicate not found in fixture: " + predicate); |
| 66 | + assertEquals(start, position.getSourceStart()); |
| 67 | + assertEquals(start + predicate.length() - 1, position.getSourceEnd()); |
| 68 | + assertEquals(file, position.getFile().toPath().toRealPath()); |
| 69 | + } |
| 70 | + |
| 71 | + private static void assertPredicateUnderline(LJError error, String predicate) { |
| 72 | + String output = error.toString().replaceAll("\u001B\\[[;\\d]*m", ""); |
| 73 | + String heading = "--> Refinement declared here:\n"; |
| 74 | + assertTrue(output.contains(heading), "Missing refinement declaration snippet"); |
| 75 | + String snippet = output.substring(output.indexOf(heading) + heading.length()); |
| 76 | + String indent = " ".repeat(error.getDeclarationPosition().getColumn() - 1); |
| 77 | + String underline = "^".repeat(predicate.length()); |
| 78 | + assertTrue(snippet.contains(indent + underline + "\n"), snippet); |
| 79 | + } |
| 80 | +} |
0 commit comments