Introduce code_frontend_returnt #6403
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
The codet class is currently shared between the front-end code classes and the classes that represent goto-instructions. This commit moves this class into a separate header file so it can be consumed by both without including everything else.
After introducing code_frontend_declt, code_declt is now used exclusively by goto instructions, and thus belongs into goto_instruction_code.h.
kroening
force-pushed
the
code_frontend_returnt
branch
from
b5b6a7c to
d66b7c5
Compare
This splits the classes that represent return statements in the frontends and the return instructions in goto instructions. They differ in semantics and in the invariants that they maintain. The goto instruction variant always has a return value. The constructors for creating that class without return value are removed.
kroening
force-pushed
the
code_frontend_returnt
branch
from
d66b7c5 to
47a3277
Compare
kroening
requested review from
chrisr-diffblue,
feliperodri,
martin-cs,
peterschrammel,
romainbrenguier,
SaswatPadhi and
tautschnig
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #6403 +/- ##
===========================================
+ Coverage 75.97% 75.98% +0.01%
===========================================
Files 1523 1524 +1
Lines 164201 164294 +93
===========================================
+ Hits 124758 124847 +89
- Misses 39443 39447 +4
Continue to review full report at Codecov.
|
kroening
force-pushed
the
code_frontend_returnt
branch
from
3856af3 to
47a3277
Compare
tautschnig
approved these changes
Oct 21, 2021
martin-cs
approved these changes
Oct 21, 2021
peterschrammel
approved these changes
Oct 21, 2021
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
-n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.