Commit 4a2013c
committed
Java object factory: initialize AbstractStringBuilder-derived types correctly
These are currently initialized as if they are directly derived from Object, which causes a crash due to the
type inconsistency between StringBuilder { AbstractStringBuilder { Object { } } } and StringBuilder { Object { } }
With this change they are initialised more like normal types, which has the side-effect that any fields they possess
that are *not* special-cased by `initialize_nondet_string_fields` are nondet-initialized as for any other type.
I add a test verifying this new behaviour, and a simpler test checking that Builder and Buffer are usable as
nondet arguments at all.1 parent 6566d10 commit 4a2013c
File tree
31 files changed
+271
-178
lines changed- jbmc
- regression/jbmc-strings
- NondetStringBuilderAndBuffer
- java/lang
- StringModelsWithFields
- java/lang
- src/java_bytecode
- unit/java_bytecode/java_object_factory
31 files changed
+271
-178
lines changedBinary file not shown.
Lines changed: 7 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
Binary file not shown.
Lines changed: 5 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
Binary file not shown.
Lines changed: 5 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
Binary file not shown.
Lines changed: 5 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
Binary file not shown.
Lines changed: 5 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
0 commit comments