Use symbol_tablet::lookup_ref and ::get_writeable_ref #4437
Conversation
smowton
requested review from
cesaro,
chrisr-diffblue,
cristina-david,
danpoe,
hannes-steffenhagen-diffblue,
kroening,
martin-cs,
NathanJPhillips,
owen-mc-diffblue,
peterschrammel,
pkesseli,
tautschnig and
thk123
as code owners
These all replace uses of lookup and get_writeable that were immediately dereferenced without being checked, thereby replacing any possible failure due to reading through a null pointer with an invariant failure.
smowton
force-pushed
the
smowton/cleanup/symbol-table-ref-methods
branch
from
096a25c to
b79a100
Compare
There was a problem hiding this comment.
This seems like a worth-while thing to do and the changes to my area are fine BUT could we make this simpler and more stringent? Are there any legitimate uses of get_writeable where it is null? Couldn't this become an invariant in general? Likewise what exactly are the invariants on lookup?
|
Users of So there aren't many users but they do exist. Unsure what you're asking about |
| @@ -227,7 +227,7 @@ void acceleration_utilst::stash_variables( | |||
| it!=vars.end(); | |||
| ++it) | |||
| { | |||
| symbolt orig=*symbol_table.lookup(*it); | |||
| symbolt orig = symbol_table.lookup_ref(*it); | |||
| @@ -768,7 +768,7 @@ void polynomial_acceleratort::stash_variables( | |||
| it!=vars.end(); | |||
| ++it) | |||
| { | |||
| symbolt orig=*symbol_table.lookup(*it); | |||
| symbolt orig = symbol_table.lookup_ref(*it); | |||
These were never changed, so might as well hold a reference into the symbol table.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: b79a100).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105870484
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 78c1c31).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105877346
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.
These all replace uses of lookup and get_writeable that were immediately dereferenced without
being checked, thereby replacing any possible failure due to reading through a null pointer with
an invariant failure.