Skip to content

Conversation

@tautschnig
Copy link
Collaborator

Please review commit by commit - each of them solves a variable shadowing problem in some subset of classes/files.

  • 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.

id2string(vt_symb_type.name) + "@"+ id2string(symbol.name);
vt_symb_var.base_name=
id2string(vt_symb_type.base_name) + "@" + id2string(symbol.base_name);
vt_symb_var.mode=ID_cpp;
Copy link
Contributor

Choose a reason for hiding this comment

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

Unrelated change?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Hmm, yes, I'll remove it.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Hmm, looking at my commit message that's actually explained:

Do not shadow "mode" in cpp front-end

Also pick up a previously set mode from a symbol rather than hard-coding ID_cpp
where possible. The symbol's mode could be ID_C or ID_cpp, depending on the
linkage specification.

Copy link
Contributor

Choose a reason for hiding this comment

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

I'm a little uncomfortable with either the commit message, or the commit - the headline of the message 'Do not shadow "mode" in cpp front-end' sounds like a simple refactoring, yet the commit also has a functional change in there too (which admittedly is mentioned in the body of the message) - i.e. the handling of previously set modes. Might it be better to either split that change out in to a separate commit, or change the wording of this commit so that the headline is more along the lines of 'Improve handling of "mode" in cpp frontend' ?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I have taken the route of amending the commit message as suggested.

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: cceb8f4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95450432

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: a94836e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95509779

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: e32dc1a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95526623

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: 2208e45).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95541818

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

🚫
This PR failed Diffblue compatibility checks (cbmc commit: d077960).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95543217
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

  • the cbmc commit has disappeared in the mean time (e.g. in a force-push)
  • the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

@tautschnig tautschnig changed the title Avoid shadowing of variables [blocks: #2310] Avoid shadowing of variables [depends-on: #3685, blocks: #2310] Jan 5, 2019
tautschnig added a commit that referenced this pull request Jan 7, 2019
Avoid shadowing in directory jbmc/unit [blocks: #3607]
@tautschnig tautschnig changed the title Avoid shadowing of variables [depends-on: #3685, blocks: #2310] Avoid shadowing of variables [blocks: #2310] Jan 7, 2019
@tautschnig tautschnig force-pushed the vs-shadow branch 2 times, most recently from 44d29c8 to 2da216c Compare January 7, 2019 16:04
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: 2da216c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96499375

{
dependencies.clean_cache();
const decision_proceduret::resultt res=supert::dec_solve();
res = supert::dec_solve();
Copy link
Contributor

Choose a reason for hiding this comment

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

I'm not a big fan of this change - makes it hard to see that this is constant throughout the loop and not dependent on it's outside loop state. A nice fix would of course be to introduce some functions or something, but perhaps an easier immediate fix for the shadowing would be call this loop_res and the other one initial_res

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Renaming done as suggested (using initial_result, refined_result).

{
PRECONDITION(f.arguments().size() == 1);
string_constraintst constraints;
string_constraintst hash_constraints;
Copy link
Contributor

Choose a reason for hiding this comment

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

⛏️ I'd probably rename the member variable to global_constraints or all_constraints

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Please forgive me for not intending to act on this one: from reading the code I got the impression that the two cases touched here affect methods that should likely be deprecated or removed. @romainbrenguier Any insights maybe?

Copy link
Contributor

Choose a reason for hiding this comment

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

No problem - all of these comments are optional, I'm not overly familiar with the code being modified here anyway.

Copy link
Contributor

Choose a reason for hiding this comment

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

Yes hash code and intern should be implemented via models rather than internally in the solver (they are very language dependent), so this should disappear.

conversion_factor_table.copy_to_operands(constant_float(f, float_spec));
for(const auto &f : two_power_e_over_ten_power_d_table)
conversion_factor_table.copy_to_operands(constant_float(f, float_spec));
for(const auto &neg : two_power_e_over_ten_power_d_table_negatives)
Copy link
Contributor

Choose a reason for hiding this comment

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

⛏️ Don't use abbreviations negative, position - though obviously a massive improvement on what was there before.
⛏️ Rename the param f to float_expr?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Done, and a separate commit doing the renaming of f is being prepared.

There is a class member of the same name, use "symbols_in_constraint" instead.
There is a class member named "result", rename the local variable to
"eval_result."
Rename both instances, the first to "initial_result" and the second to
"refined_result."
Rename the first use to "initial_instances"
There is no need to pass a class member as an argument.
Rename the method-local ones "intern_constraints" and "hash_constraints."
Rename container elements to "positive" and "negative."
A single-character name is not very descriptive, longer symbol names bear no
runtime overhead.
@tautschnig tautschnig force-pushed the vs-shadow branch 2 times, most recently from 6e271c3 to adde39e Compare January 8, 2019 12:18
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 6e271c3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96602029
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

  • the cbmc commit has disappeared in the mean time (e.g. in a force-push)
  • the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: adde39e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96604752

@tautschnig tautschnig merged commit b0f2506 into diffblue:develop Jan 9, 2019
@tautschnig tautschnig deleted the vs-shadow branch January 9, 2019 11:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

10 participants