Soundness holes: Tests and fixes#257

Open

GUIpsp wants to merge 21 commits into

mainfrom

soundness-hole-fixes

Commits on Jun 15, 2026

Add TestSoundnessHoleRuntime: runtime validation for soundness-hole tests

GUIpsp
and
claude
committed
Add soundness-hole test: double remainder (IEEE vs fmod)

GUIpsp
and
claude
committed
Fix floating-point % to use Java fmod, not IEEE-754 remainder

GUIpsp
and
claude
committed
Add soundness-hole test: float precision (FP64 vs binary32)

GUIpsp
and
claude
committed
Model Java float as 32-bit FP (binary32) with float->double promotion

GUIpsp
and
claude
committed
Add soundness-hole test: short-circuit RHS side effect applied

GUIpsp
and
claude
committed
Discard assignments in the short-circuited operand of && / ||

GUIpsp
and
claude
committed
Add soundness-hole test: field refinement assumed not established

GUIpsp
and
claude
committed
Read an unestablished external field at its default, not its refinement

GUIpsp
and
claude
committed
Add soundness-hole test: loop modeled as one iteration

GUIpsp
and
claude
committed
Havoc variables written in loop bodies

GUIpsp
and
claude
committed
Add soundness-hole test: exceptional control flow ignored

GUIpsp
and
claude
committed
Havoc variables written in try/catch bodies

GUIpsp
and
claude
committed
Add soundness-hole test: narrowing cast ignored

GUIpsp
and
claude
committed
Model floating-point to integral narrowing casts as truncation

GUIpsp
and
claude
committed
Add soundness-hole test: typestate stale under aliasing

GUIpsp
and
claude
committed
Invalidate aliased typestate on a state transition

GUIpsp
and
claude
committed
Add soundness-hole test: int multiplication overflow

GUIpsp
and
claude
committed
Add soundness-hole test: int negative modulo

GUIpsp
and
claude
committed
Add soundness-hole test: long division truncation

GUIpsp
and
claude
committed
Model Java integral types as fixed-width BitVectors

GUIpsp
and
claude
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Soundness holes: Tests and fixes#257

Soundness holes: Tests and fixes#257
GUIpsp wants to merge 21 commits into
mainfrom
soundness-hole-fixes

Commits on Jun 15, 2026

Add TestSoundnessHoleRuntime: runtime validation for soundness-hole tests

Add soundness-hole test: double remainder (IEEE vs fmod)

Fix floating-point % to use Java fmod, not IEEE-754 remainder

Add soundness-hole test: float precision (FP64 vs binary32)

Model Java float as 32-bit FP (binary32) with float->double promotion

Add soundness-hole test: short-circuit RHS side effect applied

Discard assignments in the short-circuited operand of && / ||

Add soundness-hole test: field refinement assumed not established

Read an unestablished external field at its default, not its refinement

Add soundness-hole test: loop modeled as one iteration

Havoc variables written in loop bodies

Add soundness-hole test: exceptional control flow ignored

Havoc variables written in try/catch bodies

Add soundness-hole test: narrowing cast ignored

Model floating-point to integral narrowing casts as truncation

Add soundness-hole test: typestate stale under aliasing

Invalidate aliased typestate on a state transition

Add soundness-hole test: int multiplication overflow

Add soundness-hole test: int negative modulo

Add soundness-hole test: long division truncation

Model Java integral types as fixed-width BitVectors