-
Notifications
You must be signed in to change notification settings - Fork 277
CONTRACTS: functions to compute root objects #7636
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
CONTRACTS: functions to compute root objects #7636
Conversation
Codecov ReportPatch and project coverage have no change.
Additional details and impacted files@@ Coverage Diff @@
## develop #7636 +/- ##
========================================
Coverage 78.51% 78.51%
========================================
Files 1674 1674
Lines 191935 191935
========================================
Hits 150704 150704
Misses 41231 41231 Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here. ☔ View full report in Codecov by Sentry. |
31e6deb
to
631ef11
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There are a bunch of recurring comments of mine here. For pointer-need-not-be-operand-0 you might want to make use of goto-programs/pointer_arithmetic.h
to avoid having to go over all the operands.
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.h
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.h
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.h
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.h
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.h
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.cpp
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.cpp
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.cpp
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.cpp
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.cpp
Outdated
Show resolved
Hide resolved
5822737
to
9186b70
Compare
4480e64
to
e937ead
Compare
e937ead
to
d11f7a2
Compare
#7629 also include these changes. |
d11f7a2
to
3cb8ee9
Compare
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.cpp
Outdated
Show resolved
Hide resolved
3cb8ee9
to
c43d650
Compare
@tautschnig @feliperodri latest version, should be good to go (still needs approval from @tautschnig to merge) |
c43d650
to
77512fe
Compare
@tautschnig if you have the time, could you do another round of review on this PR? |
77512fe
to
9a6fbff
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I believe this code can be simplified, see my comments.
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.h
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.h
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.h
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.cpp
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.h
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.cpp
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.cpp
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.cpp
Outdated
Show resolved
Hide resolved
src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.cpp
Outdated
Show resolved
Hide resolved
Alternative implementation of `root_object` supporting ternary operators in assignment or call LHS expressions, and object slice expressions in assigns clause targets.
9a6fbff
to
6b828d5
Compare
@tautschnig all suggestions implemented, could you please take a last look ? |
Extracted from #7541, will be tested when all new features are merged.