Given string types an appropriate name [TG-3908] by thk123 · Pull Request #2479 · diffblue/cbmc

thk123 · 2018-06-26T09:44:03Z

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 · 2018-06-26T09:53:26Z

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

kroening · 2018-06-26T10:16:30Z

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

allredj

Passed Diffblue compatibility checks (cbmc commit: 780b7aa).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77317551

antlechner

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?

This is used when constructing a symbol_typet from a struct_typet

thk123 · 2018-06-29T16:03:43Z

@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 · 2018-06-29T16:05:16Z

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 · 2018-06-29T16:06:02Z

TG PR: diffblue/test-gen#2005

allredj

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

Passed Diffblue compatibility checks (cbmc commit: fde12e6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77733602

mgudemann

LGTM

mgudemann · 2018-07-02T09:46:34Z

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

 {
  java_class_typet string_type;
  string_type.set_tag(class_name);
+  string_type.set_name("java::"+id2string(class_name));


clang-format

peterschrammel · 2018-07-02T09:50:34Z

jbmc/src/java_bytecode/java_types.h

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


allredj

Passed Diffblue compatibility checks (cbmc commit: 031a38c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77838852

allredj

Passed Diffblue compatibility checks (cbmc commit: fd2f21e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77842373

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

thk123 requested review from antlechner and romainbrenguier June 26, 2018 09:44

thk123 requested review from cesaro, mgudemann, peterschrammel and smowton as code owners June 26, 2018 09:44

thk123 changed the title ~~Given string types an appropriate name~~ Given string types an appropriate name [TG-3908] Jun 26, 2018

allredj reviewed Jun 26, 2018

View reviewed changes

thk123 mentioned this pull request Jun 26, 2018

Java object factory: initialize AbstractStringBuilder-derived types correctly #2472

Merged

antlechner approved these changes Jun 29, 2018

View reviewed changes

Given string types an appropriate name

dabc169

This is used when constructing a symbol_typet from a struct_typet

thk123 force-pushed the bugfix/TG-3908/give-string-objects-names branch from f5a25bb to fde12e6 Compare June 29, 2018 16:01

thk123 added the do not merge label Jun 29, 2018

allredj reviewed Jun 29, 2018

View reviewed changes

thk123 removed the do not merge label Jul 2, 2018

mgudemann approved these changes Jul 2, 2018

View reviewed changes

thk123 force-pushed the bugfix/TG-3908/give-string-objects-names branch from fde12e6 to 031a38c Compare July 2, 2018 09:49

peterschrammel approved these changes Jul 2, 2018

View reviewed changes

allredj reviewed Jul 2, 2018

View reviewed changes

thk123 added 2 commits July 2, 2018 11:29

Introduce method for getting the name of of java_class_type

190b485

Use new method to set the name

fd2f21e

thk123 force-pushed the bugfix/TG-3908/give-string-objects-names branch from 031a38c to fd2f21e Compare July 2, 2018 10:29

allredj reviewed Jul 2, 2018

View reviewed changes

thk123 merged commit b58813b into diffblue:develop Jul 2, 2018

thk123 deleted the bugfix/TG-3908/give-string-objects-names branch July 2, 2018 11:47

Conversation

thk123 commented Jun 26, 2018

Uh oh!

thk123 commented Jun 26, 2018

Uh oh!

kroening commented Jun 26, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

antlechner left a comment

Choose a reason for hiding this comment

Uh oh!

thk123 commented Jun 29, 2018

Uh oh!

thk123 commented Jun 29, 2018

Uh oh!

thk123 commented Jun 29, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

mgudemann left a comment

Choose a reason for hiding this comment

Uh oh!

mgudemann Jul 2, 2018

Choose a reason for hiding this comment

Uh oh!

peterschrammel Jul 2, 2018

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants