Multiple Errors

[rcosta358]

This PR closes #82 and liquid-java/vscode-liquidjava#3, by making it possible for the verifier to report more than one error at a time. This was done by throwing an LJError which stops the verification until it is caught in the method, class, interface or field visitors in the RefinementTypeChecker and then resuming the verification. For the other visitor classes, a general try-catch is present in the RefinementProcessor.

Tests were also added.

---

Additional Improvement

The verifier sometimes caught the same error twice, because spoon was calling the visitor methods more than once. Claude fixed this by changing pkg.accept() to pkg.getTypes().forEach() in theRefinementProcessor, to prevent types (classes, methods, interfaces, fields) in nested packages from being verified multiple times when the ProcessingManager traversed the package hierarchy.

This change also makes the verification run faster.

Before

liquidjava/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java

Lines 25 to 38 in 9b14c3f

	@Override
	public void process(CtPackage pkg) {
	if (!visitedPackages.contains(pkg)) {
	visitedPackages.add(pkg);
	Context c = Context.getInstance();
	c.reinitializeAllContext();
	pkg.accept(new FieldGhostsGeneration(c, factory)); // generate annotations for field ghosts
	pkg.accept(new ExternalRefinementTypeChecker(c, factory));
	pkg.accept(new MethodsFirstChecker(c, factory)); // double passing idea (instead of headers)
	pkg.accept(new RefinementTypeChecker(c, factory));
	}
	}
	}

After

liquidjava/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java

Lines 28 to 53 in 3d8b2dc

	@Override
	public void process(CtPackage pkg) {
	if (!visitedPackages.contains(pkg)) {
	visitedPackages.add(pkg);
	Context c = Context.getInstance();
	c.reinitializeAllContext();
	try {
	// process types in this package only, not sub-packages
	// first pass: gather refinements
	pkg.getTypes().forEach(type -> {
	type.accept(new FieldGhostsGeneration(c, factory)); // generate annotations for field ghosts
	type.accept(new ExternalRefinementTypeChecker(c, factory)); // process external refinements
	type.accept(new MethodsFirstChecker(c, factory)); // double passing idea (instead of headers)
	});
	// second pass: check refinements
	pkg.getTypes().forEach(type -> {
	type.accept(new RefinementTypeChecker(c, factory));
	});
	} catch (LJError e) {
	diagnostics.add(e);
	}
	}
	}
	}

[CatarinaGamboa]

Great improvement 🔥🔥🔥