Issues

• escsf1.gitbug481* tests (commons-math3) all stop at type checking

  OpenJML/OpenJML#1120 · Filter by author davidcok opened on Nov 11, 2026

• The org.jmlspecs.models library is not available; tests that use it fail at import

  OpenJML/OpenJML#1119 · Filter by author davidcok opened on Nov 11, 2026

• ESC: a subclass's represents clause is not used when the model field is read through a supertype reference (List<Integer>.contains(int) fails)

  bug
  OpenJML/OpenJML#1118 · Filter by author davidcok opened on Nov 11, 2026
  1

• --smt output is not the actual solver traffic (last query only, line-number prefixes)

  OpenJML/OpenJML#1117 · Filter by author davidcok opened on Nov 11, 2026

• Inferring a type variable as a JML primitive type (\bigint, \real) probably fails

  OpenJML/OpenJML#1116 · Filter by author davidcok opened on Nov 11, 2026

• JmlTypes.isAssignable recognizes BigInteger by string match

  OpenJML/OpenJML#1115 · Filter by author davidcok opened on Nov 11, 2026

• Iterator.hasNext() is specified strictly_pure; rejects natural iterators that update state

  OpenJML/OpenJML#1114 · Filter by author davidcok opened on Nov 11, 2026

• RAC: specs naming non-public members of library classes

  OpenJML/OpenJML#1113 · Filter by author davidcok opened on Nov 10, 2026
  2

• invariants clause: remaining tasks (tracking)

  OpenJML/OpenJML#1112 · Filter by author davidcok opened on Nov 10, 2026

• invariants clause: static-field objects, helper/super/this call sites (unsound), .jml and 'after also' placement

  OpenJML/OpenJML#1111 · Filter by author davidcok opened on Nov 10, 2026

• escfiles2.gitbug898b fails: a precondition feasibility check times out with z3 ≥ 4.16

  OpenJML/OpenJML#1109 · Filter by author davidcok opened on Nov 10, 2026
  2

• ESC: UndefinedCalledMethodPrecondition for a helper getter called in an invariant, reached through an equals override

  OpenJML/OpenJML#1107 · Filter by author davidcok opened on Nov 10, 2026

• Design: invariant composition and framing (cf. Dafny Valid()/Repr) vs. the invariants clause

  OpenJML/OpenJML#1106 · Filter by author davidcok opened on Nov 10, 2026

• ESC: compiling java.math.BigDecimal from source makes every path after 'new BigDecimal(...)' infeasible

  OpenJML/OpenJML#1103 · Filter by author davidcok opened on Nov 9, 2026

• \let initializer cannot refer to ghost or model fields

  bug
  OpenJML/OpenJML#1101 · Filter by author davidcok opened on Nov 9, 2026

• Crash in Flow when a .jml declares a model method with a body and parameters

  bug
  OpenJML/OpenJML#1100 · Filter by author davidcok opened on Nov 9, 2026

• Write and test specs for each Java library class

  OpenJML/OpenJML#1099 · Filter by author davidcok opened on Nov 9, 2026

• RAC: unrepresented model fields -- internal error with skip; interface fields reported without representation

  OpenJML/OpenJML#1098 · Filter by author davidcok opened on Nov 9, 2026

• ESC: don't require the FloatingPoint theory for proofs without floating-point operations

  OpenJML/OpenJML#1097 · Filter by author davidcok opened on Nov 9, 2026

• ESC: \let with a \real variable and a double initializer gives an SMT sort error

  OpenJML/OpenJML#1096 · Filter by author davidcok opened on Nov 9, 2026

• ESC: conditional expression inside \old crashes or is lost at call sites

  bugOpenJML
  OpenJML/OpenJML#1095 · Filter by author davidcok opened on Nov 9, 2026

• Specs: equals() is not tied to uniqueHash, so Map lookups by equal-but-distinct keys fail

  Design of the JML languagespecs (of JDK and other Java code)
  OpenJML/OpenJML#1094 · Filter by author davidcok opened on Nov 9, 2026

• Map.jml: null values, frame of put/remove, null key in clear/isEmpty

  specs (of JDK and other Java code)
  OpenJML/OpenJML#1093 · Filter by author davidcok opened on Nov 9, 2026
  1

• Eclipse: offer to re-check JML projects that depend on a newly added project

  enhancementUser interface improvements
  OpenJML/OpenJML#1092 · Filter by author davidcok opened on Nov 9, 2026

• Eclipse: ESC submenu items have no tooltips

  User interface improvements
  OpenJML/OpenJML#1091 · Filter by author davidcok opened on Nov 9, 2026