Skip to content

Instance Variables Leak Between Sibling Methods #270

Description

@rcosta358

Description
In the following example, when both the fibonacci and factorial methods are present, LiquidJava fails to report an expected verification error on the recursive call inside factorial.

Removing the fibonacci method or renaming one of the n parameters causes the expected error to be reported correctly.

Minimal reproducer

int wrongFibonacci(@Refinement("_ > 0") int n) {
    if (n == 1) return 1;
    else return fibonacci(n - 1) + fibonacci(n - 2); // reports error ✅
}

int wrongFactorial(@Refinement("_ > 0") int n) {   
    return n * factorial(n - 1); // does not report error ❌
}

Expected behavior
Recursive call of factorial should report an error because when n == 1, on the next call n == 0, which violates the parameter refinement.

Actual behavior
Does not report the error.

Likely cause
Instance variables with the same name leak between sibling methods.

Environment

  • LiquidJava version / commit: 0.0.27
  • Java version (java -version): 20
  • OS: MacOS 26

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions