Java now uses struct_tag types #3102

kroening · 2018-10-05T18:44:29Z

Note that this does two things (switching base classes to struct_tags and switching the Java front-end to struct_tags). However, they can't be done separately.

Each commit message has a non-empty body, explaining why the change was made.
My contribution is formatted in line with CODING_STANDARD.md.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
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).
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

This PR failed Diffblue compatibility checks (cbmc commit: 64bfc03).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87092812
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).

tautschnig

Changes appear to be consistent.

owen-mc-diffblue · 2018-10-07T07:03:56Z

src/cpp/cpp_typecheck_bases.cpp


-    if(base_symbol_expr.type().id() != ID_symbol_type)
+    if(base_symbol_expr.type().id() != ID_struct_tag)
    {
      error().source_location=name.source_location();
      error() << "expected type symbol as struct/class base" << eom;


Does this error message need to be updated?

smowton · 2018-10-08T15:56:21Z

Reviewed the first 30% or so, seems ok so far but don't have time to read the whole thing

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 24aa5f9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87616503
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.

martin-cs

The four lines that are in my area seem OK.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: d846585).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87698036
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 · 2018-10-12T06:39:27Z

@thk123, @allredj, please create a TG bump for this.

allredj · 2018-10-12T09:24:24Z

will do

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 5f18b69).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87756938
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.

allredj

This breaks test-generator. We're working on a fix but so far we were not able to make test-gen live with that change.

allredj

⚠️
Diffblue compatibility check is currently unavailable.
Please create manual bump.
(cbmc commit: 39e5ab6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90749965

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 4b98156).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91761785
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.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 708a46d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92467085
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.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: ddcf2c8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93180215
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.

kroening added Java Front End C++ Front End cleanup labels Oct 5, 2018

kroening assigned smowton, tautschnig and peterschrammel Oct 5, 2018

kroening requested review from smowton, tautschnig and peterschrammel October 5, 2018 18:44

kroening requested review from cesaro, chrisr-diffblue, cristina-david, martin-cs, NathanJPhillips, pkesseli, romainbrenguier and thk123 as code owners October 5, 2018 18:44

allredj reviewed Oct 6, 2018

View reviewed changes

tautschnig approved these changes Oct 6, 2018

View reviewed changes

tautschnig removed their assignment Oct 6, 2018

owen-mc-diffblue reviewed Oct 7, 2018

View reviewed changes

tautschnig assigned kroening Oct 7, 2018

kroening force-pushed the java-struct-tag branch from 64bfc03 to 24aa5f9 Compare October 11, 2018 09:43

allredj reviewed Oct 11, 2018

View reviewed changes

martin-cs approved these changes Oct 11, 2018

View reviewed changes

kroening force-pushed the java-struct-tag branch from 24aa5f9 to d846585 Compare October 11, 2018 21:08

kroening removed their assignment Oct 11, 2018

allredj reviewed Oct 11, 2018

View reviewed changes

kroening force-pushed the java-struct-tag branch from d846585 to 5f18b69 Compare October 12, 2018 10:29

allredj reviewed Oct 12, 2018

View reviewed changes

allredj suggested changes Oct 22, 2018

View reviewed changes

kroening force-pushed the java-struct-tag branch 5 times, most recently from af8a9df to 39e5ab6 Compare November 8, 2018 15:21

allredj reviewed Nov 8, 2018

View reviewed changes

kroening force-pushed the java-struct-tag branch from 39e5ab6 to 4b98156 Compare November 17, 2018 19:04

allredj reviewed Nov 17, 2018

View reviewed changes

kroening force-pushed the java-struct-tag branch from 4b98156 to 708a46d Compare November 25, 2018 12:11

allredj reviewed Nov 25, 2018

View reviewed changes

Daniel Kroening added 3 commits November 30, 2018 07:06

use a struct_tag to identify base classes

7523aeb

C++: bases are now struct tags

83ad3c2

java frontend: symbol_type -> struct_tag

ddcf2c8

kroening force-pushed the java-struct-tag branch from 708a46d to ddcf2c8 Compare November 30, 2018 15:06

allredj reviewed Nov 30, 2018

View reviewed changes

allredj mentioned this pull request Dec 5, 2018

Java now uses struct_tag types (2nd edition) #3530

Merged

7 tasks

kroening closed this Dec 7, 2018

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Java now uses struct_tag types #3102

Java now uses struct_tag types #3102

kroening commented Oct 5, 2018

allredj left a comment

tautschnig left a comment

owen-mc-diffblue Oct 7, 2018

smowton commented Oct 8, 2018

allredj left a comment

martin-cs left a comment

allredj left a comment

peterschrammel commented Oct 12, 2018

allredj commented Oct 12, 2018

allredj left a comment

allredj left a comment

allredj left a comment

allredj left a comment

allredj left a comment

allredj left a comment

Java now uses struct_tag types #3102

Java now uses struct_tag types #3102

Conversation

kroening commented Oct 5, 2018

allredj left a comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

owen-mc-diffblue Oct 7, 2018

Choose a reason for hiding this comment

smowton commented Oct 8, 2018

allredj left a comment

Choose a reason for hiding this comment

martin-cs left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

peterschrammel commented Oct 12, 2018

allredj commented Oct 12, 2018

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment