| 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
|
|
|
|
|
|
using "../"
|
|
|
|
Remove additional reference counting as part of UpdateNodeList and
UpdateNode. Simplifies code.
|
|
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.
|
|
The caching maps in ArrayExpr are broken, they only consider hashes
and don't check for structural equality. This can lead to hash collisions
and invalid Expr replacement. This is especially potetent for UpdateLists, who
only put the array name in the hash, so there can be a lot of colisions.
|
|
* use `using` instead of typdef
* use `collection.empty()` instead of size
* use `auto` if clear
* use `emplace_back` where useful
* use `nullptr` instead of NULL
* use `override` if applicable
* use `explicit` for constructor to avoid implicit conversion
|
|
Don't pollute the project include directory with optimization specific
headers.
|
|
|
|
|
|
|
