Cleanup side effects in declaration initialisers #5669
Conversation
tautschnig
requested review from
kroening,
peterschrammel and
smowton
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #5669 +/- ##
========================================
Coverage 69.49% 69.49%
========================================
Files 1243 1243
Lines 100674 100680 +6
========================================
+ Hits 69962 69968 +6
Misses 30712 30712
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
tautschnig
force-pushed
the
decl-side-effect
branch
3 times, most recently
from
8aa31e5 to
ef81046
Compare
tautschnig
force-pushed
the
decl-side-effect
branch
from
ef81046 to
554c20f
Compare
| // make sure the resulting expression has the same type as before. | ||
| exprt lhs = typecast_exprt::conditional_cast( | ||
| skip_typecast(to_binary_expr(expr).op0()), expr.type()); | ||
| expr.swap(lhs); |
There was a problem hiding this comment.
I am a bit worried about the skip_typecast, since that may remove any number of casts.
Say think of (int)(char)i, where i is an integer.
There was a problem hiding this comment.
Thank you for calling this out! I have now added sanity checks and refrained from using skip_typecast.
tautschnig
force-pushed
the
decl-side-effect
branch
from
554c20f to
cda2e53
Compare
tautschnig
force-pushed
the
decl-side-effect
branch
from
cda2e53 to
bc19627
Compare
|
|
||
| // we previously weren't able to handle the below | ||
| short a = (a ^= 0) || __assert_fail("", 2, __PRETTY_FUNCTION__); | ||
| } |
There was a problem hiding this comment.
I would replace the architecture-specific __assert_fail by some other side effect, say x++ or the like.
There was a problem hiding this comment.
Done (I've added a call to a newly added function, which in turn calls __CPROVER_assert).
| { | ||
| // Skip over those type casts, but also | ||
| // make sure the resulting expression has the same type as before. | ||
| PRECONDITION(to_typecast_expr(lhs).op().type() == expr.type()); |
There was a problem hiding this comment.
I would add a DATA_INVARIANT here to check that the typecast is there, and turn that PRECONDITION into a DATA_INVARIANT.
Declarations with initialisers generate a declaration and an assignment. The side effect in the rhs of the assignment was never cleaned up, resulting in a failing invariant during symex for the regression test included. The test was built by C-Reduce on a example originating from CSmith.
tautschnig
force-pushed
the
decl-side-effect
branch
from
bc19627 to
e63f895
Compare
3 participants
Declarations with initialisers generate a declaration and an assignment.
The side effect in the rhs of the assignment was never cleaned up,
resulting in a failing invariant during symex for the regression test
included.
The test was built by C-Reduce on a example originating from CSmith.