Skip to content

Extract call_stackt class from goto_symex_statet [depends-on: #4294] #4302

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 6 commits into from
Mar 4, 2019
Merged

Extract call_stackt class from goto_symex_statet [depends-on: #4294] #4302

merged 6 commits into from
Mar 4, 2019

Conversation

romainbrenguier
Copy link
Contributor

No functional changes.

This is based on #4294

Extract a call_stackt class from goto_symex_statet to declutter the
class definition.
This makes some calls a bit more verbose, but can be clearer.
For instance, it is not obvious what top() represent in the context of
goto_symex_state, whereas call_stack().top() is more explicit.

  • 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 force-pushed the refactor/symex_call_stack2 branch from a3d0090 to 89dfb92 Compare February 28, 2019 14:46
@tautschnig
Copy link
Collaborator

The change to jbmc/lib/java-models-library seems surprising.

@tautschnig tautschnig changed the title Extract call_stackt class from goto_symex_statet Extract call_stackt class from goto_symex_statet [depends-on: #4294] Feb 28, 2019
@romainbrenguier romainbrenguier force-pushed the refactor/symex_call_stack2 branch from 89dfb92 to 668f7f9 Compare February 28, 2019 14:55
@romainbrenguier
Copy link
Contributor Author

The change to jbmc/lib/java-models-library seems surprising.

sorry staged by mistake

NlightNFotis
NlightNFotis reviewed Feb 28, 2019
View reviewed changes
Copy link
Contributor

@NlightNFotis NlightNFotis left a comment

Choose a reason for hiding this comment

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

Minor comments.

src/goto-symex/frame.h
symex_targett::sourcet calling_location;

goto_programt::const_targett end_of_function;
exprt return_value = nil_exprt();
Copy link
Contributor

Choose a reason for hiding this comment

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

Please do not initialise members outside of constructors, unless they are static const

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Why not? This avoids having to repeat the same code for each constructor (and can avoid having to define a constructor in some cases).

Copy link
Contributor

Choose a reason for hiding this comment

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

Because it violates the Single Responsibility Principle. Unless you have a very good (architectural) reason, it's only the constructor's job to construct and initialise an object. Makes the code much more predictable as well. But that's my opinion.

@romainbrenguier romainbrenguier force-pushed the refactor/symex_call_stack2 branch 2 times, most recently from 88e4833 to 9f29a30 Compare March 1, 2019 08:58
smowton
smowton approved these changes Mar 1, 2019
View reviewed changes
Copy link
Contributor

@smowton smowton left a comment

Choose a reason for hiding this comment

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

Seems sensible

@romainbrenguier
Move goto_statet definition to its own file
7f8903e 
Having one class per header file makes it easier to navigate the code
and find what we want.
@romainbrenguier
Move framet class to its own file
3bce5c2 
Having one class per file makes it easier to navigate the code and find
what you want.
@romainbrenguier
New class for call_stack
3ea80c0 
Extract a call_stackt class from goto_symex_statet to declutter the
class definition.
This makes some calls a bit more verbose, but can be clearer.
For instance, it is not obvious what `top()` represent in the context of
goto_symex_state, whereas `call_stack().top()` is more explicit.
@romainbrenguier
Remove unused typedef
b620c57
@romainbrenguier
Apply clang-format suggestions
1ab1fff 
No functional change
@romainbrenguier
Add precondition on call_stackt::pop
52eb5c7 
Guarantee that it is never called on an empty stack.
@romainbrenguier romainbrenguier force-pushed the refactor/symex_call_stack2 branch from 9f29a30 to 52eb5c7 Compare March 4, 2019 08:21
allredj
allredj reviewed Mar 4, 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: 52eb5c7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103006835
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

tautschnig added a commit that referenced this pull request Mar 4, 2019
@tautschnig
Merge pull request #4294 from romainbrenguier/refactor/goto_state
17e53d6 
Move goto_statet and framet to their own files [blocks: #4302]
@tautschnig tautschnig merged commit fc4b5cc into diffblue:develop Mar 4, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@NlightNFotis NlightNFotis NlightNFotis left review comments

@allredj allredj allredj left review comments

@smowton smowton smowton approved these changes

@cesaro cesaro Awaiting requested review from cesaro

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@cristina-david cristina-david Awaiting requested review from cristina-david

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

@NathanJPhillips NathanJPhillips Awaiting requested review from NathanJPhillips

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

@pkesseli pkesseli Awaiting requested review from pkesseli

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

@thk123 thk123 Awaiting requested review from thk123

Assignees
No one assigned
Labels
dependent - do not merge Symbolic Execution
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@romainbrenguier @tautschnig @smowton @NlightNFotis @allredj