Treat catch parameters as variables with unknown state (#362)

Closes #333.

A catch parameter was never added to the verification context. As a
result:
1. Calls on it skipped typestate checks (`x.initCause(t)` on a caught
`Throwable` passed).
2. It took the state of an earlier, out-of-scope local with the same
name.
3. Assigning it to another variable failed with `Variable 'e' could not
be found`.

**Fix**
- `RefinementTypeChecker#visitCtCatchVariable` registers the catch
parameter like a method parameter: a new variable whose state is
unknown.
- Before that, `Context#removeVarFromContext` drops any variable with
the same name. Java forbids a catch parameter from shadowing a local
that is in scope, so such an entry is always a stale, out-of-scope
local. Fields cannot clash because they are stored under qualified
`this#…` names.

**Tests**
`testSuite/classes/catch_parameter_error` covers the three reproducers.
Each now reports the same "found true but expected noThrowable(…)" error
as the method-parameter case.

**Not fixed here**
Reproducer 3 as written in the issue (`catch (Exception e)` assigned to
a `Throwable` local) now fails with `Sorts java.lang.Throwable and
java.lang.Exception are incompatible`. This bug is separate and already
present on `main`: assigning a subtype to a supertype variable fails the
same way when the subtype comes from a method parameter. The test
therefore uses `catch (Throwable e)` for that case.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/classes/catch_parameter_error/Test.java

@@ -0,0 +1,41 @@
+package testSuite.classes.catch_parameter_error;
+
+public class Test {
+    static void load() throws Exception {
+        throw new Exception("x");
+    }
+
+    // the state of a catch parameter is unknown
+    static void unknownState(Throwable t) {
+        try {
+            load();
+        } catch (Throwable x) {
+            x.initCause(t); // Expect: State Refinement Error
+        }
+    }
+
+    // the catch parameter must not take the state of an earlier local with the same name
+    static void sameNameAsEarlierLocal() {
+        try {
+            load();
+        } catch (Exception ex) {
+            Throwable e = new Throwable("wrapped");
+        }
+        try {
+            load();
+        } catch (Throwable e) {
+            e.initCause(new RuntimeException("more")); // Expect: State Refinement Error
+        }
+    }
+
+    // the catch parameter can be used outside the catch through another variable
+    static void usedAfterCatch() {
+        Throwable failure = new Throwable("none");
+        try {
+            load();
+        } catch (Throwable e) {
+            failure = e;
+        }
+        failure.initCause(new RuntimeException("root")); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/catch_parameter_error/ThrowableRefinements.java

@@ -0,0 +1,18 @@
+package testSuite.classes.catch_parameter_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("java.lang.Throwable")
+@StateSet({"withThrowable", "noThrowable"})
+public interface ThrowableRefinements {
+    @StateRefinement(to = "noThrowable(this)")
+    void Throwable(String message);
+
+    @StateRefinement(to = "withThrowable(this)")
+    void Throwable(String message, Throwable cause);
+
+    @StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
+    Throwable initCause(Throwable cause);
+}

liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java

@@ -149,6 +149,11 @@ public RefinedVariable addVarToContext(String simpleName, CtTypeReference<?> typ
         return vi;
     }
 
+    public void removeVarFromContext(String name) {
+        for (List<RefinedVariable> l : ctxVars)
+            l.removeIf(var -> var.getName().equals(name));
+    }
+
     public RefinedVariable addInstanceToContext(String simpleName, CtTypeReference<?> type, Predicate c,
             CtElement element) {
         RefinedVariable vi = new VariableInstance(simpleName, type, c);

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -34,6 +34,7 @@
 import spoon.reflect.code.CtBinaryOperator;
 import spoon.reflect.code.CtBlock;
 import spoon.reflect.code.CtBreak;
+import spoon.reflect.code.CtCatchVariable;
 import spoon.reflect.code.CtConditional;
 import spoon.reflect.code.CtContinue;
 import spoon.reflect.code.CtDo;
@@ -179,6 +180,15 @@ public <T> void visitCtLocalVariable(CtLocalVariable<T> localVariable) {
         }
     }
 
+    @Override
+    public <T> void visitCtCatchVariable(CtCatchVariable<T> catchVariable) {
+        super.visitCtCatchVariable(catchVariable);
+        // like a method parameter, the caught object is a new variable with unknown state; Java forbids it to share a
+        // name with a local in scope, so a variable with the same name in the context is an out-of-scope local
+        context.removeVarFromContext(catchVariable.getSimpleName());
+        context.addVarToContext(catchVariable.getSimpleName(), catchVariable.getType(), new Predicate(), catchVariable);
+    }
+
     @Override
     public <T> void visitCtNewArray(CtNewArray<T> newArray) {
         super.visitCtNewArray(newArray);