Record constraints of indexed access to array constants [blocks: #2108] #4673
Conversation
tautschnig
requested review from
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 2c30f84).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112368219
| /*** Variable non-redundant update ***/ | ||
| // No obvious simplifications to writes | ||
|
|
||
| long int nonRedundantWriteLocation; |
| #include <assert.h> | ||
|
|
||
| // C semantics are that these will be zero | ||
| int uninitialisedGlobalArray1[2]; |
| } | ||
| else | ||
| { | ||
| std::vector<std::pair<std::size_t, std::size_t>> ranges; |
There was a problem hiding this comment.
Maybe add a two liner to explain what this case is doing
There was a problem hiding this comment.
Done - I added a paragraph for each of the two cases.
When even constant arrays are left to be handled by the array theory,
expressions such as { 3, 4 }[1] were actually unconstrained as we never
recorded the fact that this expression evaluates to 4. To reduce the
number of constraints to be generated for non-constant indices, ranges
of equal values just yield a single constraint, optimising the case of
large zero-initialised arrays.
tautschnig
force-pushed
the
array-constraints-fix
branch
from
2c30f84 to
10177c6
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 10177c6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112377076
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.
When even constant arrays are left to be handled by the array theory,
expressions such as { 3, 4 }[1] were actually unconstrained as we never
recorded the fact that this expression evaluates to 4. To reduce the
number of constraints to be generated for non-constant indices, ranges
of equal values just yield a single constraint, optimising the case of
large zero-initialised arrays.