Skip to content

Remove language_uit as it is no longer used #3824

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.

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

Merged
merged 2 commits into from
Feb 4, 2019

Conversation

tautschnig
Copy link
Collaborator

Use initialize_goto_model to obtain goto programs, don't run parse() etc.
directly.

Only the last commit is new, the first four are #3683.

  • 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.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • n/a 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
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

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

Looks good.

@tautschnig tautschnig changed the title Remove language_uit as it is no longer used [depends-on: #3683] Remove language_uit as it is no longer used Jan 30, 2019
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: f23f519).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99082540
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
Copy link
Collaborator Author

@allredj @peterschrammel @thk123 I suspect this needs a genuine TG bump. I'm not sure whether the solution is as simple as removing an unnecessary include or actually needs the kind of (improvement work) that was done in #3683.

Copy link
Member

@peterschrammel peterschrammel left a comment

Choose a reason for hiding this comment

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

@thk123, seems the header is still included in TG, but not used.

@tautschnig tautschnig assigned majakusber and unassigned kroening Feb 4, 2019
@thomasspriggs
Copy link
Contributor

I am looking into the TG fix.

@thomasspriggs
Copy link
Contributor

@tautschnig Please re-base on latest CBMC develop branch. The joel-bot should then pass.

This isn't used, we use cbmc_parse_optionst here.
Use initialize_goto_model to obtain goto programs, don't run parse() etc.
directly.
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: ef193de).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99673225
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.

@thomasspriggs
Copy link
Contributor

The joel-bot failure looks unrelated to the changes in this PR. The error is error: ‘const class goto_programt::instructiont’ has no member named ‘function’.

@tautschnig tautschnig merged commit 69a3cc4 into diffblue:develop Feb 4, 2019
@tautschnig tautschnig deleted the remove-language_uit branch February 4, 2019 19:17
@tautschnig
Copy link
Collaborator Author

Thanks @thomasspriggs - I guess the update after #3126 isn't merged yet (or was not at the time of the bot running).

@thomasspriggs
Copy link
Contributor

thomasspriggs commented Feb 4, 2019

I have now merged the corresponding TG PR for #3126. So the joel bot should start passing again, on future runs.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

9 participants