External refinements are not applied to packages checked before the spec's package #416

An @ExternalRefinementsFor spec is ignored when the code that uses the class is in a package that is checked before the spec's own package: its parent package, or a sibling that comes earlier. A call that violates the spec then passes verification silently.

Example

sub/VectorRefinements.java:

package sub;

import liquidjava.specification.ExternalRefinementsFor;
import liquidjava.specification.Refinement;

@ExternalRefinementsFor("java.util.Vector")
public interface VectorRefinements<E> {
    public void Vector(@Refinement("_ >= 0") int initialCapacity);
}

Client.java, in the unnamed package:

import java.util.Vector;

public class Client {
    public static void main(String[] args) {
        Vector<String> v = new Vector<>(-1);
    }
}

Verifying the directory gives Correct! Passed Verification. (checked with 0.0.35 and main).

Cause

RefinementProcessor.processPackage registers a package's external specs, checks that package's types, and only then recurses into its sub-packages. A spec is therefore unknown while every package checked before its own is verified.

Possible fix

Register the external specs (and the other first-pass information) of the whole package tree before checking any package's types.

Impact

Found while running the Barista benchmark specs (package expert.<class>;) against exercises in the unnamed package: every violation passed until the spec's package line was removed.