JBMC: Added java-models-library dependency #2225

Degiorgio · 2018-05-22T15:25:01Z

JBMC: Added java-models-library dependency

This commit adds a dependency to the java-models-library
(https://github.com/diffblue/java-models-library). This repository
contains models for a number of classes derived from the java standard
library. These models are needed, i.e., to support concurrency.

This means that the process of building JBMC has changed slightly as
one first needs to download the java-models-library:

  make -C jbmc/src java-models-library-download
  make -C jbmc/src

Due possible licensing issues, the ability to automatically embed the
java core models into JBMC has been removed. Instead, one must
explicitly use the '--classpath' option to load the models.
Consequently, the '--no-core-models' option and related code was
removed as it is no longer relevant.

Commit also adds a new make target, make dist. This target in
addition to building jbmc will create a dist/ directory with two
sub-folders, bin and lib. Executables will be copied to the former,
while 'core-models.jar' will copied to the latter.

Note: src/org/cprover/CProver.java has also been removed as this has
been superseded by the CProver.java in the java-models-library.

TEST-GEN-POINTER-BUMP: https://github.com/diffblue/test-gen/pull/1878

chrisr-diffblue · 2018-05-22T15:29:38Z

jbmc/src/Makefile

+
+java-models-library-download:
+	@echo "Downloading java models library"
+	@curl -L https://github.com/diffblue/java-models-library/archive/master.zip > java-models-library.tar.gz


This seems wrong - you are downloading a .zip file, but saving it with a .tar.gz extension...

oops, it still works but its misleading, fixed.

chrisr-diffblue · 2018-05-22T15:31:34Z

jbmc/src/java_bytecode/library/converter.cpp

@@ -66,7 +66,7 @@ int main(int argc, char *argv[])
    printf("\n");
  }

-  std::cout << "\n#define " << varname <<  "_SIZE " << size << "\n\n";
+  std::cout << "\n#define " << varname <<  "_SIZE " << size << "\n";


I know you mentioned this change in the PR description, and I don't have strong feels whether it belongs in the PR or not, but if it's in this PR it should probably be in a commit of it's own.

tautschnig

If I understand correctly, the jbmc binary will include the model library (as a large string). Does the Classpath Exception make the resulting jbmc binary distributable under the BSD license? My reading is that that's the case, but more knowledgeable people's input would be good to have.

tautschnig · 2018-05-22T15:35:18Z

.travis.yml

@@ -286,4 +288,4 @@ notifications:
    on_start: never
    on_cancel: never
    on_error: always
-


Nit pick: I think this blank line should be removed completely.

tautschnig · 2018-05-22T15:37:59Z

jbmc/src/java_bytecode/library/.gitignore

+classes
+converter
+core-models.jar
+java_core_models.inc


We don't do per-directory gitignore files elsewhere, so this might cause confusion. I'd suggest to include this in the top-level .gitignore file.

Degiorgio · 2018-05-22T16:01:07Z

@tautschnig yes this is correct, @peterschrammel ?

peterschrammel

With the risk of kicking off a side-discussion: Is there a way for the user to obtain a copy of the org.cprover package as a jar file? The user will need it in order to compile any java code that directly uses org.cprover methods. Maybe org.cprover should be published as a separate package on maven?

tautschnig · 2018-05-22T16:09:42Z

Knowing nothing about maven: cbmc and goto-cc have dist-* scripts that put together archives that eventually go on the website. I'm not sure what the intended distribution story for jbmc is, but it may be worth adding such scripts that would then also ship the compiled jar file?

Degiorgio · 2018-05-22T16:14:39Z

@peterschrammel, when jbmc/src/java_bytecode/library is built core-models.jar gets generated. This contains both the org.cprover and java model classes. If we need a jar file with only org.cprover, then we would need to modify the build scripts (either in CBMC or the java-models-library repository)

peterschrammel · 2018-05-22T16:16:55Z

@Degiorgio, can you put core-models.jar on the classpath without getting conflicts with rt.jar?

Degiorgio · 2018-05-22T16:35:53Z

@peterschrammel , as discussed, I will modify the build scripts to generate two jars files:

1: core-models.jar: containing only java models
2: cprover.jar: containing only org.cprover

will only embed core-models.jar into jbmc executable.

smowton · 2018-05-23T07:35:47Z

Does this mean jbmc will always run with the models lib, regardless of the input? I ask as it's pretty heavy, which will prevent any non-lazy-loading test from running.

Degiorgio · 2018-05-23T09:25:42Z

@smowton , by default yes, but you can disable the models by specifying the '--no-core-models' flag. Will run some tests on this. Worst case we will make it opt-in instead of opt-out

peterschrammel · 2018-05-24T09:49:00Z

We should keep it 'opt out' because no 'normal user' would be able to run the tool without core models.
I have commits in https://github.com/peterschrammel/cbmc/tree/cav18-rebased that clean up all the tests to enable lazy loading where necessary, but requires further rebasing now.

Degiorgio · 2018-05-30T08:53:12Z

@peterschrammel out of abundance of caution, would it be acceptable, to make it 'opt-in' at first? My reasoning here is that without the lazy loading option it will lead to a blow-up, even for the simplest of use-cases. I think if we where to make it it 'opt-out' we should also make lazy loading 'opt-out'.

Degiorgio · 2018-05-31T16:18:57Z

@peterschrammel @tautschnig updated to address possible licensing issues.

Degiorgio · 2018-05-31T16:20:36Z

@peterschrammel I will split core-models.jar (into two jars, one for core-models and one for CProver API) in a separate pr.

cesaro

A couple of things to change

cesaro · 2018-06-01T16:26:47Z

jbmc/README.md

 make -C jbmc/src
 ```
+


The file COMPILING.md should be updated as well.

cesaro · 2018-06-01T16:29:34Z

jbmc/src/Makefile

@@ -1,4 +1,5 @@
 DIRS = janalyzer jbmc jdiff java_bytecode miniz
+ROOT = ../


Is this variable necessary? You could obtain the path pointed by it via $(CPROVER_DIR)?

CPROVER_DIR gives the path to the project root, since the generated files are for JBMC, it kind does not make sense for the JBMC distribution folder to be in the root of the repository (it should be in $(CPROVER_DIR)/jbmc

That's what I meant, you could use $(CPROVER_DIR)/jbmc wherever you use ROOT. You can ignore this, it's a small thing.

cesaro · 2018-06-01T16:32:02Z

jbmc/src/Makefile

+# extended JBMC models download, for your convenience
+java-models-library-download:
+	@echo "Downloading java models library"
+	@curl -L https://github.com/diffblue/java-models-library/archive/master.zip > java-models-library.zip


I would have use the /tmp folder as a temporary folder to store the zip file, but that's not very important.

I took this approach as its the one being used for minisat, for the sake of consistency, will leave it as is.

Could you use wget here (as we do for minisat-download)?

The minisat download uses (by default) lwp-download, which doesn't pick up the OS certificate chain required for HTTPS. I'm tempted to suggest to get rid of lwp-download instead.

cesaro · 2018-06-01T16:32:34Z

jbmc/src/Makefile

+
+.PHONY: dist
+dist: java-models-library-download all
+	@mkdir --p $(ROOT)dist/lib


-p instead of --p.

cesaro · 2018-06-01T16:36:20Z

jbmc/src/Makefile

+	@curl -L https://github.com/diffblue/java-models-library/archive/master.zip > java-models-library.zip
+	@unzip java-models-library.zip
+	@rm java-models-library.zip
+	@cp -r java-models-library-master/src java_bytecode/library


I see no reason to hide the commands here with @. I would remove it.

cesaro · 2018-06-01T16:36:58Z

jbmc/src/Makefile

+	@cp java_bytecode/library/core-models.jar $(ROOT)dist/lib
+	@mkdir --p $(ROOT)dist/bin
+	@cp jbmc/jbmc $(ROOT)dist/bin
+	@cp janalyzer/janalyzer $(ROOT)dist/bin


I would definitively like to see what make dist is doing when I type it, better to remove the @.

cesaro · 2018-06-01T16:50:29Z

jbmc/src/java_bytecode/library/CMakeLists.txt

+include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake")
+download_project(PROJ java_models_library
+    URL https://github.com/diffblue/java-models-library/archive/master.zip
+    PATCH_COMMAND cmake -E copy_directory "${JBMC_BINARY_DIR}/../../java_models_library-src/src"


Please document why you use the PATCH_COMMAND ;)

cesaro · 2018-06-01T16:51:43Z

jbmc/src/java_bytecode/library/CMakeLists.txt

-    DEPENDS ${JAVA_CORE_MODELS_INC})
+# copy 'core-models.jar' to '<PROJECT_ROOT>/jbmc/src/java_bytecode/library'.
+# This is needed to deal with unit tests that make use of the core-models
+# library.


add so that they can find the 'core-models.jar' in the same place as if the project had been compiled with 'make'.

cesaro · 2018-06-04T10:43:37Z

jbmc/src/Makefile

@@ -1,4 +1,5 @@
 DIRS = janalyzer jbmc jdiff java_bytecode miniz
+ROOT = ../


That's what I meant, you could use $(CPROVER_DIR)/jbmc wherever you use ROOT. You can ignore this, it's a small thing.

peterschrammel · 2018-06-04T16:56:29Z

jbmc/src/Makefile

+# extended JBMC models download, for your convenience
+java-models-library-download:
+	@echo "Downloading java models library"
+	@curl -L https://github.com/diffblue/java-models-library/archive/master.zip > java-models-library.zip


Could you use wget here (as we do for minisat-download)?

peterschrammel · 2018-06-04T16:57:24Z

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -40,7 +39,6 @@ Author: Daniel Kroening, [email protected]
  "(java-no-load-class):"

 #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/                                          \
-  " --no-core-models                 don't load internally provided models for core classes in\n"/* NOLINT(*) */ \


You have to remove the next line too!

oops,fixed.

peterschrammel · 2018-06-04T16:58:05Z

.gitignore

@@ -122,9 +121,13 @@ src/ansi-c/file_converter
 src/ansi-c/file_converter.exe
 src/ansi-c/library/converter
 src/ansi-c/library/converter.exe
-jbmc/src/java_bytecode/converter
-jbmc/src/java_bytecode/converter.exe
+jbmc/src/java_bytecode/library/converter.exe


This should probably go into the PR that is on hold.

peterschrammel · 2018-06-04T16:59:11Z

jbmc/src/java_bytecode/library/converter.cpp

@@ -66,7 +66,7 @@ int main(int argc, char *argv[])
    printf("\n");
  }

-  std::cout << "\n#define " << varname <<  "_SIZE " << size << "\n\n";
+  std::cout << "\n#define " << varname << "_SIZE " << size << "\n";


This file should be moved to the other PR.

@peterschrammel I'm not sure I get this. The converter program was committed long time ago. This just fixes a bug in it, I see no value in moving this bug fix to another PR. It has to be fixed no matter what?

This commit adds a dependency to the java-models-library (https://github.com/diffblue/java-models-library). This repository contains models for number of classes derived from the java standard library. These models are needed to support concurrency. This means that the process of building JBMC has changed slightly as one first needs to download the java-models-library. I.E: make -C jbmc/src java-models-library-download make -C jbmc/src Due possible licensing issues, the ability to automatically embed the java core models into JBMC has been removed. Instead, one must explicitly use the '--classpath' option to load the models. Consequently, the '--no-core-models' option and related code was removed as it is no longer relevant. Commit also adds a new make target, 'make dist'. This target in addition to building jbmc will create a 'dist' directory with two sub-folders, bin and lib. Executables will be copied to the former, while 'core-models.jar' will copied to the latter. Note: src/org/cprover/CProver.java has also been removed as this has been superseded by the CProver.java in the java-models-library.

Degiorgio · 2018-06-05T09:29:57Z

@peterschrammel addressed the issues you raised, with regards to the minor fix, my opinion is that it should stay in the PR as it is a bug that is currently present in develop and it is in a way related to the PR (although admittedly a bit contradictory, as in one commit we are removing core-models and in the other-one we are fixing it). Having said this, I have no issues with dropping it from this PR.

peterschrammel · 2018-06-05T12:52:29Z

jbmc/src/java_bytecode/library/converter.cpp

@@ -66,7 +66,7 @@ int main(int argc, char *argv[])
    printf("\n");
  }

-  std::cout << "\n#define " << varname <<  "_SIZE " << size << "\n\n";
+  std::cout << "\n#define " << varname << "_SIZE " << size << "\n";


9441a92 Merge pull request diffblue#2317 from tautschnig/c++-attributes-lists cad7b3a Merge pull request diffblue#2297 from romainbrenguier/bugfix/starts-with 7a6277d Reformat documentation without latex 0c56151 Add test for StartsWith d599dfc Allow duplicate instantiations of the same constant string 6763669 Correct starts_with for offset out of bound case 71f80e1 Deprecates add_axioms_for_is_suffix 8ee1c16 Merge pull request diffblue#2340 from tautschnig/c++-cassert 39a5631 Enabled failed-tests output in cbmc-cpp fafe4d9 C++ front-end: support =delete method declarations e3de3f6 Re-enable access control checks df85911 Fix access in test b092a13 char16_t and char32_t are typedefs in Visual Studio 1e00fcf Default to C++14 as language standard accepted by the C++ front-end on Windows 61ec7fc Merge pull request diffblue#2331 from diffblue/arch_flags_tests 8b2fc41 mark gcc tests as 'gcc-only' to prevent execution by goto-cl on Windows ebf7c7e fix return values of __builtin_classify_type 57ed2bc fix gcc_attributes10 2796025 Merge pull request diffblue#2329 from diffblue/msvc_packed_union 37c0b83 Merge pull request diffblue#2309 from qaphla/regression be6f3c9 Merge pull request diffblue#2346 from peterschrammel/fix-class-models-nondet d49ea09 Added an initial set of tests for contracts, which (expectedly) either fail or will need to be redone once the new flags are added in. d17c990 Merge pull request diffblue#2321 from tautschnig/vs-temporary-filet 43d008a Merge pull request diffblue#2347 from diffblue/smt2-bounds-checks dfff111 Merge pull request diffblue#2348 from tautschnig/c++-block-pointer 1d93fa1 Visual Studio packs bit-fields differently bffb1ca smt2_parser: avoid access to vector without prior size check e6d76e5 Merge pull request diffblue#2349 from tautschnig/document-gcc-req 7d0195a Fix allow-null initialization logic for class models 5a50203 Merge pull request diffblue#2308 from smowton/smowton/feature/must-not-throw-annotation bd74d87 Merge pull request diffblue#2343 from tautschnig/c++-auto d08a75a Document the required GCC/G++ version as >= 5.0 612fc38 C++ front-end: Type check Apple block pointers 278e506 Merge pull request diffblue#2345 from tautschnig/c++-array-ini af83568 C++11 auto type specifier 24ba2a0 Tests for proper pre-C++11 handling of "auto" 830c1d8 Revert "parse C++11 auto declarations" f3a3e79 Merge pull request diffblue#2344 from tautschnig/c++-vs-enum ce4884e C++ front-end: maintain #array_ini flag 19cfa50 Visual Studio supports C11 _Alignof e0d56da Support Visual Studio's forward enum declarations ab60852 Add org.cprover.MustNotThrow method attribute 5b8897e Merge pull request diffblue#2342 from tautschnig/constructor 12e8f46 Merge pull request diffblue#2341 from tautschnig/c++-qualified bc568b7 Only parameter-free constructors can be static initializer functions 57a14b0 C++ front-end: qualified template specialisation can just be accepted bcf8e61 Use temporary_filet for automatic resource management 1d95ab4 Permit compound literals in place of PODs e229b4c Typecheck initializer lists 999ad15 Swap order of subtypes in construction of merged_type nodes 4a47de6 Mark already-typechecked types as such d5183fb Permit GCC attributes after struct/class in class declaration d82f554 Permit asm post-declarator mixed in any order with other qualifiers fde09ca C++ front-end: parse GCC attributes 1f9deb3 Merge pull request diffblue#2333 from tautschnig/reduce-test-memory-footprint 04a8c35 Merge pull request diffblue#2334 from tautschnig/c++-virtual 0216dbd Merge pull request diffblue#2336 from tautschnig/c++-pointer-to-member 73d688d Merge pull request diffblue#2270 from peterschrammel/fix-stub-identifiers 13a1afc Merge pull request diffblue#2338 from tautschnig/c++-enum-operator 4ff6d5c Merge pull request diffblue#2337 from tautschnig/c++-enum-class 21bbecc Reduce memory cost of test by using a scalar variable instead of an array 439d6d3 Merge pull request diffblue#2332 from diffblue/goto-cc-warning-syntax a8f9fd9 C++ front-end: support pointer to non-method members 2f34833 C++ operator overload over enum tag types 4637f87 Fix virtual table construction f3550ea Cleanup: is_virtual is trivally true in this context a172c34 C++ virtual tables: fix inconsistent string suffixes ec5425e Code cleanup a7502c9 C++: support enum class 9e9f251 Prefix identifiers in stubs with function name 774060b Merge pull request diffblue#1768 from peterschrammel/fix-java-main-harness 3cb8bcf Deduplicate string tests 9b19015 Fix tests with incorrect main methods b047091 Simplify main method detection for Java b726dd1 Add regression tests for initialization of Java main args 7348c74 Elements of String array argument to Java main cannot be null 751c040 Simplify check whether String model is present 7a3a07f fix test result for goto-cl 8f2a82e Generalize allow_null to max_nonnull_tree_depth bbe8cca Java main method must be public 86b143b Merge pull request diffblue#2316 from tautschnig/ssa-perf-fix a6d32eb Merge pull request diffblue#2323 from tautschnig/vs-float 86687f7 Fix typos in doxygen f2ec10e Merge pull request diffblue#2320 from tautschnig/vs-return-type 0f2cc3a Merge pull request diffblue#2330 from diffblue/msvc-utf8 bdd5bbb ask CL preprocessor for UTF-8 output 1df3b9d Merge pull request diffblue#2325 from tautschnig/vs-empty-files ecee38d Remove useless cpp files ae1d039 Merge pull request diffblue#2322 from tautschnig/vs-cstring aeafc49 Merge pull request diffblue#2311 from diffblue/aws-codebuild-windows d4cd32d AWS codebuild buildspec for Windows 2c21295 missing dependency in Makefile 3fcdae1 Merge pull request diffblue#2319 from tautschnig/vs-linker-warning 6c22191 Merge pull request diffblue#2312 from diffblue/missing-iterator-headers 6a16f85 Merge pull request diffblue#2324 from tautschnig/vs-big-int-copyright d9a2339 Merge pull request diffblue#2327 from mre/patch-1 363291a Fix typo 8d6335a big-int copyright line c15f47f Mark floating-point constants as float 7e03746 Avoid using C string functions 3e8eff4 Fix the return type to match the class member types 1cb3d4d Avoid Visual Studio linker warning 33787ed missing <iterator> header 223d872 Revert undocumented change of 27153d1 63acc5b Merge pull request diffblue#2303 from smowton/smowton/fix/initialize-before-class-literal-init f927ae9 Merge pull request diffblue#2313 from smowton/smowton/admin/coverity-travis 6982f86 Improve coverity Travis build 894a20f Merge pull request diffblue#2294 from tautschnig/c++-built-ins 4edecbc Rename add_cprover_X_library to cprover_X_library_factory 1201ffe C++ front-end: Use C factory for compiler builtins 0451f1e C++ front-end now has its own library ed05d3e Refactor add_cprover_library to make parts re-usable by the C++ front-end 0ea6143 Make link_to_library independent of the C front-end c8702ab CPROVER library linking: move status message to front-end c471f72 jdiff: remove C library d597d90 Remove unused include 6877b21 Merge pull request diffblue#2305 from tautschnig/c++-operator da5ce90 Fix operator parsing 0d04f37 Merge pull request diffblue#2239 from mgudemann/bugfix/generics/fix_infinite_recursion 2e83ec9 Zero-initialize Class literals before calling initializer function b7725b8 Merge pull request diffblue#2306 from tautschnig/c++-qualifiers 0612749 Merge pull request diffblue#2304 from tautschnig/appveyor-warnings e54bba2 Merge pull request diffblue#2293 from tautschnig/c++-decltype-bit-field d196cf7 Add regression test for recursive generic-parameters 934c555 Do not lose method qualifiers d7b1572 Doxygen update 2d9970c Clarify and correct 04565b4 Un-deprecate to_integer(constant_exprt) feb59ab Use not-as-deprecated version of to_integer e23a1bb Avoid deprecated code_typet() constructor aef48c2 Avoid implicit cast int -> bool c5de7ba Merge pull request diffblue#2296 from smowton/smowton/fix/restore-float128 8c08946 decltype(bit field type) is the underlying subtype 9160e99 Merge pull request diffblue#2292 from tautschnig/c++-windows 7b61482 Extend cbmc ts18661 test 4180e65 Add test for gcc-5 b46e4bf Improve gcc-4 and -7 tests b0d1f9e Restore _Float128 support by default 22b9182 Merge pull request diffblue#2165 from tautschnig/interpreter-member-offset 5fd18a9 Enable C++ regression tests on AppVeyor 8d86e44 Prevent regression failures of cpp tests on windows 9adf5f1 Configure C++ language standard in goto-cl 10a4685 Merge pull request diffblue#2219 from tautschnig/nondet-initializer e12cb04 Merge pull request diffblue#2298 from tautschnig/move-printf_formatter 71c1227 Merge pull request diffblue#2299 from tautschnig/no-c_qualifier 339fcbd Merge pull request diffblue#2300 from tautschnig/no-c_typecast 0a77ce0 Do not use c_qualifiers on goto-program expressions d089ddd Do not use c_typecast in pointer-analysis 60ab7ec Array/vector sizes can be size_t 4031eac Non-negative array/vector sizes are invariants cf41a88 nondet_initializer to build deep non-deterministic expressions 626fb98 Rename zero_initializer to expr_initializer in preparation of generalisation bc15b1b Move zero_initializer to util 7716f3f Remove unused include cc23b20 Move printf_formatter to goto-programs 2ed63f5 Merge pull request diffblue#2156 from tautschnig/gcc-8-fixes 260156f Merge pull request diffblue#2288 from peterschrammel/code-type-const 2bea6fc Merge pull request diffblue#2274 from peterschrammel/travis-new-doxygen c6cfb02 Merge pull request diffblue#2291 from tautschnig/c++-fixes-1 80112d8 Make CMake regression test set match the Makefile one 63c5a32 Install doxygen 1.8.14 on travis 1bd942f Remove redundant invariants 11005ec Remove duplicate save_scope fc670b5 Do not lint .h files in regression/ 763d4d1 Style improvements 204c60f Failing regression test from diffblue#933 1132562 Failing regression test from diffblue#661 fe8ef6d Whitespace cleanup, comment type fixed 5bb13db Initial set of mini-system-c tests 3564324 Line break 402b29b Fix broken comment frame 8480d96 Fix command-line option syntax a3a4696 Fix syntax errors in C++ regression tests f2c60cf Do not use assert without prior declaration 7c053bf Merge pull request diffblue#2290 from diffblue/flt_rounds 4a7a389 Merge pull request diffblue#2262 from karkhaz/kk-rm-noop-depth-lookup 43b41a4 Simplify return f6586ed Rename functions to `get_recursively_instantiated_type` b0fde14 Doxygen update, clarification 8b4920e Return input pointer_type in case of no instantiation 05ff12d Clarifications and corrections 2c5e0b8 Return bound if no concrete instantiation is found 26e5433 Add unit test for mutually recursive generic parameters 6ff2993 Choose mapped-to type when doing higher depth search 31004f5 Search through stack for instantiation 3264023 Fix Typo 258e3ae Track recursion for generic type parameter definition 7360696 Use `std::vector` instead of `std::stack` 8f094e2 added model for FreeBSD __flt_rounds 98379b3 Interpreter: simplify code by not using member_offset_iterator 64cd733 Make code_typet declarations const 6d5e446 Merge pull request diffblue#2240 from diffblue/get-gcc-version b618d94 Merge pull request diffblue#2269 from peterschrammel/parameters-code-type 2a72bf2 Merge pull request diffblue#2268 from allredj/trigger-testgen 78794e2 undo parts of diffblue#2185 e040723 _FloatX support based on gcc version cd6ecec goto-cc now reports version of installed gcc fd910a7 added gcc_versiont 09a4e6c run() can now redirect stderr 32fd0c2 Return original type instead of nil in original_return_type 29bf299 Test for incomplete code_typet construction 05a5efb Use the two-param code_typet constructor 103c7b7 Add missing module definitions 724a36c Add two-param code_typet constructors and deprecate the default one 63a5131 Make sure code_typet is fully constructed 61b9647 Revert 0b3170d: Stabilize clinit wrapper function type parameters da34ceb Merge pull request diffblue#2283 from tautschnig/appveyor-fix 4d70915 Merge pull request diffblue#2279 from diffblue/void-star-arithmetic d668583 Merge pull request diffblue#2282 from diffblue/unused-lambda-capture 2a2907e Unstall AppVeyor by checking for the correct file path 7bad913 the 'this' capture is not used d24f773 Merge pull request diffblue#2233 from thomasspriggs/global_null_message_handler 690613d Merge pull request diffblue#2275 from tautschnig/gcc-case-range e8ff243 Merge pull request diffblue#2225 from cesaro/extended-java-models 5242dc9 Merge pull request diffblue#2265 from smowton/smowton/fix/dont-advertise-ignored-methods 6eab2f9 document why sizeof(void) works 690d10b Merge pull request diffblue#1956 from romainbrenguier/refactor/prop_conv_straightforward2 fc33598 Implement GCC's switch-case ranges e8d26ae Merge pull request diffblue#2267 from LAJW/lajw/always-load-cprover-nondet-initialize c6d2dba JBMC: Added java-models-library dependency e5f3c41 Use a reference with exception types that use vtables 7211280 Silence spurious GCC 8 warning 0c00835 Do not use parentheses around the declared symbol 4f3c102 Silence Minisat's use of realloc on non-POD and fix and use its xrealloc 3082d9d Merge pull request diffblue#2029 from tautschnig/remove-asm c14677b Java frontend: don't advertise ignored methods f8df76a Merge pull request diffblue#2276 from tautschnig/c-string-zero bb1bae9 Merge pull request diffblue#2184 from tautschnig/human-readable-output d35c2ac Refactoring in boolbvt::convert_byte_extract 523f8ae Zero-length C string operations should not yield pointer checks a673e5d Add test verifying that the cproverNondetInitialize method is always loaded 4d67ed5 goto-instrument: Remove inline asm before doing various operations 6f51513 Print (at debug level) the current SSA step being converted b0fce60 Print (at debug level) the size of assignments during symex e515f26 List all candidate functions for a function pointer at debug verbosity 9717af2 messaget helper to encapsulate if(debug-verbosity) { complex output } e698be9 Cleanup: use most suitable symbol_exprt constructor 07ef32d remove_const_function_pointerst::functionst only holds symbol expressions 75f021c Print current depth in BMC progress debug logging 65f0ec0 Provide a source location when analysis finds constness is lost 6f72d9b Split binary string in plain-text output of goto trace in groups of 8 0ff1384 Remove unused local variable e05dad5 Clang format include order. 8e20ac6 Use global `null_message_handlert` instead of duplicates. dab421c Add global instance of `null_message_handlert` 1a4fc92 Merge pull request diffblue#2089 from tautschnig/remove-skip-cleanup 971a34b Always load cprover-nondet-initialize d58eeb4 Add webhook to invoke a Diffblue-specific function 1b43ee9 Refactoring in boolbvt::convert_bitwise adc2d5d Make convert_abs take an abs_exprt parameter b837b8a Remove useless throws in boolbvt::convert_index 52d0fe4 Make build_offset_map return an offset_mapt 2dc7bee Replacing throws by invariants in boolbv convert 15ce938 Enable remove_skip to soundly remove skips with labels 3f34c1a Explicitly invoke goto_program.update() where remove_skip is not used 6bac80e Run remove_skip in passes that may introduce skips 533775c Remove redundant calls to compute_{location,loop}_numbers e9cdffd remove_skip includes goto_{program,functions}.update(), avoid redundant calls cfb733a Make remove_skip call goto_program.update() 91d47c2 remove_skip implementation restricted to a range of instructions 41d38bc Remove unused includes of remove_skip.h c9ead2c Avoid redundant calls to remove_skip 6298c18 Fix wrong function description 9e355e9 Use make_skip to turn an instruction into a SKIP b055179 Relax test: there need not be any code at the end of the block to cover f1a5d6a Make functions non-empty so that the test remains stable under skip cleanup 1bd4f04 JBMC: Minor fix, removing superfluous padding from converter b5ebe6b Remove string lookups from goto_symext main loop e77cabc Remove optionst member from goto_symext git-subtree-dir: cbmc git-subtree-split: 9441a92

Degiorgio requested review from cesaro, chrisr-diffblue, forejtv, kroening, mgudemann, peterschrammel, smowton, tautschnig and thk123 as code owners May 22, 2018 15:25

Degiorgio force-pushed the extended-java-models branch 2 times, most recently from 28c949a to 3288db1 Compare May 22, 2018 15:28

Degiorgio changed the title ~~JBMC: Added java-library models dependency~~ JBMC: Added java-models-library dependency May 22, 2018

Degiorgio force-pushed the extended-java-models branch 2 times, most recently from a047d3b to 51d926a Compare May 22, 2018 15:33

chrisr-diffblue reviewed May 22, 2018

View reviewed changes

Degiorgio force-pushed the extended-java-models branch from 51d926a to 572b166 Compare May 22, 2018 15:43

tautschnig reviewed May 22, 2018

View reviewed changes

Degiorgio force-pushed the extended-java-models branch from 572b166 to 3d7ebae Compare May 22, 2018 15:59

peterschrammel reviewed May 22, 2018

View reviewed changes

Degiorgio force-pushed the extended-java-models branch 4 times, most recently from 5bd719b to 8e0288e Compare May 22, 2018 19:34

Degiorgio force-pushed the extended-java-models branch 9 times, most recently from d505ff3 to 64c74c9 Compare May 23, 2018 13:07

Degiorgio force-pushed the extended-java-models branch from 64c74c9 to 72a9b78 Compare May 29, 2018 16:14

Degiorgio force-pushed the extended-java-models branch 2 times, most recently from 3a8588f to 11bbd99 Compare May 31, 2018 16:17

Degiorgio force-pushed the extended-java-models branch 2 times, most recently from 9158a15 to a97cdb3 Compare June 1, 2018 08:39

cesaro suggested changes Jun 1, 2018

View reviewed changes

JBMC: Minor fix, removing superfluous padding from converter

1bd4f04

Degiorgio force-pushed the extended-java-models branch from a97cdb3 to 4d07be9 Compare June 3, 2018 19:12

cesaro approved these changes Jun 4, 2018

View reviewed changes

Degiorgio force-pushed the extended-java-models branch from 4d07be9 to 8e38aa7 Compare June 4, 2018 10:56

peterschrammel reviewed Jun 4, 2018

View reviewed changes

Degiorgio force-pushed the extended-java-models branch from 8e38aa7 to c6d2dba Compare June 5, 2018 09:24

peterschrammel approved these changes Jun 5, 2018

View reviewed changes

cesaro merged commit e8ff243 into diffblue:develop Jun 5, 2018

		@@ -1,4 +1,5 @@
		DIRS = janalyzer jbmc jdiff java_bytecode miniz
		ROOT = ../

JBMC: Added java-models-library dependency #2225

JBMC: Added java-models-library dependency #2225

Conversation

Degiorgio commented May 22, 2018 • edited by cesaro Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio commented May 22, 2018 • edited Loading

peterschrammel left a comment • edited Loading

Choose a reason for hiding this comment

tautschnig commented May 22, 2018

Degiorgio commented May 22, 2018 • edited Loading

peterschrammel commented May 22, 2018

Degiorgio commented May 22, 2018 • edited Loading

smowton commented May 23, 2018

Degiorgio commented May 23, 2018 • edited Loading

peterschrammel commented May 24, 2018 • edited Loading

Degiorgio commented May 30, 2018 • edited Loading

Degiorgio commented May 31, 2018

Degiorgio commented May 31, 2018

cesaro left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio Jun 3, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio commented Jun 5, 2018 • edited Loading

Choose a reason for hiding this comment

Degiorgio commented May 22, 2018 •

edited by cesaro

Loading

Degiorgio commented May 22, 2018 •

edited

Loading

peterschrammel left a comment •

edited

Loading

Degiorgio commented May 22, 2018 •

edited

Loading

Degiorgio commented May 22, 2018 •

edited

Loading

Degiorgio commented May 23, 2018 •

edited

Loading

peterschrammel commented May 24, 2018 •

edited

Loading

Degiorgio commented May 30, 2018 •

edited

Loading

Degiorgio Jun 3, 2018 •

edited

Loading

Degiorgio commented Jun 5, 2018 •

edited

Loading