Skip to content

introduce API for goto_instructiont::source_location #6400

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
kroening merged 1 commit into from
Oct 20, 2021
Merged

introduce API for goto_instructiont::source_location #6400

kroening merged 1 commit into from
Oct 20, 2021

Conversation

@kroening
Copy link
Collaborator

@kroening kroening commented Oct 19, 2021

This introduces two methods for wrapping the accesses to
goto_instructiont::source_location. The field is now protected to prevent
direct access.

  • 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 kroening force-pushed the goto_instruction_location_API branch 2 times, most recently from 216855b to f61a64d Compare October 19, 2021 10:24
@kroening kroening marked this pull request as ready for review October 19, 2021 11:18
@codecov
Copy link

codecov bot commented Oct 19, 2021 •
edited
Loading

Codecov Report

Merging #6400 (216855b) into develop (a55f5ae) will increase coverage by 0.00%.
The diff coverage is 69.86%.

❗ Current head 216855b differs from pull request most recent head 8e14af7. Consider uploading reports for the commit 8e14af7 to get more accurate results
Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #6400   +/-   ##
========================================
  Coverage    75.97%   75.98%           
========================================
  Files         1523     1523           
  Lines       164201   164227   +26     
========================================
+ Hits        124758   124780   +22     
- Misses       39443    39447    +4
Impacted Files Coverage Δ
src/analyses/custom_bitvector_analysis.cpp 54.77% <0.00%> (ø)
src/analyses/dependence_graph.cpp 89.26% <0.00%> (ø)
src/analyses/interval_analysis.cpp 0.00% <0.00%> (ø)
src/analyses/local_bitvector_analysis.cpp 74.70% <0.00%> (ø)
src/analyses/local_may_alias.cpp 62.96% <0.00%> (ø)
src/analyses/static_analysis.cpp 46.73% <0.00%> (ø)
...sitivity/variable_sensitivity_dependence_graph.cpp 84.40% <0.00%> (ø)
src/goto-cc/linker_script_merge.cpp 0.00% <0.00%> (ø)
src/goto-diff/change_impact.cpp 0.00% <0.00%> (ø)
src/goto-diff/goto_diff_base.cpp 81.25% <0.00%> (ø)
... and 115 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 293748d...8e14af7. Read the comment docs.

peterschrammel
peterschrammel approved these changes Oct 19, 2021
View reviewed changes
src/goto-programs/goto_program.h
return _source_location;
}

source_locationt &source_location_nonconst()
Copy link
Member

@peterschrammel peterschrammel Oct 19, 2021

Choose a reason for hiding this comment

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

Is the idea to use a _nonconst suffix now consistently for this purpose?

Copy link
Collaborator Author

@kroening kroening Oct 19, 2021

Choose a reason for hiding this comment

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

Yes. I don't love it, but the alternative would be to add as_const everywhere else.
The goal would be to avoid any usage of _nonconst, whenever feasible, and use the constructors instead.

martin-cs
martin-cs approved these changes Oct 19, 2021
View reviewed changes
Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

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

The bits I am maintainer for look fine.

@kroening kroening changed the title intruduce API for goto_instructiont::source_location introduce API for goto_instructiont::source_location Oct 20, 2021
tautschnig
tautschnig approved these changes Oct 20, 2021
View reviewed changes
src/goto-programs/instrument_preconditions.cpp
Comment on lines 40 to 44
if(
i_it->is_assert() &&
i_it->source_location().get_property_class() == ID_precondition)
result.push_back(i_it);
Copy link
Collaborator

@tautschnig tautschnig Oct 20, 2021

Choose a reason for hiding this comment

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

Nit picking: add braces for the body.

src/goto-programs/instrument_preconditions.cpp
Comment on lines 59 to 65
if(
instruction.is_assert() &&
instruction.source_location().get_property_class() == ID_precondition)
instruction.type=LOCATION;
Copy link
Collaborator

@tautschnig tautschnig Oct 20, 2021

Choose a reason for hiding this comment

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

Nit picking: add braces for the body.

@kroening kroening force-pushed the goto_instruction_location_API branch from f61a64d to 11c711f Compare October 20, 2021 10:38
@kroening
introduce API for goto_instructiont::source_location
8e14af7 
This introduces two methods for wrapping the accesses to
goto_instructiont::source_location.  The field is now protected to prevent
direct access.
@kroening kroening force-pushed the goto_instruction_location_API branch from 11c711f to 8e14af7 Compare October 20, 2021 10:45
@kroening kroening merged commit 268a0d0 into develop Oct 20, 2021
@kroening kroening deleted the goto_instruction_location_API branch October 20, 2021 12:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tautschnig tautschnig tautschnig approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

@feliperodri feliperodri feliperodri approved these changes

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

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

@romainbrenguier romainbrenguier Awaiting requested review from romainbrenguier

@SaswatPadhi SaswatPadhi Awaiting requested review from SaswatPadhi

Assignees

@kroening kroening

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@kroening @tautschnig @peterschrammel @feliperodri @martin-cs