| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Previously, the code did two consecutive checks. First one succeeded
only if the given index was not already seen and the second one did
an analogous check but for arrays. However, if the given index usage
was already detected for some array, its usage for another array that
already had some other index detected would be silently skipped and the
`incompatible` flag would not be set.
Therefore, if the code contained e.g. the following conditional jump on two
arrays with two symbolic indices, the multi-index access would remain
undetected:
if ((array1[k] + array2[x] + array2[k]) == 0)
Resulting in the following output:
KLEE: WARNING: OPT_I: infeasible branch!
KLEE: WARNING: OPT_I: successful
|
|
|
|
Value transformation operates on word instead of byte arrays.
That means the Read indicies need to be adjusted to reflect that.
Previously IndexCleanerVisitor tried to remove the multiplications in the index
to covert byte indicies to word indicies. However as the two added test cases show
this is not sufficent. Therefore we remove the IndexCleanerVisistor and just divide
the index with word size which should always be correct.
|
|
buildMixedSelectExpr was using the byte index for holes in the
select condition instead of the word based one. This only occured
if there was more than 1 hole.
|
|
ArrayExprOptimizer read the UpdateList in the wrong order, which
meant that it used least recent update instead of the most recent one.
This patch fixes this as well as adds a test to illustrate the issue.
|
|
|
|
|
|
|
|
|
|
|
