Issues

• ESC: latent inconsistency in axioms -- harmless changes (unspecified methods in runtime bigint; an equivalent string.jml restatement) make string-literal methods' preconditions contradictory

  bug
  OpenJML/OpenJML#1024 · Filter by author davidcok opened on Oct 8, 2026

• Test order dependence: compiler.testExtension2 fails after testExtension1 in the same run (extension-loading state survives)

  bug
  OpenJML/OpenJML#1023 · Filter by author davidcok opened on Oct 8, 2026

• Feasibility timeouts reported as 'Aborted feasibility check: unknown reason: "canceled"' (z3 5.1.0 says canceled, not timeout)

  bug
  OpenJML/OpenJML#1022 · Filter by author davidcok opened on Oct 8, 2026
  1

• Windows release: unzipping under a long path silently drops files (163-character entries in the exploded JDK)

  bug
  OpenJML/OpenJML#1021 · Filter by author davidcok opened on Oct 8, 2026

• ESC bit-vector encoding: char compared as signed (c > 'a' fails for c = '\uffff'; Safe-mode char cast checks missing)

  bug
  OpenJML/OpenJML#1020 · Filter by author davidcok opened on Oct 8, 2026

• RAC: Long.MIN_VALUE + 49 evaluates to 49 (long constant plus int), also in Java code

  bug
  OpenJML/OpenJML#1019 · Filter by author davidcok opened on Oct 8, 2026

• Casting a \bigint to int: ESC does not narrow (unsound), RAC warns in Java math mode

  bug
  OpenJML/OpenJML#1018 · Filter by author davidcok opened on Oct 8, 2026
  2

• Type annotations: OpenJML changes to Attr.visitAnnotatedType crash in NOJML mode (NPE on valid code) and on misplaced annotations on anonymous-class new expressions

  bug
  OpenJML/OpenJML#1016 · Filter by author davidcok opened on Oct 8, 2026

• jml-lint: false 'annotation the Java declaration does not have' warnings for @Deprecated Character methods, after a method reference to Character in a generic call

  bug
  OpenJML/OpenJML#1015 · Filter by author davidcok opened on Oct 8, 2026

• Specs: add +RAC counterparts for clauses that are -RAC because they use ESC-only model fields (follow-up to #1012)

  enhancementspecs (of JDK and other Java code)
  OpenJML/OpenJML#1014 · Filter by author davidcok opened on Oct 7, 2026

• Specs tests: generated RAC run-time smoke test for every specified library class (stopgap until real per-class tests)

  enhancementspecs (of JDK and other Java code)
  OpenJML/OpenJML#1013 · Filter by author davidcok opened on Oct 7, 2026

• javac (JDK 11-25): AssertionError in DeferredAttr.DeferredType.complete during recovery of a call on a primitive inside a method argument (hidden; exit code 4)

  bug
  OpenJML/OpenJML#1011 · Filter by author davidcok opened on Oct 6, 2026
  1

• ESC: every toString override fails the inherited Object.toString postcondition (\result.chars == modelString)

  bugspecs (of JDK and other Java code)
  OpenJML/OpenJML#1010 · Filter by author davidcok opened on Oct 6, 2026

• RAC: racbug1 -- invariant calling non-helper methods overflows the stack; golden pins a fragile stack trace

  bug
  OpenJML/OpenJML#1009 · Filter by author davidcok opened on Oct 6, 2026

• setup-vars incorrectly assumes Windows JDK when running the Ubuntu ARM64 distribution under WSL

  OpenJML/OpenJML#1007 · Filter by author marcel139 opened on Oct 5, 2026

• Warnings about declarations in a .jml file are reported against the .java file (wrong file, offset reused)

  OpenJML/OpenJML#1006 · Filter by author davidcok opened on Oct 5, 2026

• Array slices: a[lo..hi] as a value is mis-typed and unsupported in ESC and RAC

  OpenJML/OpenJML#1005 · Filter by author davidcok opened on Oct 5, 2026

• Misc: pre-existing problems and loose ends (from #969 work and the 2026-10-04/05 sessions)

  OpenJML/OpenJML#1004 · Filter by author davidcok opened on Oct 5, 2026

• Generalized quantifiers (\sum, \product, \num_of, \max, \min) and \choose, \choosex in ESC: forms not yet supported or not yet proved

  OpenJML/OpenJML#1003 · Filter by author davidcok opened on Oct 5, 2026

• Unify (or reconcile) the computation of quantifier range bounds: IntegerRangeBounds, RAC bounds, JmlAttr, and \forall/\exists

  OpenJML/OpenJML#1002 · Filter by author davidcok opened on Oct 5, 2026

• ESC support for \sum, \product and \num_of (port of PR #773)

  OpenJML/OpenJML#1001 · Filter by author davidcok opened on Oct 5, 2026

• ESC support for \max and \min; an empty range should be a well-definedness error

  OpenJML/OpenJML#1000 · Filter by author davidcok opened on Oct 5, 2026

• ESC: explain why an assertion could not be established (motivated by T_RacExit's Diverges report), without changing existing output

  enhancement
  OpenJML/OpenJML#999 · Filter by author davidcok opened on Oct 4, 2026
  1

• How to diagnose SMT trigger problems (matching loops) behind long-running or 'possible timeout' ESC proofs

  OpenJML/OpenJML#998 · Filter by author davidcok opened on Oct 4, 2026

• Claude's items at time of 21.0.28 release

  OpenJML/OpenJML#995 · Filter by author davidcok opened on Oct 1, 2026