Skip to content

Remove {f,F}orall_goto_functions #5615

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 1, 2021

Conversation

tautschnig
Copy link
Collaborator

@tautschnig tautschnig commented Nov 18, 2020

This was useful in the past, but with C++-11 we can use a ranged-for to
avoid the iterator altogether (in all but the cases in goto-diff, where
we now make the iterator explicit).

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a 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.

@tautschnig tautschnig self-assigned this Nov 18, 2020
@codecov
Copy link

codecov bot commented Nov 19, 2020

Codecov Report

Merging #5615 (e8e0193) into develop (261f598) will decrease coverage by 0.00%.
The diff coverage is 59.03%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #5615      +/-   ##
===========================================
- Coverage    69.71%   69.71%   -0.01%     
===========================================
  Files         1242     1242              
  Lines       100889   100889              
===========================================
- Hits         70338    70334       -4     
- Misses       30551    30555       +4     
Flag Coverage Δ
cproversmt2 43.39% <60.57%> (-0.01%) ⬇️
regression 66.67% <57.83%> (-0.01%) ⬇️
unit 32.29% <30.65%> (-0.01%) ⬇️

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files Coverage Δ
jbmc/src/janalyzer/janalyzer_parse_options.cpp 48.20% <0.00%> (ø)
src/analyses/custom_bitvector_analysis.cpp 55.26% <0.00%> (ø)
src/analyses/flow_insensitive_analysis.h 59.09% <ø> (ø)
src/analyses/interval_analysis.cpp 0.00% <0.00%> (ø)
src/goto-analyzer/goto_analyzer_parse_options.cpp 73.90% <0.00%> (ø)
src/goto-diff/change_impact.cpp 0.00% <0.00%> (ø)
src/goto-diff/unified_diff.cpp 0.00% <0.00%> (ø)
src/goto-instrument/accelerate/accelerate.cpp 0.00% <0.00%> (ø)
src/goto-instrument/branch.cpp 0.00% <0.00%> (ø)
src/goto-instrument/concurrency.cpp 0.00% <0.00%> (ø)
... and 66 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 261f598...e8e0193. Read the comment docs.

@hannes-steffenhagen-diffblue
Copy link
Contributor

Yes please. Though I think it’d probably be a bit too ambitious to do them all in one PR

@tautschnig tautschnig force-pushed the remove-forall-macros branch 2 times, most recently from 90bd35a to 4cb985c Compare January 26, 2021 21:38
@tautschnig tautschnig changed the title Remove forall_* macros Remove forall_* macros [depends-on: #5783, #5785, #5788, #5789, #5790] Jan 26, 2021
@tautschnig tautschnig force-pushed the remove-forall-macros branch from 4cb985c to 11d2947 Compare January 30, 2021 23:03
@tautschnig tautschnig changed the title Remove forall_* macros [depends-on: #5783, #5785, #5788, #5789, #5790] Remove forall_* macros Jan 30, 2021
@tautschnig tautschnig changed the title Remove forall_* macros Remove {f,F}orall_goto_functions Jan 30, 2021
@tautschnig tautschnig marked this pull request as ready for review January 30, 2021 23:05
@tautschnig tautschnig removed their assignment Jan 30, 2021
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.

Thanks for these patches; sorry I missed this one.

@@ -173,7 +173,7 @@ class flow_insensitive_analysis_baset
const goto_functionst &goto_functions);

bool fixedpoint(
goto_functionst::function_mapt::const_iterator it,
const goto_functionst::function_mapt::value_type &gf_entry,
Copy link
Collaborator

Choose a reason for hiding this comment

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

This feels like it might be better as a goto_programt?

}

bool flow_insensitive_analysis_baset::fixedpoint(
const goto_functionst::function_mapt::const_iterator it,
const goto_functionst::function_mapt::value_type &gf_entry,
Copy link
Collaborator

Choose a reason for hiding this comment

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

goto_programt ?

@@ -52,7 +52,7 @@ class goto_program_coverage_recordt : public coverage_recordt
public:
goto_program_coverage_recordt(
const namespacet &ns,
goto_functionst::function_mapt::const_iterator gf_it,
const goto_functionst::function_mapt::value_type &gf_entry,
Copy link
Collaborator

Choose a reason for hiding this comment

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

Feels a little cumbersome. Isn't this a goto_functiont?

Copy link
Collaborator Author

@tautschnig tautschnig Jan 31, 2021

Choose a reason for hiding this comment

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

These also require the name of the goto_functiont. What could be done is passing that information as two arguments? That would probably make for are clearer interface. Let me fix this.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Now done.

This was useful in the past, but with C++-11 we can use a ranged-for to
avoid the iterator altogether (in all but the cases in goto-diff, where
we now make the iterator explicit).
@tautschnig tautschnig force-pushed the remove-forall-macros branch from 11d2947 to e8e0193 Compare January 31, 2021 21:35
@tautschnig tautschnig self-assigned this Jan 31, 2021
@tautschnig tautschnig merged commit 5a41cb6 into diffblue:develop Feb 1, 2021
@tautschnig tautschnig deleted the remove-forall-macros branch February 1, 2021 07:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants