Skip simple nondet initialization for arrays of bool #3827
Conversation
Nondeterministic arrays of Booleans must go through cell-wise initialization, because they are treated in a special way to cope with the discrepancy between the Java representation of Bools (as bytes) and the solver representation (as single bit literals).
allredj
requested review from
cesaro,
cristina-david,
NathanJPhillips,
peterschrammel,
pkesseli,
smowton and
thk123
as code owners
| @@ -1441,6 +1441,9 @@ void java_object_factoryt::gen_nondet_array_init( | |||
| else | |||
| { | |||
| // Arrays of primitive types can be initialized with a single instruction | |||
| // We don't do this for arrays of Booleans, because Bools are represented | |||
There was a problem hiding this comment.
These are bools not Booleans (i.e. we're talking about the primitive type)
There was a problem hiding this comment.
Oh yes, I wanted to sound smart by correctly capitalising Boolean, but then of course we can confuse it with Boolean objects. Good catch. Since this is blocking TG, I will leave it as it is and do a PR on top of that to correct the typo.
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 0304c32).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97697479
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
|
test-gen/develop is momentarily pointing to this branch. DON'T DELETE |
Nondeterministic arrays of Booleans must go through cell-wise initialization, because they are treated in a special way to cope with the discrepancy between the Java representation of Bools (as bytes) and the solver representation (as single bit literals).