Skip to content

Given string types an appropriate name [TG-3908] #2479

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

Given string types an appropriate name [TG-3908] #2479

merged 3 commits into from
Jul 2, 2018

Conversation

thk123
Copy link
Contributor

@thk123 thk123 commented Jun 26, 2018

This is used when constructing a symbol_typet from a struct_typet. This causes problems in TG, not sure exactly how I can demonstrate the problem in CBMC.

@thk123
Copy link
Contributor Author

thk123 commented Jun 26, 2018

Will wait for TG to catch up to cbmc develop before creating a bump for this as non-urgent.

@thk123 thk123 changed the title Given string types an appropriate name Given string types an appropriate name [TG-3908] Jun 26, 2018
@kroening
Copy link
Member

there should be a set_name/get_name in class_typet, with the commentary that this is the identifier of the symbol.

allredj
allredj reviewed Jun 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: 780b7aa).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77317551

@thk123 thk123 mentioned this pull request Jun 26, 2018
Merged
antlechner
antlechner approved these changes Jun 29, 2018
View reviewed changes
Copy link
Contributor

@antlechner antlechner left a comment

Choose a reason for hiding this comment

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

Approving as this fixes a bug that's blocking me. :) Note that abstract string types like CharSequence are also missing an ID_abstract, would it be possible to add that too?

Given string types an appropriate name
dabc169 
This is used when constructing a symbol_typet from a struct_typet
@thk123 thk123 force-pushed the bugfix/TG-3908/give-string-objects-names branch from f5a25bb to fde12e6 Compare June 29, 2018 16:01
@thk123
Copy link
Contributor Author

thk123 commented Jun 29, 2018

@kroening method added - a proper cleanup should be done to ensure all uses of ID_name are done appropriately and consider whether it is even helpful to have a name and a tag associated with each class (where the later is essentially the name minus java::). But this is out of scope for this PR.

@thk123
Copy link
Contributor Author

thk123 commented Jun 29, 2018

Picked java_class_typet as the java parser seemed to be the main user of this field, can move to class_typet if it makes sense from the C++ perspective.

Motivation for keeping it low in the hierarchy: adding it suggests to the user a guarantee that all class_typets will have a name. I am certain for Java this is reasonable, but not for C++ so didn't want to imply a false level of confidence.

@thk123
Copy link
Contributor Author

thk123 commented Jun 29, 2018

TG PR: diffblue/test-gen#2005

allredj
allredj reviewed Jun 29, 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: f5a25bb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77733039
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).

allredj
allredj reviewed Jun 29, 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: fde12e6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77733602

mgudemann
mgudemann approved these changes Jul 2, 2018
View reviewed changes
Copy link
Contributor

@mgudemann mgudemann left a comment

Choose a reason for hiding this comment

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

LGTM

jbmc/src/java_bytecode/java_string_library_preprocess.cpp Outdated
@@ -222,6 +222,7 @@ void java_string_library_preprocesst::add_string_type(
{
java_class_typet string_type;
string_type.set_tag(class_name);
string_type.set_name("java::"+id2string(class_name));
Copy link
Contributor

Choose a reason for hiding this comment

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

clang-format

@thk123 thk123 force-pushed the bugfix/TG-3908/give-string-objects-names branch from fde12e6 to 031a38c Compare July 2, 2018 09:49
peterschrammel
peterschrammel approved these changes Jul 2, 2018
View reviewed changes
jbmc/src/java_bytecode/java_types.h Outdated

/// Get the name of the struct, which can be used to look up its symbol
/// in the symbol table.
irep_idt get_name() const
Copy link
Member

Choose a reason for hiding this comment

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

Const &?

allredj
allredj reviewed Jul 2, 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: 031a38c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77838852

@thk123 thk123 force-pushed the bugfix/TG-3908/give-string-objects-names branch from 031a38c to fd2f21e Compare July 2, 2018 10:29
allredj
allredj reviewed Jul 2, 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: fd2f21e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77842373

@thk123 thk123 merged commit b58813b into diffblue:develop Jul 2, 2018
@thk123 thk123 deleted the bugfix/TG-3908/give-string-objects-names branch July 2, 2018 11:47
NathanJPhillips added a commit to NathanJPhillips/cbmc that referenced this pull request Aug 22, 2018
@NathanJPhillips
Squashed 'cbmc/' changes from 6fd77f4..f90ed9e
496bbc6 
f90ed9e Merge pull request diffblue#2515 from NathanJPhillips/feature/ignored-methods
4a12a29 Prevent crash when only instance of class is marked as an overlay
841313d Add ability to mark methods as ignored (not loaded)
0c20014 Merge pull request diffblue#2513 from tautschnig/clean
4c14354 Merge pull request diffblue#2490 from tautschnig/switch-range
72b92a4 Merge pull request diffblue#2471 from tautschnig/vs-non-static
1941c6c Merge pull request diffblue#2508 from tautschnig/skip-typecast
a9e4ce9 Merge pull request diffblue#2512 from tautschnig/fix-typo
2be11f3 Make "clean" target in regression tests do full cleanup
97e9314 Do not hardcode tests.log as option -s <suffix> may be in use
ad1f266 Fix typo seperated -> separated
15d4307 Evaluate expressions that delimit GCC switch/case ranges
770b779 Make skip_typecast widely available
b4f5800 Merge pull request diffblue#2492 from NathanJPhillips/doc/get_writeable_symbol
b58813b Merge pull request diffblue#2479 from thk123/bugfix/TG-3908/give-string-objects-names
fd2f21e Use new method to set the name
190b485 Introduce method for getting the name of of java_class_type
ffbb83f Merge pull request diffblue#2496 from diffblue/compilation-instructions2
594c2f2 unzip is needed on Debian, plus say how to build jbmc on Windows
dabc169 Given string types an appropriate name
76eaf86 Doxygen comment on get_writeable_symbol
7191f23 Do not unnecessarily mark local variables static

git-subtree-dir: cbmc
git-subtree-split: f90ed9e
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

@mgudemann mgudemann mgudemann approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

@antlechner antlechner antlechner approved these changes

@romainbrenguier romainbrenguier Awaiting requested review from romainbrenguier

@cesaro cesaro Awaiting requested review from cesaro

@smowton smowton Awaiting requested review from smowton

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@thk123 @kroening @mgudemann @peterschrammel @allredj @antlechner