Set name of java array types #2355
Merged
+5
−0
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
owen-mc-diffblue
requested review from
cesaro,
mgudemann,
peterschrammel,
smowton and
thk123
as code owners
owen-mc-diffblue
force-pushed
the
owen-jones-diffblue/add-name-to-array-type
branch
from
b52dc90 to
27b18a4
Compare
|
This seems sensible, your suggestion seems sensible, in either case this needs a manual TG bump to check the tests. |
allredj
reviewed
Jun 15, 2018
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 27b18a4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76407979
smowton
approved these changes
Jun 15, 2018
owen-mc-diffblue
force-pushed
the
owen-jones-diffblue/add-name-to-array-type
branch
from
27b18a4 to
2df6d81
Compare
|
@thk123 I've made the TG bump: https://github.com/diffblue/test-gen/pull/1964 |
|
The TG bump has passed |
|
@thk123 CI has passed, the TG bump passed - review and merge? |
thk123
approved these changes
Jun 18, 2018
allredj
reviewed
Jun 18, 2018
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 2df6d81).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76541461
NathanJPhillips
pushed a commit
to NathanJPhillips/cbmc
that referenced
this pull request
Aug 22, 2018
e6d196d Merge pull request diffblue#2355 from owen-jones-diffblue/owen-jones-diffblue/add-name-to-array-type 6f7580d Merge pull request diffblue#2351 from romainbrenguier/bugfix/null-array b2089b7 Add unit test for array_poolt 2df6d81 Set name of java array types 50e02b0 Simplify make_char_array_for_char_pointer 645eda9 Improve invariant message 3c7a671 Look up for null pointer in array pool 32a4186 Merge pull request diffblue#2302 from romainbrenguier/refactor/ci-lazy-methods c4aadab Extract handle_virtual_methods_with_no_callees cac016d Extract a convert_and_analyze_method method ca0adc9 Correct indentation 24b6936 Extract entry_point_methods method 360fabe Merge pull request diffblue#2356 from peterschrammel/fix-goto-simplification 4394016 Temporary fix to enable if-then-else simplifications d433438 Test for if-then-else optimisation in goto convert e5d1c12 Merge pull request diffblue#2354 from Degiorgio/disable-soundness-check-for-shared-pointers 7d4d4bd Skip check for unsoundness in shared pointer handling (java only) 8e6244c Merge pull request diffblue#2043 from peterschrammel/fail-on-uncaught-exception ec3010f Merge pull request diffblue#1994 from tautschnig/concurrency-soundness 1a9850a Merge pull request diffblue#2326 from tautschnig/c++-enum b71efaf Merge pull request diffblue#2019 from tautschnig/remove-unused 26b13ae Abort concurrency encoding in possibly unsound cases cd2ef4b Enable throwing of AssertionError 653d887 Remove wrong assumption from goto check 07acde4 Refactor user-defined assertion translation for Java 04c0205 Assert that there is uncaught exception 1daf466 Use resolver to translate cpp_name to scoped base_name 471b20f Remove prop_assignmentt interface 2639cf1 Remove unused solvers/prop/prop_conv_store.{h,cpp} 502687e Remove unused solver/prop/prop_wrapper.h ae56978 Remove unused goto-analyzer/static_analyzer.{h,cpp} 2260f82 Remove path_accelerationt interface d350e5c Remove unused nondet_ifthenelse.{h,cpp} a4936f8 Remove unused cpp/recursion_counter.h 71cfbbd Remove unused sorted_vector.h 4d4c9c6 Revert "added pipe_stream class" 2696420 Revert "new exception class" 3fb06ba Revert "Added utility class to convert strings into expressions" 55bdbc7 Recompile regression test class files 118f41f Merge pull request diffblue#2352 from tautschnig/c++-auto-tc 5a4dc8d Merge pull request diffblue#2315 from diffblue/fix-goto 199d4cc prevent half-constructed GOTO instructions 72156d5 C++ front-end: fix auto+references after already-typechecked cleanup 8fac5ed Merge pull request diffblue#2069 from romainbrenguier/refactor/convert_instruction 309d207 remove conversion for non-deterministic-goto 67081d5 Extract convert_pop function cd98a1f Extract convert_switch function f2acb00 Extract convert_dup2_x2 function 66cf709 Extract convert_dup2_x1 function e0735af Extract convert_dup2 function 51f53ca Extract convert_const function d627638 Extract convert_invoke function fcfca08 Extract replace_calls_to_cprover_assume function 0a521a4 Extract convert_checkcast function 4c28f99 Extract convert_athrow function 21e37a8 Extract convert_monitorexit function a7bbf53 Extract do_exception_handling function 0aa1c8e Extract convert_monitorenter function 48dd97f Extract convert_multianewarray function edc4a28 Extract convert_newarray function f8d00f6 Extract convert_new function b846798 Extract convert_putstatic function 27af4a2 Extract convert_putfield function f1edff9 Extract convert_getstatic function 68bddf1 Remove redundant assert 6f0f3fb Extract convert_cmp2 function 3049281 Extract convert_cmp function 5a5788c Extract convert_ushr function 305ede8 Extract convert_iinc function 61d03da Extract convert_ifnull function b4f6d04 Extract convert_if_nonull function 0e911d4 Extract convert_if function 651246e Extract convert_if_cmp function fc95df1 Extract convert_ret function ce58dca Extract convert_aload/store/astore functions 14e3c35 Extract convert_invokedynamic function 939bb53 Rename iterators and use auto ddb31a0 Extract draw_edges_from_ret_to_jsr function 390063f Extract try_catch_handler function 87a4f31 Make label static 36ed947 Replace assert by invariant 036f1b1 Use auto for iterator types git-subtree-dir: cbmc git-subtree-split: e6d196d
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Most types have a name like
java::java.lang.Objectand a tag likejava.lang.Object. Arrays don't have a name and have a tag likejava::array[int]orjava::array[reference]. I've set the name to be the same as the tag.I think we should also remove the
java::from the front of the tag, to be more consistent with other types.