Repository navigation

Make the String and StringBuilder models sound - #75

Closed

nils-loose wants to merge 5 commits into

svcomp27/integrationfrom

fix/string-model-soundness

Closed

Make the String and StringBuilder models sound#75
nils-loose wants to merge 5 commits into
svcomp27/integrationfrom
fix/string-model-soundness

Commits on Oct 18, 2026
- Make the String models match Java
  
  nils-loose
  and
  claude
  committed
  0f84f31
- Make the StringBuilder model exact, and record the index checks of String calls
  
  nils-loose
  and
  claude
  committed
  186d971
- Do not count the exactly defined String UFs as precision loss
  
  nils-loose
  and
  claude
  committed
  ae83736
- Test that the String and StringBuilder models are exact
  
  nils-loose
  and
  claude
  committed
  0df4738
- Keep the nested replace, as precision loss; model the constructor's capacity
  
  nils-loose
  and
  claude
  committed
  ac1a353