Skip to content

Conversation

@tautschnig
Copy link
Collaborator

add_axioms_for_char_at, add_axioms_for_is_empty, add_axioms_from_char only
initialized one of the three vectors.

@romainbrenguier I am not entirely sure the modified initialisation code actually initialises the intended members.

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

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

symbol_exprt char_sym = fresh_symbol("char", str.type().subtype());
const exprt constraint = equal_exprt(char_sym, str[f.arguments()[1]]);
return {char_sym, {{constraint}}};
return {char_sym, {{constraint}, {}, {}}};
Copy link
Contributor

Choose a reason for hiding this comment

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

This seems ok, but maybe a clearer solution would be to declare the string_constrainst explicitely:

string_constraintst constraints;
constraints.existential = equal_exprt(char_sym, str[f.arguments()[1]]);
return {char_sym, constraints};

to replace the last two lines.

Copy link
Contributor

@romainbrenguier romainbrenguier left a comment

Choose a reason for hiding this comment

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

This is ok, I just put a suggestion to make the code clearer.

add_axioms_for_char_at, add_axioms_for_is_empty, add_axioms_from_char only
initialized one of the three vectors.
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: c078a69).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95249315

@tautschnig tautschnig merged commit 33561aa into diffblue:develop Dec 19, 2018
@tautschnig tautschnig deleted the vs-member-init branch December 19, 2018 12:42
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.

3 participants