Issues

External specs: a @StateSet declared later in the file is not found by an interface earlier in it

liquid-java/liquidjava#452 · opened

on Oct 29, 2026

Crash: "Sorts Int and Bool are incompatible" when a JDK method's result is passed to a parameter refined in an external spec

liquid-java/liquidjava#451 · opened

on Oct 29, 2026

False error in external specs: a @Ghost the constructor does not set gives "Ghost 'old' could not be found" at the next from-only call

liquid-java/liquidjava#450 · opened

on Oct 29, 2026

False error: @StateRefinement(from = "false") gives "State Conflict Error: Found multiple disjoint states"

liquid-java/liquidjava#449 · opened

on Oct 29, 2026

Crash: an array initializer (new T[] {...}) passed to a parameter refined with length() gives "Sorts ... and Bool are incompatible"

liquid-java/liquidjava#448 · opened

on Oct 29, 2026

Soundness: a field initialised in its declaration keeps that state in other methods, even after the constructor changed it

liquid-java/liquidjava#446 · opened

on Oct 29, 2026

1

False error: a known state 'a or b' is refused by a method allowed from a and from b (one @StateRefinement per state)

liquid-java/liquidjava#445 · opened

on Oct 29, 2026

A float ghost crashes the verifier: "Ghost not implemented for type float"

liquid-java/liquidjava#443 · opened

on Oct 29, 2026

In-source return refinement `_ == true --> s(this)` binds `this` to the return value (Argument Mismatch)

liquid-java/liquidjava#442 · opened

on Oct 29, 2026

Soundness: reassigning a parameter changes the state recorded from its earlier use (`new HashMap<>(n); n = 5`)

liquid-java/liquidjava#439 · opened

on Oct 28, 2026

Soundness: a field write through another object of the same class (`o.x = 5`) is applied to `this.x`

liquid-java/liquidjava#438 · opened

on Oct 28, 2026

Internal error "Expr cannot be cast to BoolExpr" on a local assigned from an array element (`Res r = rs[0]`)

liquid-java/liquidjava#437 · opened

on Oct 28, 2026

Verifier crashes on `++` or `--` on a field of another object (`c.count++`)

liquid-java/liquidjava#436 · opened

on Oct 28, 2026

Named state sets, so a spec can refer to a whole set (e.g. old(phase(this)))

liquid-java/liquidjava#435 · opened

on Oct 28, 2026

Unannotated methods of the same class: a parameter's state is unknown inside, and the method's effect is lost at the call site

liquid-java/liquidjava#429 · opened

on Oct 27, 2026

Only the first error in a method is reported; later errors in the same method are hidden

liquid-java/liquidjava#428 · opened

on Oct 27, 2026

Soundness: after a loop, an object with an external spec keeps the state set inside the loop body

liquid-java/liquidjava#427 · opened

on Oct 27, 2026

Verifier crashes on an assignment to a field of a class that cannot be resolved

liquid-java/liquidjava#426 · opened

on Oct 27, 2026

External refinements are not applied to packages checked before the spec's package

liquid-java/liquidjava#416 · opened

on Oct 24, 2026

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

liquid-java/liquidjava#406 · opened

on Oct 14, 2026

False error: a call used as an operand loses the link between its return refinement and its arguments

liquid-java/liquidjava#405 · opened

on Oct 13, 2026

False error: array length is not known to be non-negative

liquid-java/liquidjava#404 · opened

on Oct 13, 2026

TestExamples crashes on a diagnostic without a source position

liquid-java/liquidjava#403 · opened

on Oct 13, 2026

Soundness: an error in an enum or record static initializer hides errors in later types

liquid-java/liquidjava#402 · opened

on Oct 13, 2026

Soundness: a Java version set in the maven-compiler-plugin configuration is ignored, so declarations are dropped and verification passes

liquid-java/liquidjava#401 · opened

on Oct 13, 2026

Navigation Menu

Repository navigation

Issues

External specs: a @StateSet declared later in the file is not found by an interface earlier in it

Crash: "Sorts Int and Bool are incompatible" when a JDK method's result is passed to a parameter refined in an external spec

False error in external specs: a @Ghost the constructor does not set gives "Ghost 'old' could not be found" at the next from-only call

False error: @StateRefinement(from = "false") gives "State Conflict Error: Found multiple disjoint states"

Crash: an array initializer (new T[] {...}) passed to a parameter refined with length() gives "Sorts ... and Bool are incompatible"

Soundness: a field initialised in its declaration keeps that state in other methods, even after the constructor changed it

False error: a known state 'a or b' is refused by a method allowed from a and from b (one @StateRefinement per state)

A float ghost crashes the verifier: "Ghost not implemented for type float"

In-source return refinement `_ == true --> s(this)` binds `this` to the return value (Argument Mismatch)

Soundness: reassigning a parameter changes the state recorded from its earlier use (`new HashMap<>(n); n = 5`)

Soundness: a field write through another object of the same class (`o.x = 5`) is applied to `this.x`

Internal error "Expr cannot be cast to BoolExpr" on a local assigned from an array element (`Res r = rs[0]`)

Verifier crashes on `++` or `--` on a field of another object (`c.count++`)

Named state sets, so a spec can refer to a whole set (e.g. old(phase(this)))

Unannotated methods of the same class: a parameter's state is unknown inside, and the method's effect is lost at the call site

Only the first error in a method is reported; later errors in the same method are hidden

Soundness: after a loop, an object with an external spec keeps the state set inside the loop body

Verifier crashes on an assignment to a field of a class that cannot be resolved

External refinements are not applied to packages checked before the spec's package

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

False error: a call used as an operand loses the link between its return refinement and its arguments

False error: array length is not known to be non-negative

TestExamples crashes on a diagnostic without a source position

Soundness: an error in an enum or record static initializer hides errors in later types

Soundness: a Java version set in the maven-compiler-plugin configuration is ignored, so declarations are dropped and verification passes