Issues

• A constructor of one class cannot change the state of its argument (new PipedInputStream(pos) connects pos)

  enhancement
  liquid-java/liquidjava#380 · Filter by author CatarinaGamboa opened on Oct 8, 2026

• An external spec cannot refine methods its class inherits

  bug
  liquid-java/liquidjava#379 · Filter by author CatarinaGamboa opened on Oct 8, 2026

• States named across specs resolve only if the declaring spec was registered first

  bug
  liquid-java/liquidjava#378 · Filter by author CatarinaGamboa opened on Oct 8, 2026

• Verifier crashes when a subclass value is assigned to a supertype local: "Sorts java.lang.Exception and java.io.IOException are incompatible"

  bug
  liquid-java/liquidjava#377 · Filter by author CatarinaGamboa opened on Oct 8, 2026

• Verifier crashes on a generic type variable compared with its bound: "Sorts X and java.lang.Throwable are incompatible"

  bug
  liquid-java/liquidjava#376 · Filter by author CatarinaGamboa opened on Oct 8, 2026

• Simplify trues when not used

  enhancement
  liquid-java/liquidjava#375 · Filter by author CatarinaGamboa opened on Oct 8, 2026

• Dont simplify the target variable in Found

  enhancement
  liquid-java/liquidjava#374 · Filter by author CatarinaGamboa opened on Oct 8, 2026

• Rename fresh to more useful name

  enhancement
  liquid-java/liquidjava#373 · Filter by author CatarinaGamboa opened on Oct 8, 2026

• Calls on this inside a user subclass of a specified JDK class are not checked

  bug
  liquid-java/liquidjava#372 · Filter by author CatarinaGamboa opened on Oct 8, 2026

• Soundness: an if without else on a bare boolean drops the path where the branch is not taken

  bug
  liquid-java/liquidjava#371 · Filter by author CatarinaGamboa opened on Oct 8, 2026

• Detect delegating superclass constructors from bytecode instead of a hard-coded list

  liquid-java/liquidjava#367 · Filter by author CatarinaGamboa opened on Oct 8, 2026

• Soundness: try/catch is checked as if the catch block always runs

  bug
  liquid-java/liquidjava#364 · Filter by author CatarinaGamboa opened on Oct 7, 2026

• Support bitwise and shift compound assignments without internal null errors

  bug
  liquid-java/liquidjava#360 · Filter by author rcosta358 opened on Oct 6, 2026

• Verifier crashes on a call to a varargs method with two or more arguments

  bug
  liquid-java/liquidjava#349 · Filter by author CatarinaGamboa opened on Oct 6, 2026

• False error: a[i].length is rejected as an invalid refinement expression

  bug
  liquid-java/liquidjava#348 · Filter by author CatarinaGamboa opened on Oct 6, 2026

• False error: a var local passed to a refined parameter ("expected int, got var")

  bug
  liquid-java/liquidjava#347 · Filter by author CatarinaGamboa opened on Oct 6, 2026

• Verifier crashes on yield new X(...) when X's constructor is refined

  bug
  liquid-java/liquidjava#346 · Filter by author CatarinaGamboa opened on Oct 6, 2026

• Verifier crashes on a type-pattern switch (case String s ->)

  bug
  liquid-java/liquidjava#345 · Filter by author CatarinaGamboa opened on Oct 6, 2026

• Verifier crashes on a var local in a binary operator

  bug
  liquid-java/liquidjava#344 · Filter by author CatarinaGamboa opened on Oct 6, 2026

• Verifier crashes on a method call inside a static method of an interface

  bug
  liquid-java/liquidjava#343 · Filter by author CatarinaGamboa opened on Oct 6, 2026

• Soundness: the methods of a record are not verified when an external spec is present

  bug
  liquid-java/liquidjava#342 · Filter by author CatarinaGamboa opened on Oct 6, 2026

• Soundness: a call inside an anonymous class body changes the field state seen by other methods

  bug
  liquid-java/liquidjava#341 · Filter by author CatarinaGamboa opened on Oct 6, 2026

• Soundness: a field read in another method is assumed to still hold its initializer

  bug
  liquid-java/liquidjava#340 · Filter by author CatarinaGamboa opened on Oct 6, 2026

• Soundness: a catch block is checked as if the whole try block had completed

  bug
  liquid-java/liquidjava#339 · Filter by author CatarinaGamboa opened on Oct 6, 2026

• Soundness: after a loop, the state is taken from the loop body as if it ran at least once

  bug
  liquid-java/liquidjava#338 · Filter by author CatarinaGamboa opened on Oct 6, 2026