diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-03-22 09:55:53 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-03-22 10:32:49 +0000 |
commit | a6e21a84f3ffa0bfb2031db2abf7e584bc07649f (patch) | |
tree | b4d59874b000a60cb0550e67c5a29f5ba568bbd4 /tools | |
parent | 253796d20214c0886cbc84fbabf0ba4bfd28a8db (diff) | |
download | klee-a6e21a84f3ffa0bfb2031db2abf7e584bc07649f.tar.gz |
Try to fix #348
The problem was that ``assertCreatedPointEvaluatesToTrue()`` used in the IndependentSolver assumed that it would be given an assignment for every array. If this wasn't the case the ``Assignment`` object by default would just replace every read of an unknown array with a byte filled with zeros. This problem would appear if ``IndependentSolver::getInitialValues(...)`` was called without asking for assignment for used arrays. I saw two ways of fixing this * Get an assignment for all arrays even if the client didn't ask for them. This guarantees that is the query is satisfiable then we can compute a concrete assignment. * Just do a "best effort" check and only check expressions that can be fully assigned to. I chose the latter because the first option seems pretty wasteful, especially for an assert. The second option isn't ideal though as it would be possible to compute an assignment that for the whole query leads to "unsat" but we wouldn't notice.
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions