remove lhs_object from goto_trace_stept #2204
Conversation
kroening
force-pushed
the
remove-lhs-object
branch
from
879999c to
aaca385
Compare
|
FWIW I remember @tautschnig expressing ... disappointment ... with the GraphML witnesses. |
kroening
force-pushed
the
remove-lhs-object
branch
from
aaca385 to
72ecad8
Compare
kroening
force-pushed
the
remove-lhs-object
branch
2 times, most recently
from
636bbe1 to
ea0ea36
Compare
|
The way the assignment is generated in error traces is now much simpler -- but it's non-obvious whether that simpler way is right or wrong. |
kroening
force-pushed
the
remove-lhs-object
branch
from
ea0ea36 to
794daaa
Compare
|
Depends on #2824, which should get tweaked/reviewed/merged first. |
|
Reading the code changes I'm finding it near impossible to assess whether what's happening is right or wrong (except that the graphml bit is now missing one sanity check). Can we have tests that actually inspect contents of the trace output, please? |
kroening
force-pushed
the
remove-lhs-object
branch
from
794daaa to
844a34c
Compare
|
Now added a test that checks the cases I could think of for console traces. The XML output changes as the 'value' elements are removed. I'll make that a separate commit. |
Rationale: * lhs_object_value may be extremely large (think of large struct or array), but the information is contained in (more compact form) full_lhs_value. * lhs_object is contained in full_lhs. A helper function is provided to extract it.
kroening
force-pushed
the
remove-lhs-object
branch
from
844a34c to
df868b8
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 844a34c).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: df868b8).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
Not done yet; in particular, it's unclear to me how these GraphML witnesses look like.