False error: a local declared inside try is "not found" at a call in finally #406

With the Barista BufferedInputStream spec (read() returns _ >= -1; read(byte[], int, int) refines its length):

import java.io.*;

public class Repro {
    static int load(InputStream raw, boolean known) throws IOException {
        BufferedInputStream input = new BufferedInputStream(raw);
        try {
            int cost = 0;
            if (known) {
                int length = input.read();
                if (length >= 0) {
                    byte[] nonce = new byte[length];
                    input.read(nonce, 0, length);
                }
            }
            return cost;
        } finally {
            input.close();
        }
    }
}

On main 1c6807b (and 321a732):

Not Found Error: Variable 'length' could not be found
  input.close();   (in the finally)

length is a block-local of the try; the state of input recorded in the try (after read(nonce, 0, length)) mentions it, and when the finally checks close() against that state, length is out of scope. Expected: Correct! Passed Verification. (out-of-scope locals should be eliminated or kept as fresh variables when the state flows into the finally / after the block).

Found in a real-code example (secrets-for-android FileUtils, a length-prefixed read in try/finally). Since #366 the example's earlier workaround (guarding with a block instead of an early return) no longer avoids it.