diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2018-07-07 00:00:33 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-03-19 10:01:55 +0000 |
commit | 28da6d9a03a7e2bf8ab1371267b049c73938c4e5 (patch) | |
tree | a90fce26299c741529b884573557051867a8f3ae /test/VectorInstructions | |
parent | 19640bf12f051ad531df7295674a574b43c242ae (diff) | |
download | klee-28da6d9a03a7e2bf8ab1371267b049c73938c4e5.tar.gz |
Fix representation of ReadExpr of equivalent arrays
ObjectStates can be shared between multiple states. A read expression of a symbolic object can be represented differently depending on previous read expression on the same object. If the read expression uses a symbolic index, all pending updates will become entries in the update list of the object state. If the same object state is read again, with a concrete index, the latest update list item will be referenced, even though it might contain more recent but non-essential updates. If, instead, a concrete read will be executed first, it does not contain the non-essential updates. For both executions, the ReadExpr with a constant index will have two different representations, which is not intented. This patch makes sure, we do not include more recent, non-essential updates for concrete reads. Fixes #921
Diffstat (limited to 'test/VectorInstructions')
0 files changed, 0 insertions, 0 deletions