Skip to content

Conversation

kroening
Copy link
Collaborator

@kroening kroening commented Sep 2, 2019

This improves type safety, and will enable restricing the exprt interface.

This is the final one in ansi-c/.

  • 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).
  • n/a 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.

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: 291a871).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/125451568
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

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: 8688613).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/125461334

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: 387fd14).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/131386071

Comment on lines 1142 to 1144
to_code(to_unary_expr(src).op()).get_statement() != ID_block)
return convert_norep(src, precedence);
Copy link
Collaborator

Choose a reason for hiding this comment

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

May I ask for braces to be added?

Comment on lines 1585 to 1589
to_unary_expr(src).op().id() == ID_predicate_passive_symbol)
dest = to_unary_expr(src).op().get_string(ID_identifier);
Copy link
Collaborator

Choose a reason for hiding this comment

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

Braces, please.

@@ -2082,7 +2082,7 @@ std::string expr2ct::convert_union(
if(src.operands().size()!=1)
return convert_norep(src, precedence);

std::string tmp=convert(src.op0());
std::string tmp = convert(to_union_expr(src).op());
Copy link
Collaborator

Choose a reason for hiding this comment

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

Hmm, could we actually get rid of tmp here and just inline the convert call below, where tmp is currently used? (It would be nice if over time we could get rid of any uses of the non-descriptive name tmp.)

@@ -2934,7 +2934,7 @@ std::string expr2ct::convert_code_assign(
const code_assignt &src,
unsigned indent)
{
std::string tmp=convert_binary(src, "=", 2, true);
std::string tmp = convert_binary(to_binary_expr(src), "=", 2, true);
Copy link
Collaborator

Choose a reason for hiding this comment

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

As above: can tmp please be removed and the call be inlined instead?

Comment on lines 3545 to 3547
{
return convert(to_index_expr(object).array());
}
Copy link
Collaborator

Choose a reason for hiding this comment

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

Braces don't seem to be necessary here (I'm only objecting to their use, because the other cases of this if don't use braces either.

@tautschnig tautschnig assigned kroening and unassigned tautschnig Oct 18, 2019
This improves type safety, and will enable restricing the exprt interface.

These are the final ones in ansi-c/.
@kroening
Copy link
Collaborator Author

@tautschnig All done.

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: 3c117db).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/132746298

@kroening kroening merged commit 9f021d1 into develop Oct 21, 2019
@kroening kroening deleted the opX-ansi-c branch October 21, 2019 14:29
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.

3 participants