Repository navigation

Soundness holes: Tests and fixes - #257

Closed

GUIpsp wants to merge 21 commits into

mainfrom

soundness-hole-fixes

Closed

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
  
  GUIpsp
  and
  claude
  committed
  6519c7b
- Add soundness-hole test: double remainder (IEEE vs fmod)
  
  GUIpsp
  and
  claude
  committed
  4eb45ac
- Fix floating-point % to use Java fmod, not IEEE-754 remainder
  
  GUIpsp
  and
  claude
  committed
  5c6a6ab
- Add soundness-hole test: float precision (FP64 vs binary32)
  
  GUIpsp
  and
  claude
  committed
  9ee52f7
- Model Java float as 32-bit FP (binary32) with float->double promotion
  
  GUIpsp
  and
  claude
  committed
  1b64f32
- Add soundness-hole test: short-circuit RHS side effect applied
  
  GUIpsp
  and
  claude
  committed
  5d3f1c2
- Discard assignments in the short-circuited operand of && / ||
  
  GUIpsp
  and
  claude
  committed
  c23f819
- Add soundness-hole test: field refinement assumed not established
  
  GUIpsp
  and
  claude
  committed
  cc0ae00
- Read an unestablished external field at its default, not its refinement
  
  GUIpsp
  and
  claude
  committed
  7ffc2ac
- Add soundness-hole test: loop modeled as one iteration
  
  GUIpsp
  and
  claude
  committed
  ff8623f
- Havoc variables written in loop bodies
  
  GUIpsp
  and
  claude
  committed
  e5ce861
- Add soundness-hole test: exceptional control flow ignored
  
  GUIpsp
  and
  claude
  committed
  9dcb850
- Havoc variables written in try/catch bodies
  
  GUIpsp
  and
  claude
  committed
  95aef14
- Add soundness-hole test: narrowing cast ignored
  
  GUIpsp
  and
  claude
  committed
  1b7d95a
- Model floating-point to integral narrowing casts as truncation
  
  GUIpsp
  and
  claude
  committed
  12a6cf3
- Add soundness-hole test: typestate stale under aliasing
  
  GUIpsp
  and
  claude
  committed
  671ad43
- Invalidate aliased typestate on a state transition
  
  GUIpsp
  and
  claude
  committed
  9106d32
- Add soundness-hole test: int multiplication overflow
  
  GUIpsp
  and
  claude
  committed
  f134911
- Add soundness-hole test: int negative modulo
  
  GUIpsp
  and
  claude
  committed
  6243c93
- Add soundness-hole test: long division truncation
  
  GUIpsp
  and
  claude
  committed
  a6c5b85
- Model Java integral types as fixed-width BitVectors
  
  GUIpsp
  and
  claude
  committed
  11c748c

Commits

Commits on Jun 15, 2026