[tautschnig]

Class: create primitive classes without calling forName

Class.forName calls CProver.notModelled() and then throws an
AssertionError, as its model is incomplete. getPrimitiveClass(String),
getPrimitiveClass(int) and getSuperclass() still called forName, and
the static initializers of all boxed types call getPrimitiveClass (e.g.,
Integer. calls getPrimitiveClass(4)). Thus, JBMC reported a
failing assertion in forName for any program that uses a boxed type, and
did not explore any paths beyond that call.

Create the Class objects in getPrimitiveClass directly instead.
isPrimitive(), which compares the name with string literals by
reference, still works, as the names are the same literals.

getSuperclass() now returns null, which matches the existing comment
that the model assumes there is no superclass. Returning a new Class
object instead would make Enum.getDeclaringClass() return a different
object on each call, so that E.A.getDeclaringClass() ==
E.B.getDeclaringClass() would not hold.

With JBMC, assertions about Integer.TYPE.isPrimitive() and getName(),
and about HashMap and ArrayList of Integer, now verify, and a false
assertion about a HashMap is still reported as failing.

Byte, Short, Float: use the right primitive class for TYPE

Byte.TYPE, Short.TYPE and Float.TYPE were initialised with
getPrimitiveClass(7), which is the class of double, so that, e.g.,
Byte.TYPE.getName() returned "double". Use the indices of byte (2),
short (3) and float (6) instead, and mark the change from the JDK
source, which uses getPrimitiveClass(String), as Integer.java does.

[Copilot]

Pull request overview

This PR prevents internal java.lang.Class helpers (primitive-class lookup and getSuperclass()) from calling Class.forName(String), which is intentionally CProver.notModelled() + AssertionError in this model library. This avoids spurious verification failures triggered during boxed-primitive <clinit> execution (e.g., Integer.TYPE initialization).

Changes:

• Add a private cproverClassWithName(String) factory to create Class instances with a known name without routing through forName.
• Route getPrimitiveClass(String), getPrimitiveClass(int), and getSuperclass() through the new factory.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.