[tautschnig]

Commit 75beb6b made Class.forName call CProver.notModelled(), as it does
not run static initializers. Object.getClass() is implemented as
Class.forName(CProver.classIdentifier(this)), so every path through
getClass() was cut off: for example, assertions after a call to
Object.toString(), Enum.compareTo, or an equals() method that compares
getClass() results were reported as SUCCESS without being checked.

The model before that commit, which kept Class objects in two static
arrays of size 8, had problems as well:

• With more than 8 classes, forName returned a nondeterministic object.
• Class literals (Foo.class) were not in the arrays, so
  Class.forName("Foo") == Foo.class was false.
• With JBMC's --nondet-static, the non-final static arrays are
  initialised nondeterministically, which made the search for a class
  name compare it with nondeterministic strings: JBMC's nondet-static
  regression test did not terminate within 15 minutes with that model,
  and finishes within a second when the arrays are final.

Keep all Class objects in a linked list instead, whose head is stored in
a final array so that --nondet-static leaves it alone.
cproverInitializeClassLiteral, which JBMC calls to initialise each class
literal, adds the literal to the list, and forName adds a new Class
object only if none with that name exists yet. Thus there is one Class
object per class name, as in the JVM. forName now throws
NullPointerException for a null name, as the JVM does. It still does
not run static initializers, and does not throw ClassNotFoundException
for names of classes that do not exist; its documentation now says so.

Each lookup compares the name with those of all Class objects created
so far using String.equals, which is expensive for JBMC's string solver
when there are many of them: a program that calls getClass() on objects
of 10 different classes took 81 seconds. JBMC therefore implements
getClass() for all classes except java.lang.Object itself without going
through forName (diffblue/cbmc#9390), so that this lookup is only used
for explicit calls of Class.forName and for getClass() on objects of
type java.lang.Object. For class literals to be added to the list, JBMC
must initialise class literals after the static fields of
java.lang.Class, which diffblue/cbmc#9390 also does; with older versions
of JBMC, Class.forName("Foo") == Foo.class remains false.

This builds on #43, which makes the models' internal uses of forName
(getPrimitiveClass, getSuperclass) use a separate factory instead.

With these models (and #49 for building with JDK 25), 3 of JBMC's
regression tests fail, compared with 113 with the current master branch:
two depend on the numbering of dynamic objects in traces, and one fails
JBMC's trace validation also without this change. This holds both with
and without diffblue/cbmc#9390. With #43 and #49, but without this
change, 3 tests fail as well, but two of them because getClass() on an
object of type java.lang.Object reaches CProver.notModelled().

This PR is based on the branch of #43; until #43 is merged, its base is that branch.

[Copilot]

🟡 Changes recommended

Critical issues allow lazy initialization and concurrent registration to return distinct Class objects for the same name, while concurrent updates can also lose registrations.

2 open issues

• Concurrent class registration returns duplicate Class objects · New
• forName returns noncanonical Class objects before lazy registration · New

What changed in this PR

Restores a working Class.forName model so verification can continue through dependent calls, with a shared registry intended to preserve Class identity.

Changes:

• Replaces the unused fixed-size arrays with a linked registry backed by a final array.
• Registers class literals and reuses registered objects in forName.
• Adds null-name rejection and documents unsupported initialization and class-existence checks.

File	Description
src/​main/​java/​java/​lang/​Class.java	Implements the Class registry, restores forName, and registers class literals.

_{Review effort: Balanced}