bv_get_rec: ensure all expressions are properly typed #7020
Conversation
The regression test included here failed as of 55fc192 for a member_exprt over an untyped nil_exprt was being constructed. While at it, get rid of the split-brain problem that passing the type separately from the expression had created.
|
Windows jobs temporarily failing for https://status.chocolatey.org/issues/2022-07-18-scheduled-maintenance-chocolatey-community-repository-and-website/. |
Codecov Report
@@ Coverage Diff @@
## develop #7020 +/- ##
========================================
Coverage 77.88% 77.88%
========================================
Files 1569 1569
Lines 180891 180892 +1
========================================
+ Hits 140878 140880 +2
+ Misses 40013 40012 -1
Continue to review full report at Codecov.
|
| return bv_get_rec(expr, map_entry.literal_map, 0); | ||
| else | ||
| { | ||
| PRECONDITION(expr.type() == typet{}); |
There was a problem hiding this comment.
This gives me lots of "I don't think types are supposed to work like that" feelings. But I recognise that this is an improvement on what is there and not what the patch is addressing.
| @@ -274,7 +269,9 @@ exprt boolbvt::bv_get_rec( | |||
|
|
|||
| exprt boolbvt::bv_get(const bvt &bv, const typet &type) const | |||
There was a problem hiding this comment.
Can we get rid of this method?
There was a problem hiding this comment.
Not unless we get rid of boolbvt::bv_get_cache, which invokes this method.
The regression test included here failed as of 55fc192 for a
member_exprt over an untyped nil_exprt was being constructed. While at
it, get rid of the split-brain problem that passing the type separately
from the expression had created.