-
Notifications
You must be signed in to change notification settings - Fork 273
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
Use submodule to download java-models-library #2426
Use submodule to download java-models-library #2426
Conversation
This won't fix the current CI failures in |
But it's a step in the right direction, indeed |
9d055e2
to
c00bf6f
Compare
I have no prior experience on how GitHub displays submodules or submodule updates as PRs: is the set-up such that this PR would set the submodule at some commit, and any updates would be done via PR that just changes the commit that's being pointed to? |
There was a problem hiding this 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: c00bf6f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77136993
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).
set(CMAKE_JAVA_COMPILE_FLAGS -sourcepath "src" -d "classes" -XDignore.symbol.file) | ||
|
||
# create a target for the executable performing the .jar -> .inc conversion | ||
# Executable |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Probably keep the comment above?
@tautschnig Yes |
c00bf6f
to
6f34439
Compare
Looks like tests that directly reference the core-models jar location need amending. Also perhaps worth looking at whether it's right that they core dump when the path is wrong, rather than reporting an error cleanly. |
We'll need to produce a bit of scripting to be still able to distribute tar balls. @tautschnig How does this work with Debian? |
Since there isn't a problem distributing it when the source is made available it's all fine as far as Debian is concerned. I believe the only point of concern is any user shipping binary-only products based on CBMC. Those will want a GPL-free tarball. |
6f34439
to
c2d4649
Compare
c2d4649
to
f7a4082
Compare
757bbcb
to
b00b5bd
Compare
@peterschrammel I already approved, people who own other code needed. |
dec31d2
to
3ea16f4
Compare
3ea16f4
to
b34e951
Compare
There was a problem hiding this 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: b34e951).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78496248
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).
* Squashed 'cbmc/' changes from 6409eae..2af8433 2af8433 Merge pull request diffblue#2566 from tautschnig/vs-sparse-array de65ec6 Merge pull request diffblue#2541 from tautschnig/vs-string-static 7c4b5aa Merge pull request diffblue#2568 from tautschnig/vs-parameter-names ef3eb4f Merge pull request diffblue#2567 from peterschrammel/fix-mcdc 53baae6 Merge pull request diffblue#2460 from tautschnig/vs-local-unused 6acabcb Merge pull request diffblue#2563 from tautschnig/vs-rm-interface 3c2e55e Merge pull request diffblue#2426 from peterschrammel/java-models-library-submodule 440ceb6 Document proposed best practice for unused parameters 370d4c6 Convert /* */ comments into // 1abbf1e Clean up commented code b34e951 Use submodule to download java-models-library 3f255b2 Merge pull request diffblue#2388 from peterschrammel/improve-jbmc-options 15f44c7 Revert "Mark tests which fail due to invariant violations" dce4afd Make local-assigned-but-not-used annotation applicable to all compilers 86d057d (interval_)sparse_arrayt: Remove unnecessary use of "virtual" and further cleanup 0d7a943 Merge pull request diffblue#2558 from tautschnig/linking-xen 5acc0b0 Merge pull request diffblue#2392 from NathanJPhillips/cleanup/small_map_layout ee4d802 Merge pull request diffblue#2565 from tautschnig/vs-float-bvt 754b36d Accept more mismatching function definition/declaration pairs d1a4169 Merge pull request diffblue#2542 from tautschnig/vs-string-refinement b2cd358 Cleanup of float_bvt 0a39f40 Remove unused interface c749b8f Merge pull request diffblue#2429 from tautschnig/vs-endian 0a10bf3 Drop java prefix from throw-runtime-exceptions option 548baea Improve naming of command line options 39bc7ea Make --lazy-methods and --refine-strings default eb9e3bb Merge pull request diffblue#2561 from Degiorgio/get-current-thread-id-fix d98a39b Merge pull request diffblue#2556 from peterschrammel/run-string-smoke-tests 34404f0 Set little_endian in the same way that boolbv_byte_extract already does 4a8dc96 JBMC: removed camel-casing from function identifiers 9059be7 JBMC: CProver.getCurrentThreadID:()I conversion fix d393d1c Merge pull request diffblue#2435 from tautschnig/vs-ranged-for be7159a Merge pull request diffblue#2425 from tautschnig/vs-virtual 44cc033 Change index variable name, simplify code 0c9658f Add missing virtual destructor c6f9231 Merge pull request diffblue#2553 from tautschnig/always-inline-partial-revert fa94bc0 Merge pull request diffblue#2531 from tautschnig/debian4 41863e7 Merge pull request diffblue#2539 from tautschnig/vs-unsigned-constant f1afbff Remove unnecessary PLATFORM_DIRS 0c75b47 Run strings-smoke-tests and janalyzer tests 0acae08 Merge pull request diffblue#2535 from tautschnig/debian7 35ddf0b Merge pull request diffblue#2533 from tautschnig/debian5 580f539 Merge pull request diffblue#2534 from tautschnig/debian6 b73a9e3 Merge pull request diffblue#2420 from tautschnig/vs-invariant 9b087dc Merge pull request diffblue#2550 from tautschnig/vs-return dc35270 Merge pull request diffblue#2547 from tautschnig/vs-dummy-init ff88c16 Merge pull request diffblue#2554 from tautschnig/ld-options 3209628 Merge pull request diffblue#2450 from tautschnig/c++-name-resolution 61a6acd Name resolution may require further template instantiation 0f15d47 goto-ld: accept (but do not process) further ld options 4c6cfc0 Merge pull request diffblue#2448 from tautschnig/c++-delayed-body c46d46d Merge pull request diffblue#2439 from tautschnig/vs-pointer 7e4dd05 Merge pull request diffblue#2440 from tautschnig/vs-list 1f237ff Merge pull request diffblue#2464 from tautschnig/vs-unused1 7be54b8 Merge pull request diffblue#2544 from tautschnig/vs-value-set 7f373c8 Merge pull request diffblue#2549 from tautschnig/vs-unsigned-option b17fefa Merge pull request diffblue#2540 from tautschnig/vs-explicit-cast 425db26 Merge pull request diffblue#2530 from tautschnig/debian3 2598141 Mark integer constants as unsigned when lhs is unsigned 0da9766 Merge pull request diffblue#2538 from tautschnig/vs-use-to_ulong e501317 Additional regression tests for always_inline 17a50c5 Revert "Apply symbol replacement in type_arg members" 016ad92 Revert "Fully interpret __attribute__((always_inline))" ee9444f Merge pull request diffblue#2532 from tautschnig/debian2 c8725cb Merge pull request diffblue#2536 from tautschnig/debian8 d6565ec Merge pull request diffblue#2537 from tautschnig/vs-non-deprecated 16e6a99 Use type-consistent unsigned value for unreachable return statement a746a2c Extract unsigned value from options 681ec22 Add dummy initialisation to avoid Visual Studio warning c789088 Remove unused parameter from value_set_fivrt::flatten_rec 4d8aa45 Use std::string(N, ' ') instead of static locals 18faa5a String refinement: remove unused parameters 96a7014 Explicit type cast to avoid signed/unsigned warning 2aa6a2f Use non-deprecated to_integer(constant_expr) 13f83d5 Use to_ulong instead of the deprecated integer2ulong 26803f7 Test only works with simplification enabled be5f2ff Use architecture-specific compiler flags to configure bit width during preprocessing 60ad26c kfreebsd also uses ELF, and hybrid binaries are thus supported c6c1938 utf8 to utf16 conversion must use native endianness bc7a527 Fix copy&paste error in C library cd6127a Regression test should succeed even if char is an unsigned type dab6a6e Fix tests that are only correct on little-endian architectures 8187bdd Merge pull request diffblue#2526 from jeannielynnmoulton/jeannie/AnonymousInnerClasses af0ce5a Captures anonymous inner class information. d20a12e Merge pull request diffblue#2517 from jeannielynnmoulton/jeannie/InnerStaticClasses fe73955 Captures information for static inner classes. 4193f02 Remove unused parameters message_handler, ns 02e3840 Fix delayed method body conversion for templates d0c2a49 Remove unused parameter from list_calls_and_arguments 0e9aa90 Remove unused and inconsistent pointer_object_has_type 497d296 Fix invariant: value must be strictly positive 3aa9b72 Add comment explaining unusual layout git-subtree-dir: cbmc git-subtree-split: 2af8433 * Add .gitmodules with details of java-models-library * Small changes to jbmc command line arguments * Add --no-refine-strings to cmdline, always set
2af8433 Merge pull request diffblue#2566 from tautschnig/vs-sparse-array de65ec6 Merge pull request diffblue#2541 from tautschnig/vs-string-static 7c4b5aa Merge pull request diffblue#2568 from tautschnig/vs-parameter-names ef3eb4f Merge pull request diffblue#2567 from peterschrammel/fix-mcdc 53baae6 Merge pull request diffblue#2460 from tautschnig/vs-local-unused 6acabcb Merge pull request diffblue#2563 from tautschnig/vs-rm-interface 3c2e55e Merge pull request diffblue#2426 from peterschrammel/java-models-library-submodule 440ceb6 Document proposed best practice for unused parameters 370d4c6 Convert /* */ comments into // 1abbf1e Clean up commented code b34e951 Use submodule to download java-models-library 3f255b2 Merge pull request diffblue#2388 from peterschrammel/improve-jbmc-options 15f44c7 Revert "Mark tests which fail due to invariant violations" dce4afd Make local-assigned-but-not-used annotation applicable to all compilers 86d057d (interval_)sparse_arrayt: Remove unnecessary use of "virtual" and further cleanup 0d7a943 Merge pull request diffblue#2558 from tautschnig/linking-xen 5acc0b0 Merge pull request diffblue#2392 from NathanJPhillips/cleanup/small_map_layout ee4d802 Merge pull request diffblue#2565 from tautschnig/vs-float-bvt 754b36d Accept more mismatching function definition/declaration pairs d1a4169 Merge pull request diffblue#2542 from tautschnig/vs-string-refinement b2cd358 Cleanup of float_bvt 0a39f40 Remove unused interface c749b8f Merge pull request diffblue#2429 from tautschnig/vs-endian 0a10bf3 Drop java prefix from throw-runtime-exceptions option 548baea Improve naming of command line options 39bc7ea Make --lazy-methods and --refine-strings default eb9e3bb Merge pull request diffblue#2561 from Degiorgio/get-current-thread-id-fix d98a39b Merge pull request diffblue#2556 from peterschrammel/run-string-smoke-tests 34404f0 Set little_endian in the same way that boolbv_byte_extract already does 4a8dc96 JBMC: removed camel-casing from function identifiers 9059be7 JBMC: CProver.getCurrentThreadID:()I conversion fix d393d1c Merge pull request diffblue#2435 from tautschnig/vs-ranged-for be7159a Merge pull request diffblue#2425 from tautschnig/vs-virtual 44cc033 Change index variable name, simplify code 0c9658f Add missing virtual destructor c6f9231 Merge pull request diffblue#2553 from tautschnig/always-inline-partial-revert fa94bc0 Merge pull request diffblue#2531 from tautschnig/debian4 41863e7 Merge pull request diffblue#2539 from tautschnig/vs-unsigned-constant f1afbff Remove unnecessary PLATFORM_DIRS 0c75b47 Run strings-smoke-tests and janalyzer tests 0acae08 Merge pull request diffblue#2535 from tautschnig/debian7 35ddf0b Merge pull request diffblue#2533 from tautschnig/debian5 580f539 Merge pull request diffblue#2534 from tautschnig/debian6 b73a9e3 Merge pull request diffblue#2420 from tautschnig/vs-invariant 9b087dc Merge pull request diffblue#2550 from tautschnig/vs-return dc35270 Merge pull request diffblue#2547 from tautschnig/vs-dummy-init ff88c16 Merge pull request diffblue#2554 from tautschnig/ld-options 3209628 Merge pull request diffblue#2450 from tautschnig/c++-name-resolution 61a6acd Name resolution may require further template instantiation 0f15d47 goto-ld: accept (but do not process) further ld options 4c6cfc0 Merge pull request diffblue#2448 from tautschnig/c++-delayed-body c46d46d Merge pull request diffblue#2439 from tautschnig/vs-pointer 7e4dd05 Merge pull request diffblue#2440 from tautschnig/vs-list 1f237ff Merge pull request diffblue#2464 from tautschnig/vs-unused1 7be54b8 Merge pull request diffblue#2544 from tautschnig/vs-value-set 7f373c8 Merge pull request diffblue#2549 from tautschnig/vs-unsigned-option b17fefa Merge pull request diffblue#2540 from tautschnig/vs-explicit-cast 425db26 Merge pull request diffblue#2530 from tautschnig/debian3 2598141 Mark integer constants as unsigned when lhs is unsigned 0da9766 Merge pull request diffblue#2538 from tautschnig/vs-use-to_ulong e501317 Additional regression tests for always_inline 17a50c5 Revert "Apply symbol replacement in type_arg members" 016ad92 Revert "Fully interpret __attribute__((always_inline))" ee9444f Merge pull request diffblue#2532 from tautschnig/debian2 c8725cb Merge pull request diffblue#2536 from tautschnig/debian8 d6565ec Merge pull request diffblue#2537 from tautschnig/vs-non-deprecated 16e6a99 Use type-consistent unsigned value for unreachable return statement a746a2c Extract unsigned value from options 681ec22 Add dummy initialisation to avoid Visual Studio warning c789088 Remove unused parameter from value_set_fivrt::flatten_rec 4d8aa45 Use std::string(N, ' ') instead of static locals 18faa5a String refinement: remove unused parameters 96a7014 Explicit type cast to avoid signed/unsigned warning 2aa6a2f Use non-deprecated to_integer(constant_expr) 13f83d5 Use to_ulong instead of the deprecated integer2ulong 26803f7 Test only works with simplification enabled be5f2ff Use architecture-specific compiler flags to configure bit width during preprocessing 60ad26c kfreebsd also uses ELF, and hybrid binaries are thus supported c6c1938 utf8 to utf16 conversion must use native endianness bc7a527 Fix copy&paste error in C library cd6127a Regression test should succeed even if char is an unsigned type dab6a6e Fix tests that are only correct on little-endian architectures 8187bdd Merge pull request diffblue#2526 from jeannielynnmoulton/jeannie/AnonymousInnerClasses af0ce5a Captures anonymous inner class information. d20a12e Merge pull request diffblue#2517 from jeannielynnmoulton/jeannie/InnerStaticClasses fe73955 Captures information for static inner classes. 4193f02 Remove unused parameters message_handler, ns 02e3840 Fix delayed method body conversion for templates d0c2a49 Remove unused parameter from list_calls_and_arguments 0e9aa90 Remove unused and inconsistent pointer_object_has_type 497d296 Fix invariant: value must be strictly positive 3aa9b72 Add comment explaining unusual layout git-subtree-dir: cbmc git-subtree-split: 2af8433
No description provided.