-
Notifications
You must be signed in to change notification settings - Fork 277
JBMC: Added java-models-library dependency #2225
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
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -233,6 +233,7 @@ jobs: | |
name: "diffblue/cbmc" | ||
description: "Travis build of ${TRAVIS_COMMIT}" | ||
notification_email: "coverity-scan@diffblue.com" | ||
build_command_prepend: "make -C jbmc/src java-models-library-download" | ||
build_command_prepend: "make -C src minisat2-download" | ||
build_command: "make -C src -j2; make -C jbmc/src -j2" | ||
branch_pattern: "develop" | ||
|
@@ -259,6 +260,7 @@ jobs: | |
install: | ||
- ccache -z | ||
- ccache --max-size=1G | ||
- make -C jbmc/src java-models-library-download | ||
- make -C src minisat2-download | ||
- make -C src/ansi-c library_check | ||
- make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3 | ||
|
@@ -286,4 +288,3 @@ notifications: | |
on_start: never | ||
on_cancel: never | ||
on_error: always | ||
|
||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Nit pick: I think this blank line should be removed completely. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. done |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -30,8 +30,10 @@ Compilation | |
To compile you need to run the command: | ||
|
||
```bash | ||
make -C jbmc/src java-models-library-download | ||
make -C jbmc/src | ||
``` | ||
|
||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The file There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. done |
||
Output | ||
====== | ||
|
||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,5 @@ | ||
DIRS = janalyzer jbmc jdiff java_bytecode miniz | ||
ROOT = ../ | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Is this variable necessary? You could obtain the path pointed by it via There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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 There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. That's what I meant, you could use |
||
|
||
include config.inc | ||
|
||
|
@@ -40,11 +41,33 @@ generated_files: $(patsubst %, %_generated_files, $(DIRS)) | |
# cleaning | ||
|
||
.PHONY: clean | ||
clean: $(patsubst %, %_clean, $(DIRS)) cprover_clean | ||
clean: $(patsubst %, %_clean, $(DIRS)) cprover_clean dist_clean | ||
|
||
$(patsubst %, %_clean, $(DIRS)): | ||
$(MAKE) $(MAKEARGS) -C $(patsubst %_clean, %, $@) clean ; \ | ||
|
||
.PHONY: cprover_clean | ||
cprover_clean: | ||
$(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/src clean | ||
|
||
.PHONY: dist_clean | ||
dist_clean: | ||
rm -rf $(ROOT)dist | ||
|
||
# extended JBMC models download, for your convenience | ||
java-models-library-download: | ||
@echo "Downloading java models library" | ||
@wget https://github.com/diffblue/java-models-library/archive/master.zip -O java-models-library.zip | ||
@unzip java-models-library.zip | ||
@rm java-models-library.zip | ||
@cp -r java-models-library-master/src java_bytecode/library | ||
@rm -r java-models-library-master | ||
|
||
.PHONY: dist | ||
dist: java-models-library-download all | ||
mkdir -p $(ROOT)dist/lib | ||
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 | ||
cp jdiff/jdiff $(ROOT)dist/bin |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -27,7 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com | |
#include <langapi/language.h> | ||
|
||
#define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \ | ||
"(no-core-models)" \ | ||
"(java-assume-inputs-non-null)" \ | ||
"(java-throw-runtime-exceptions)" \ | ||
"(java-max-input-array-length):" \ | ||
|
@@ -40,8 +39,6 @@ Author: Daniel Kroening, kroening@kroening.com | |
"(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(*) */ \ | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. You have to remove the next line too! There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. oops,fixed. |
||
" the Java Class Library\n" /* NOLINT(*) */ \ | ||
" --java-assume-inputs-non-null never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \ | ||
" entry point with null\n" /* NOLINT(*) */ \ | ||
" --java-throw-runtime-exceptions make implicit runtime exceptions explicit\n" /* NOLINT(*) */ \ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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"; | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This file should be moved to the other PR. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. @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? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. ok |
||
src.close(); | ||
return 0; | ||
} |
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 should probably go into the PR that is on hold.