Fix bounds checking for structs with flexible array members #4324
Conversation
tautschnig
requested review from
chrisr-diffblue,
danpoe,
martin-cs,
owen-mc-diffblue,
peterschrammel,
smowton and
thk123
as code owners
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 24b6676).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103095037
Status will be re-evaluated on next push.
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).
-
the compatibility was already broken by an earlier merge.
| type_matches_size = | ||
| equal_exprt(size, typecast_exprt(type_size_opt.value(), size.type())); | ||
| { | ||
| type_matches_size = if_exprt{ |
There was a problem hiding this comment.
This definitely warrants an explanatory comment
There was a problem hiding this comment.
Will add one as soon as #4325 is in.
The constraints did not make sure that the dynamic size (__CPROVER_malloc_size) actually referred to the object we are looking at (__CPROVER_malloc_object).
tautschnig
force-pushed
the
flexible-array-fix
branch
from
24b6676 to
ae0a1f3
Compare
tautschnig
assigned tautschnig and unassigned smowton, peterschrammel and chrisr-diffblue
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: ae0a1f3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103124110
Status will be re-evaluated on next push.
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).
-
the compatibility was already broken by an earlier merge.
The constraints did not make sure that the dynamic size (__CPROVER_malloc_size)
actually referred to the object we are looking at (__CPROVER_malloc_object).