Skip to content

Goto symex state clean-up #3445

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
merged 18 commits into from
Nov 26, 2018
Merged

Goto symex state clean-up #3445

merged 18 commits into from
Nov 26, 2018

Conversation

romainbrenguier
Copy link
Contributor

No functional changes.

  • Each commit message has a non-empty body, explaining why the change was made.
  • 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/
  • [na] 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.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj
allredj reviewed Nov 19, 2018
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: 9db048d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91899118

majakusber
majakusber reviewed Nov 20, 2018
View reviewed changes
Copy link

@majakusber majakusber left a comment

Choose a reason for hiding this comment

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

All useful stuff! I have only one question regarding the use of struct versus class.

src/goto-symex/goto_symex_state.h
@@ -267,9 +267,8 @@ class goto_symex_statet final

// stack frames -- these are used for function calls and
// for exceptions
class framet
struct framet
Copy link

Choose a reason for hiding this comment

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

I didn't know that was the convention. I only found this in the CBMC coding standard:
Prefer use of class instead of struct.
But that seems to be out of date.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

In general people use class when there are virtual functions, but I don't think it's explicitly a CBMC convention.

Copy link
Contributor

Choose a reason for hiding this comment

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

The C++ Core Guidelines has two guidelines which relate to this:

  • C.2: Use class if the class has an invariant; use struct if the data members can vary independently
  • C.8: Use class rather than struct if any member is non-public

tautschnig
tautschnig approved these changes Nov 24, 2018
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

Needs a rebase, otherwise good to go.

@romainbrenguier
Remove typedef used only once
d1be84d
@romainbrenguier
Use ranged for instead of iterators
1410f06
@romainbrenguier
Remove typedef used only once
6527421
@romainbrenguier
Remove typedef used only once
aff8880
@romainbrenguier
Make framet a struct
607ed1c 
As convention we generaly use `class` in presence of virtual functions,
which is not the case here.
@romainbrenguier
Make threadt a struct
5344bee 
No function change.
As a convention we use class in presence of virtual function, which is
not the case here, so struct is prefered.
@romainbrenguier
Remove trivial constructor
0b7ff55 
No functional change
@romainbrenguier
Remove typedef used only once
a30d8a7
@romainbrenguier
Remove unimplemented declaration
41508c9
@romainbrenguier
Remove field that is assigned but never read
6896b16
@romainbrenguier
Replace constructor by default values for fields
4443c61
@romainbrenguier
Replace constructor by default values for fields
c61a00d
@romainbrenguier
Use ranged-for instead of iterators
c1eda5e
@romainbrenguier
Remove typedef used only once
9153342
@romainbrenguier
Use auto for iterator type
512c30b
@romainbrenguier
Use ranged-for instead of iterators
f4b1533
allredj
allredj reviewed Nov 26, 2018
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: 27b4b03).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92507822

@romainbrenguier romainbrenguier merged commit 8a75ce4 into diffblue:develop Nov 26, 2018
@romainbrenguier romainbrenguier deleted the refactor/symex-part4 branch November 26, 2018 09:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj approved these changes

@owen-mc-diffblue owen-mc-diffblue owen-mc-diffblue left review comments

@tautschnig tautschnig tautschnig approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

@majakusber majakusber majakusber approved these changes

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

Assignees

@romainbrenguier romainbrenguier

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@romainbrenguier @tautschnig @peterschrammel @majakusber @allredj @owen-mc-diffblue