Skip to content

introduce instructiont::assign_lhs() and assign_rhs() #5865

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 1 commit into from
May 14, 2021
Merged

introduce instructiont::assign_lhs() and assign_rhs() #5865

merged 1 commit into from
May 14, 2021

Conversation

kroening
Copy link
Member

This mirrors the change in #5861 by replacing the use of code_assignt by
directly returning the lhs and rhs expressions. The client code is
simplified.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@codecov
Copy link

codecov bot commented Feb 24, 2021 •
edited
Loading

Codecov Report

Merging #5865 (9ff5919) into develop (dd36155) will decrease coverage by 0.08%.
The diff coverage is 87.36%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #5865      +/-   ##
===========================================
- Coverage    75.33%   75.24%   -0.09%     
===========================================
  Files         1447     1447              
  Lines       157988   158053      +65     
===========================================
- Hits        119013   118926      -87     
- Misses       38975    39127     +152
Impacted Files Coverage Δ
src/ansi-c/c_typecheck_base.cpp 50.54% <0.00%> (-5.38%) ⬇️
src/ansi-c/c_typecheck_base.h 100.00% <ø> (+13.33%) ⬆️
src/goto-checker/symex_coverage.cpp 95.76% <ø> (ø)
src/goto-instrument/accelerate/accelerate.cpp 34.89% <0.00%> (ø)
src/goto-instrument/code_contracts.h 94.11% <ø> (ø)
src/goto-instrument/concurrency.cpp 0.00% <0.00%> (ø)
src/goto-instrument/nondet_volatile.cpp 86.55% <ø> (-0.15%) ⬇️
src/goto-instrument/replace_calls.cpp 89.55% <0.00%> (+1.31%) ⬆️
src/goto-programs/goto_inline_class.cpp 84.09% <ø> (-0.09%) ⬇️
src/goto-instrument/goto_program2code.cpp 69.20% <60.00%> (+0.06%) ⬆️
... and 71 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update e9b5f5c...9ff5919. Read the comment docs.

@kroening kroening force-pushed the goto_instruction_assign branch 2 times, most recently from 8121569 to e261c0d Compare February 26, 2021 10:46
@kroening kroening marked this pull request as ready for review February 26, 2021 10:50
@tautschnig
Copy link
Collaborator

@kroening This is failing some tests.

tautschnig
tautschnig reviewed Feb 26, 2021
View reviewed changes
src/goto-programs/goto_program.h Outdated
@@ -183,13 +183,43 @@ class goto_programt
codet code;

/// Get the assignment for ASSIGN
DEPRECATED(SINCE(2021, 2, 24, "Use dead_symbol instead"))
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copy&paste error?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed

src/goto-programs/goto_program.h Outdated
/// Set the assignment for ASSIGN
DEPRECATED(SINCE(2021, 2, 24, "Use dead_symbol instead"))
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copy&paste error?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed

@kroening kroening force-pushed the goto_instruction_assign branch 3 times, most recently from 2c0dec0 to 32a78bf Compare March 15, 2021 17:16
@tautschnig tautschnig force-pushed the goto_instruction_assign branch from 32a78bf to 946e12c Compare May 13, 2021 21:14
@tautschnig tautschnig assigned tautschnig and unassigned kroening May 13, 2021
@kroening @tautschnig
introduce instructiont::assign_lhs() and assign_rhs()
9ff5919 
This mirrors the change in #5861 by replacing the use of code_assignt by
directly returning the lhs and rhs expressions.  The client code is
simplified.
@tautschnig tautschnig force-pushed the goto_instruction_assign branch from 946e12c to 9ff5919 Compare May 13, 2021 21:45
@tautschnig tautschnig merged commit a719ea3 into develop May 14, 2021
@tautschnig tautschnig deleted the goto_instruction_assign branch May 14, 2021 09:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tautschnig tautschnig tautschnig left review comments

@peterschrammel peterschrammel peterschrammel approved these changes

@martin-cs martin-cs martin-cs approved these changes

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue Awaiting requested review from hannes-steffenhagen-diffblue

@romainbrenguier romainbrenguier Awaiting requested review from romainbrenguier

@smowton smowton Awaiting requested review from smowton

Assignees

@tautschnig tautschnig

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@kroening @tautschnig @peterschrammel @martin-cs