Issues

• 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 with a sort mismatch on .length of a non-int array

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

• External specs do not reach user subclasses: a typestate call on a subclass receiver crashes with a sort mismatch

  bug
  liquid-java/liquidjava#353 · Filter by author CatarinaGamboa 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

• Soundness: a state change made through an alias is not seen through the original variable

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

• Soundness: a typestate call chained on a constructor (new X(..).m()) is not checked

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

• Verifier crashes on instanceof in an if condition

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

• Soundness: the implicit close() of try-with-resources is not modelled

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

• Soundness: catch parameters are not treated as variables (state unchecked, or taken from an unrelated local)

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

• Soundness: short-circuit RHS assignments are treated as executed

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

• Soundness: a field of another class or object is read as this class's field with the same name

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

• Soundness: a local variable with a constant's name shadows the constant (Format.JPG read as local JPG)

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

• Soundness: if/else-if assignment followed by a guard hides a state violation

  bug
  liquid-java/liquidjava#304 · Filter by author CatarinaGamboa opened on Sep 30, 2026

• Soundness: an int passed to a float refined parameter is not checked

  bug
  liquid-java/liquidjava#303 · Filter by author CatarinaGamboa opened on Sep 30, 2026