[nils-loose]

Fixes a set of small executor bugs. Each commit fixes one bug.

Changes

commit	bug	change
e9ae9b0	class name check rejects default-package names starting with L	Util.checkClassName now rejects only real descriptors (;, (, )). The allowlist is gone, so LinkedListEntry passes too.
eaeb2d9	a main called from main re-runs Intrinsics.init (DuplicateThreadContextException)	If the thread already has a context, init/terminate of an endpoint only count nesting. The outermost endpoint still ends the run.
b09b432	Verifier.nondet* in Main.<clinit> runs before the thread context exists	In SV_COMP mode, the <clinit> of a class that declares static main(String[]) calls Intrinsics.initBeforeEntry. That call starts the execution. main's init then continues it and clears the initializer's locals.
ccd0536	ValueFactory.createObjectValue appends to ClassDepot's cached interface list on every NEW	ClassDepot now returns unmodifiable views, and ValueFactory merges into a copy.
1624541	Field.get looks up the field by the method name get	It now uses reflectFieldName, and boxes a primitive field.
81f8042	AASTORE of an ANEWARRAY String[] row into a MULTIANEWARRAY is dropped	The row is copied into a StringArrayValue and stored. Writes through other references to the row do not reach the copy, so the store records a context loss.
30be08f	an exception leaving super(...)/this(...) (or any <init> call inside a constructor) breaks the invocation stack	The processor marks these invokes using the existing probe 420. Like abandoned <clinit>s, it closes them and their frames when an invoke below them ends or throws. A try/catch in the instrumentation is not possible: HotSpot rejects a handler that covers the uninitialized this ("flags are not assignable").
519c375	GETVALUE_primitive mismatch halts the executor	It now resyncs to the concrete value and records a context loss. A SAFE result becomes UNKNOWN. Violations found on later paths are still reported.
3ee3cb4	DoubleValue/FloatValue.asStringValue not implemented	Returns String.valueOf(concrete), and records a context loss if the value is symbolic.
f6c0a51	tests	EntryAgentSpec (clinit input, nested main, exception from a super constructor), ClassDepotTypeInfoSpec, and asStringValue cases in FloatValueTest

FCMP NaN (fcmp-nan-unordered-not-encoded) is not part of this PR: #74 fixes it the same way.

Measurement

The config is the competition one: --sv-comp, 300 s, --mem15g, no SA. Runs are compared with baseline-results.jsonl.

The measured set has 1501 runs:

• all 1043 baseline-correct runs;
• 55 runs whose KB record names one of these causes;
• 362 non-correct runs that took under 150 s;
• 41 slow expected-VIOLATION runs and algorithms runs.

The float and argv families and every flipped run were re-run on the final head, after the FCMP commit was dropped.

Result: +46 gained, 0 lost, net +46. No new wrong verdict. One wrong verdict is already in the baseline (AlbersProjection_true valid-assert, false VIOLATION) and is unchanged.

task	prop	base	new	pts	commit
argv-tasks/StdAudio_exceptionless	NRE	unknown	SAFE	+2	b09b432
argv-tasks/StdAudio_exceptionprone	NRE	unknown	VIOLATION	+1	b09b432
argv-tasks/PieSegment_true	VA	false VIOLATION	timeout	+16	b09b432 (see limits)
argv-tasks/PieSegment_false	VA	timeout	VIOLATION	+1	b09b432 (see limits)
securibench/Refl2	NRE / VA	unknown	SAFE / VIOLATION	+3	1624541
securibench/Arrays10	NRE / VA	unknown	VIOLATION / VIOLATION	+2	81f8042
securibench/Inter7	NRE / VA	unknown	SAFE / VIOLATION	+3	30be08f
jbmc-regression/StringBuilderCapLen01	both	unknown	SAFE	+4	519c375
jbmc-regression/StringStartEnd01	both	unknown	SAFE	+4	519c375
jbmc-regression/StringIndexMethods01	both	unknown	SAFE	+4	519c375
jbmc-regression/StringBuilderChars04	VA	unknown	VIOLATION	+1	519c375
jbmc-regression/StringValueOf01	both	unknown	SAFE	+4	3ee3cb4
float-nonlinear-calculation/MathSin	VA	unknown	VIOLATION	+1	3ee3cb4

Most commits fix a distinct crash signature, so each flip is attributed by the signature it removes. The two PieSegment flips are the exception: they were checked with a build without b09b432, which reproduces the base results.

These bugs are fixed but flip nothing at 300 s:

• list1, list2 (class name check): they now time out because of path explosion (about 3^10 paths).
• rtems lock-00-01-10 (nested main): the run now gets past init, but the target deadlocks in some rounds. The task's no-deadlock verdict is false, and the run ends in a stall.
• StrictLineReader (clinit): UNKNOWN because of uncaught target exceptions, as the KB predicts.
• SortedListInsert, aastore_aaload1 (ClassDepot): still time out.

Tests

• gradle test: 8748 passed.
• agentTest: 7 passed.

Known limits

• b09b432 affects most tasks. Every Main with an assert has a <clinit> ($assertionsDisabled), so the trace now starts there. Across the 1501 runs this changed only the PieSegment pair. In both, the solver picked different models:
  • PieSegment_true reaches the real assertion failure in base, so the expected verdict looks wrong. On this branch a model with a huge float makes the target loop forever.
  • PieSegment_false: the reverse.
  • Treat these +17 points as luck, not as a fix.
• 81f8042 always records a context loss on such a store. A SAFE result with this pattern stays UNKNOWN.
• 519c375 can hide model bugs. It turns model-bug crashes into context losses. The warning is still logged.
• Unrelated explorer hazard. During development, a VerifyError in the target ("Unable to initialize main class") was reported as SAFE (== OK). A target JVM that fails to start should give UNKNOWN.

🤖 Generated with Claude Code

[nils-loose]

Included in dev through #92 (merge commit 534c182), together with the fixes for interactions between PRs. This PR stays as the record of the change and its measured flips.