Skip to content

Unit test expr_skeleton and move it to its own file #4843

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
romainbrenguier merged 2 commits into from
Jul 2, 2019
Merged

Unit test expr_skeleton and move it to its own file #4843

romainbrenguier merged 2 commits into from
Jul 2, 2019

Conversation

@romainbrenguier
Copy link
Contributor

@romainbrenguier romainbrenguier commented Jun 26, 2019 •
edited
Loading

Move the class to its own files and unit test it.

  • Each commit message has a non-empty body, explaining why the change was made.
  • [na] Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • [na] 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).
  • [na] My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • [na] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@romainbrenguier romainbrenguier mentioned this pull request Jun 27, 2019
Merged
4 tasks
@romainbrenguier romainbrenguier force-pushed the unit-test/expr-skeleton branch from 8694d73 to 28a7b27 Compare June 27, 2019 07:22
@romainbrenguier romainbrenguier changed the title Unit test expr_skeleton Unit test expr_skeleton and move it to its own file Jun 27, 2019
@romainbrenguier romainbrenguier force-pushed the unit-test/expr-skeleton branch 3 times, most recently from 94c97af to 9c31050 Compare June 27, 2019 09:12
allredj
allredj reviewed Jun 27, 2019
View reviewed changes
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: 9c31050).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/117126740
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.

@romainbrenguier
Copy link
Contributor Author

romainbrenguier commented Jul 1, 2019

@smowton I've updated the method names

majakusber
majakusber approved these changes Jul 1, 2019
View reviewed changes
unit/goto-symex/expr_skeleton.cpp
SCENARIO("expr skeleton", "[core][goto-symex][symex-assign][expr-skeleton]")
{
const symbol_exprt foo{"foo", typet{}};
GIVEN("Skeletons `☐`, `☐[index]` and `☐.field1`")
Copy link

@majakusber majakusber Jul 1, 2019

Choose a reason for hiding this comment

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

⛏️ Why use the symbol here? Seems strange..

Copy link
Contributor Author

@romainbrenguier romainbrenguier Jul 1, 2019

Choose a reason for hiding this comment

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

Do you mean ☐? It is used in the same way as in the documentation https://github.com/diffblue/cbmc/pull/4843/files#diff-003f21a13603cd3a681d0d0f440e114bR20

@romainbrenguier
Move expr_skeleton class to its own file
51598f8 
Makes it easier to navigate through the code.
@romainbrenguier
Add a unit test for expr skeleton
948e9f4 
Tests the behavior of apply and compose.
@romainbrenguier romainbrenguier force-pushed the unit-test/expr-skeleton branch from 9c31050 to 948e9f4 Compare July 2, 2019 08:38
allredj
allredj reviewed Jul 2, 2019
View reviewed changes
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: 948e9f4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/117637722

@romainbrenguier romainbrenguier merged commit abf7a6d into diffblue:develop Jul 2, 2019
@romainbrenguier romainbrenguier deleted the unit-test/expr-skeleton branch July 2, 2019 10:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@tautschnig tautschnig Awaiting requested review from tautschnig tautschnig is a code owner

3 more reviewers

@allredj allredj allredj left review comments

@smowton smowton smowton approved these changes

@majakusber majakusber majakusber approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@smowton smowton

@peterschrammel peterschrammel

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@romainbrenguier @smowton @majakusber @allredj @peterschrammel