about summary refs log tree commit diff homepage
path: root/TODO.txt
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2018-07-07 00:00:33 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2019-03-19 10:01:55 +0000
commit28da6d9a03a7e2bf8ab1371267b049c73938c4e5 (patch)
treea90fce26299c741529b884573557051867a8f3ae /TODO.txt
parent19640bf12f051ad531df7295674a574b43c242ae (diff)
downloadklee-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 'TODO.txt')
0 files changed, 0 insertions, 0 deletions