Skip to content

introduce instructiont::decl_symbol() #5861

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

Merged
merged 1 commit into from
Feb 25, 2021
Merged

Conversation

kroening
Copy link
Member

This addresses the issue of the ambiguous dual-use of code_declt in both the
C front-end and the goto-program API by replacing the use of code_declt by
directly returning the symbol_exprt. 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.

kroening added a commit that referenced this pull request Feb 24, 2021
This mirrors the change in #5861 by replacing the use of code_deadt by
directly returning the symbol_exprt.  The client code is simplified.
kroening added a commit that referenced this pull request Feb 24, 2021
This mirrors the change in #5861 by replacing the use of code_deadt by
directly returning the symbol_exprt.  The client code is simplified.
kroening added a commit that referenced this pull request Feb 24, 2021
This mirrors the change in #5861 by replacing the use of code_deadt by
directly returning the symbol_exprt.  The client code is simplified.
@kroening kroening force-pushed the goto_instruction_decl branch from d301d0b to 776362e Compare February 24, 2021 13:10
kroening added a commit that referenced this pull request Feb 24, 2021
This mirrors the change in #5861 by replacing the use of code_returnt by
directly returning the return value expression.  The client code is
simplified considerably.
kroening added a commit that referenced this pull request Feb 24, 2021
This mirrors the change in #5861 by replacing the use of code_returnt by
directly returning the return value expression.  The client code is
simplified considerably.
@kroening kroening force-pushed the goto_instruction_decl branch from 776362e to 60892e0 Compare February 24, 2021 13:43
kroening added a commit that referenced this pull request Feb 24, 2021
This mirrors the change in #5861 by replacing the use of code_returnt by
directly returning the return value expression.  The client code is
simplified considerably.
kroening added a commit that referenced this pull request Feb 24, 2021
This mirrors the change in #5861 by replacing the use of code_returnt by
directly returning the return value expression.  The client code is
simplified considerably.
@kroening kroening force-pushed the goto_instruction_decl branch from 60892e0 to 4fd73c1 Compare February 24, 2021 14:08
@codecov
Copy link

codecov bot commented Feb 24, 2021

Codecov Report

Merging #5861 (4fd73c1) into develop (4daa686) will increase coverage by 0.00%.
The diff coverage is 92.66%.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #5861   +/-   ##
========================================
  Coverage    72.89%   72.89%           
========================================
  Files         1423     1423           
  Lines       154229   154242   +13     
========================================
+ Hits        112426   112440   +14     
+ Misses       41803    41802    -1     
Impacted Files Coverage Δ
src/analyses/global_may_alias.cpp 0.00% <0.00%> (ø)
src/analyses/goto_check.cpp 88.28% <ø> (ø)
src/analyses/uninitialized_domain.cpp 0.00% <0.00%> (ø)
.../goto-instrument/goto_instrument_parse_options.cpp 58.20% <ø> (ø)
...rc/goto-instrument/goto_instrument_parse_options.h 100.00% <ø> (ø)
src/goto-programs/goto_convert_class.h 87.30% <ø> (ø)
src/goto-diff/goto_diff_parse_options.cpp 58.67% <75.00%> (ø)
src/goto-programs/goto_program.h 89.40% <80.00%> (+0.03%) ⬆️
src/goto-analyzer/goto_analyzer_parse_options.cpp 73.25% <90.90%> (ø)
src/util/std_code.h 94.00% <90.90%> (ø)
... and 36 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 a4c81ef...c830360. Read the comment docs.

kroening added a commit that referenced this pull request Feb 24, 2021
This mirrors the change in #5861 by replacing the use of code_deadt by
directly returning the symbol_exprt.  The client code is simplified.
This addresses the issue of the ambiguous dual-use of code_declt in both the
C front-end and the goto-program API by replacing the use of code_declt by
directly returning the symbol_exprt.  The client code is simplified.
@kroening kroening force-pushed the goto_instruction_decl branch from 4fd73c1 to c830360 Compare February 24, 2021 14:21
kroening added a commit that referenced this pull request Feb 24, 2021
This mirrors the change in #5861 by replacing the use of code_returnt by
directly returning the return value expression.  The client code is
simplified considerably.
kroening added a commit that referenced this pull request Feb 24, 2021
This mirrors the change in #5861 by replacing the use of code_returnt by
directly returning the return value expression.  The client code is
simplified considerably.
@kroening kroening marked this pull request as ready for review February 24, 2021 16:45
kroening added a commit that referenced this pull request Feb 24, 2021
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.
kroening added a commit that referenced this pull request Feb 25, 2021
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 merged commit 818fdf2 into develop Feb 25, 2021
@tautschnig tautschnig deleted the goto_instruction_decl branch February 25, 2021 22:54
kroening added a commit that referenced this pull request Feb 26, 2021
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.
kroening added a commit that referenced this pull request Mar 15, 2021
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.
kroening added a commit that referenced this pull request Mar 15, 2021
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.
kroening added a commit that referenced this pull request Mar 15, 2021
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 pushed a commit that referenced this pull request May 13, 2021
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 pushed a commit that referenced this pull request May 13, 2021
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.
TGWDB pushed a commit to TGWDB/cbmc that referenced this pull request May 17, 2021
This mirrors the change in diffblue#5861 by replacing the use of code_assignt by
directly returning the lhs and rhs expressions.  The client code is
simplified.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants