abstract_environmentt::eval rework #5644
Conversation
jezhiggins
force-pushed
the
abstract_environmentt-eval
branch
3 times, most recently
from
2af2fcf to
5e51e4c
Compare
| @@ -0,0 +1,15 @@ | |||
| CORE | |||
| union.c | |||
| --variable-sensitivity --vsd --verify | |||
There was a problem hiding this comment.
I think --vsd and --variable-sensitivity should do the same thing. One was for backwards compatibility.
There was a problem hiding this comment.
Please can you go down to just one of these two?
| ^\[main.assertion.5\] line 19 x.a==0: UNKNOWN$ | ||
| ^\[main.assertion.6\] line 20 x.a==1: UNKNOWN$ | ||
| ^\[main.assertion.7\] line 21 x.b==0: UNKNOWN$ | ||
| ^\[main.assertion.8\] line 22 x.b==1: UNKNOWN$ |
There was a problem hiding this comment.
With a "most recently written" abstraction for unions it should be possible to turn about half of these into successes but for now all unknown is the best that can be done.
| namespacet &ns | ||
| ); | ||
|
|
||
| SCENARIO( |
There was a problem hiding this comment.
Unit tests are good. In theory much of VSD should be testable via unit tests so having more is a good thing.
| return array_abstract_object->read(*this, index_expr, ns); | ||
| } | ||
| else if(simplified_id == ID_array) | ||
| else if( |
There was a problem hiding this comment.
Yes; these are all basically the same constant case.
|
Reflecting on this, I think the only uses of |
|
Better -- thank you. |
jezhiggins
force-pushed
the
abstract_environmentt-eval
branch
from
7c136ef to
c16842d
Compare
union_abstract_object is only top or bottom, consequently this test tells us very little beyond telling us union member access works doesn't explode. However there is nowhere else in the tests that doing anything at all with unions, so it is a least a little backstop.
Move it out of abstract_environment. union_abstract_objects can also be the target of member expressions, but this is not implemented in the current code so I've left it out of here too.
Move it out of abstract_environment.
Now we've moved some work into expression_transform, we don't need a read member on the base class.
jezhiggins
force-pushed
the
abstract_environmentt-eval
branch
from
c16842d to
97b6d87
Compare
Codecov Report
@@ Coverage Diff @@
## develop #5644 +/- ##
===========================================
+ Coverage 69.41% 69.44% +0.02%
===========================================
Files 1243 1243
Lines 100609 100584 -25
===========================================
+ Hits 69839 69846 +7
+ Misses 30770 30738 -32
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
jezhiggins
requested review from
chrisr-diffblue,
peterschrammel and
smowton
as code owners
| @@ -0,0 +1,15 @@ | |||
| CORE | |||
| union.c | |||
| --variable-sensitivity --vsd --verify | |||
There was a problem hiding this comment.
Please can you go down to just one of these two?
Refactoring work centred on abstract_environmentt::eval, trying to reduce the volume of special case handling.
Moved implementation of indexing, member access, and pointer dereferencing out into the target object types. This allowed us to combine several of the if-ladder cases together.