Skip to content

Remove cmdlinet from init/lazy_goto_model #3518

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 2 commits into from
Dec 3, 2018
Merged

Remove cmdlinet from init/lazy_goto_model #3518

merged 2 commits into from
Dec 3, 2018

Conversation

peterschrammel
Copy link
Member

It should be possible to build a goto model without requiring a cmdlinet, e.g. in unit tests.

Caution! This breaks most driver programs.

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

@peterschrammel peterschrammel force-pushed the no-cmdline-in-goto-model branch 3 times, most recently from 779832d to e2d75fa Compare December 3, 2018 00:54
allredj
allredj reviewed Dec 3, 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.

🚫
This PR failed Diffblue compatibility checks (cbmc commit: e2d75fa).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93300370
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

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 incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

tautschnig
tautschnig approved these changes Dec 3, 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.

A nice step forward! I am assuming TG just needs a genuine update due to the API change.

jbmc/src/jbmc/jbmc_parse_options.cpp Outdated
@@ -106,8 +106,11 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
usage_error();
exit(1); // should contemplate EX_USAGE from sysexits.h
}

Copy link
Collaborator

Choose a reason for hiding this comment

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

Nit pick: unrelated change?

jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp Outdated
optionst options;
parse_java_language_options(command_line, options);
options.set_option("java-cp-include-files", "CustomVSATest.class");
std::vector<std::string> files = {"pointer-analysis/CustomVSATest.jar"};
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nit pick: it may make things easier to read if just passing this directly to initialize_goto_model instead of adding this files local variable. Just less context for the reader to remember.

src/langapi/language_ui.cpp
@@ -112,8 +113,12 @@ bool language_uit::final()
{
language_files.set_message_handler(*message_handler);

// TODO: This should be moved elsewhere because it is not used in
// this repository.
Copy link
Collaborator

Choose a reason for hiding this comment

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

Maybe create an issue for this?

Copy link
Member Author

Choose a reason for hiding this comment

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

#3519

@peterschrammel
Copy link
Member Author

I am assuming TG just needs a genuine update due to the API change.

Already got one that is passing.

@peterschrammel
Remove cmdlinet from init/lazy_goto_model
cd90c7d 
It should be possible to build a goto model
without requiring a cmdlinet, e.g. in unit tests.
@peterschrammel
Reformat #if-#endif
7183e66 
to make clang-format happy
@peterschrammel peterschrammel force-pushed the no-cmdline-in-goto-model branch from e2d75fa to 7183e66 Compare December 3, 2018 09:23
allredj
allredj reviewed Dec 3, 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.

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 7183e66).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93331192
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

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 incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

@peterschrammel peterschrammel mentioned this pull request Dec 3, 2018
Merged
7 tasks
chrisr-diffblue
chrisr-diffblue approved these changes Dec 3, 2018
View reviewed changes
Copy link
Contributor

@chrisr-diffblue chrisr-diffblue left a comment

Choose a reason for hiding this comment

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

Looks like a nice cleanup.

src/langapi/language_ui.cpp
bool stubs_enabled=_cmdline.isset("generate-opaque-stubs");
bool stubs_enabled = false;
if(options != nullptr)
stubs_enabled = options->is_set("generate-opaque-stubs");
Copy link
Contributor

Choose a reason for hiding this comment

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

Is this any easier to read if written as bool stubs_enabled = options != nullptr ? options->is_set(..) : false; ?

Copy link
Member Author

Choose a reason for hiding this comment

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

Will be removed in #3520 anyway.

@peterschrammel peterschrammel merged commit b4cd9cc into diffblue:develop Dec 3, 2018
@peterschrammel peterschrammel deleted the no-cmdline-in-goto-model branch December 3, 2018 14:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@smowton smowton smowton approved these changes

@tautschnig tautschnig tautschnig approved these changes

@chrisr-diffblue chrisr-diffblue chrisr-diffblue approved these changes

@cesaro cesaro Awaiting requested review from cesaro

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

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

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@pkesseli pkesseli Awaiting requested review from pkesseli

Assignees

@peterschrammel peterschrammel

@chrisr-diffblue chrisr-diffblue

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@peterschrammel @smowton @tautschnig @allredj @chrisr-diffblue