Skip to content

Commit b34e951

Browse files
peterschrammelpeterschrammel
committed
Use submodule to download java-models-library
1 parent 3f255b2 commit b34e951

File tree

12 files changed

+47
-81
lines changed

12 files changed

+47
-81
lines changed

Diff for: ‎.gitmodules

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
[submodule "jbmc/lib/java-models-library"]
2+
path = jbmc/lib/java-models-library
3+
url = https://github.com/diffblue/java-models-library.git

Diff for: ‎.travis.yml

+6-2
Original file line numberDiff line numberDiff line change
@@ -229,6 +229,7 @@ jobs:
229229
- ccache -z
230230
- ccache --max-size=1G
231231
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5'
232+
- git submodule update --init --recursive
232233
- cmake --build build -- -j4
233234
script: (cd build; ctest -V -L CORE -j2)
234235

@@ -254,6 +255,7 @@ jobs:
254255
- ccache -z
255256
- ccache --max-size=1G
256257
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7'
258+
- git submodule update --init --recursive
257259
- cmake --build build -- -j4
258260
script: (cd build; ctest -V -L CORE -j2)
259261

@@ -287,6 +289,7 @@ jobs:
287289
- ccache -z
288290
- ccache --max-size=1G
289291
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/clang++-6.0' '-DCMAKE_CXX_FLAGS=-Qunused-arguments'
292+
- git submodule update --init --recursive
290293
- cmake --build build -- -j4
291294
script: (cd build; ctest -V -L CORE -j2)
292295

@@ -305,6 +308,7 @@ jobs:
305308
- ccache -z
306309
- ccache --max-size=1G
307310
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
311+
- git submodule update --init --recursive
308312
- cmake --build build -- -j4
309313
script: (cd build; ctest -V -L CORE -j2)
310314

@@ -328,7 +332,7 @@ jobs:
328332
name: "diffblue/cbmc"
329333
description: "Travis build of ${TRAVIS_COMMIT}"
330334
notification_email: "[email protected]"
331-
build_command_prepend: "make -C jbmc/src java-models-library-download"
335+
build_command_prepend: "make -C jbmc/src setup-submodules"
332336
build_command_prepend: "make -C src minisat2-download"
333337
build_command: "make -C src -j2; make -C jbmc/src -j2"
334338
branch_pattern: "develop"
@@ -349,7 +353,7 @@ jobs:
349353
install:
350354
- ccache -z
351355
- ccache --max-size=1G
352-
- make -C jbmc/src java-models-library-download
356+
- make -C jbmc/src setup-submodules
353357
- make -C src minisat2-download
354358
- make -C src/ansi-c library_check
355359
- make -C src/cpp library_check

Diff for: ‎CMakeLists.txt

+1
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,7 @@ set_target_properties(
8181
xml
8282

8383
java_bytecode
84+
java-models-library
8485
jbmc
8586
jbmc-lib
8687
janalyzer

Diff for: ‎appveyor.yml

+1-5
Original file line numberDiff line numberDiff line change
@@ -42,17 +42,13 @@ install:
4242
& 7z x minisat2_2.2.1.orig.tar.gz
4343
&7z x minisat2_2.2.1.orig.tar
4444
}
45-
if (!(Test-Path java-models-library-master\.gitignore)) {
46-
& appveyor downloadfile https://github.com/diffblue/java-models-library/archive/master.zip -FileName jml.zip
47-
& 7z x jml.zip
48-
}
4945
cd ..
5046
5147
cache: deps
5248

5349
build_script:
5450
- cmd: |
55-
cp -r deps/java-models-library-master/src jbmc/src/java_bytecode/library
51+
make -C jbmc/src setup-submodules
5652
cp -r deps/minisat2-2.2.1 minisat-2.2.1
5753
patch -d minisat-2.2.1 -p1 < scripts/minisat-2.2.1-patch
5854
call "C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\vcvarsall.bat" x64

Diff for: ‎buildspec-windows.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ phases:
1919
2020
- |
2121
$env:Path = "C:\tools\cygwin\bin;$env:Path"
22-
cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/src BUILD_ENV=MSVC" '
22+
cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/src setup-submodules" && bash -c "make -j4 -C jbmc/src BUILD_ENV=MSVC" '
2323
cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/unit all BUILD_ENV=MSVC ; exit 0" '
2424
2525
post_build:

Diff for: ‎buildspec.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ phases:
1515
commands:
1616
- echo Build started on `date`
1717
- make -C src minisat2-download
18-
- make -C jbmc/src java-models-library-download
18+
- make -C jbmc/src setup-submodules
1919
- make -C src CXX="ccache g++" -j2
2020
- make -C unit CXX="ccache g++" -j2
2121
- make -C jbmc/src CXX="ccache g++" -j2

Diff for: ‎jbmc/CMakeLists.txt

+6
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,9 @@
11
add_subdirectory(regression)
22
add_subdirectory(src)
33
add_subdirectory(unit)
4+
5+
add_custom_target(java-models-library ALL
6+
COMMAND mvn package
7+
COMMAND cp target/core-models.jar ${CMAKE_CURRENT_SOURCE_DIR}/src/java_bytecode/library/
8+
WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library
9+
)

Diff for: ‎jbmc/lib/java-models-library

Submodule java-models-library added at 6b422b1

Diff for: ‎jbmc/regression/jbmc-generics/type_erasure/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
TestClass.class
3-
--function TestClass.testFunction --classpath ../../../src/java_bytecode/library/core-models.jar:.
3+
--function TestClass.testFunction --classpath `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
44
EXIT=0
55
SIGNAL=0
66
VERIFICATION SUCCESSFUL

Diff for: ‎jbmc/src/Makefile

+4-10
Original file line numberDiff line numberDiff line change
@@ -54,19 +54,13 @@ cprover_clean:
5454
dist_clean:
5555
rm -rf $(ROOT)dist
5656

57-
# extended JBMC models download, for your convenience
58-
java-models-library-download:
59-
@echo "Downloading java models library"
60-
@wget https://github.com/diffblue/java-models-library/archive/master.zip -O java-models-library.zip
61-
@unzip java-models-library.zip
62-
@rm java-models-library.zip
63-
@cp -r java-models-library-master/src java_bytecode/library
64-
@rm -r java-models-library-master
57+
setup-submodules:
58+
git submodule update --init --recursive
6559

6660
.PHONY: dist
67-
dist: java-models-library-download all
61+
dist: setup-submodules all
6862
mkdir -p $(ROOT)dist/lib
69-
cp java_bytecode/library/core-models.jar $(ROOT)dist/lib
63+
cp ../lib/java-models-library/target/core-models.jar $(ROOT)dist/lib
7064
mkdir -p $(ROOT)dist/bin
7165
cp jbmc/jbmc $(ROOT)dist/bin
7266
cp janalyzer/janalyzer $(ROOT)dist/bin

Diff for: ‎jbmc/src/java_bytecode/library/CMakeLists.txt

-30
Original file line numberDiff line numberDiff line change
@@ -1,32 +1,2 @@
1-
message(STATUS "Downloading java-models-library...")
2-
include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake")
3-
4-
# Note: 'PATCH_COMMAND' is being used instead of 'COMMAND' as
5-
# 'download_project' does not work as expected if called without
6-
# 'PATCH_COMMAND'.
7-
download_project(PROJ java_models_library
8-
URL https://github.com/diffblue/java-models-library/archive/master.zip
9-
PATCH_COMMAND cmake -E copy_directory "${CMAKE_BINARY_DIR}/java_models_library-src/src"
10-
"${JBMC_SOURCE_DIR}/java_bytecode/library/src"
11-
)
12-
13-
find_package(Java REQUIRED)
14-
include(UseJava)
15-
16-
set(CMAKE_JAVA_COMPILE_FLAGS -sourcepath "src" -d "classes" -XDignore.symbol.file)
17-
181
# create a target for the executable performing the .jar -> .inc conversion
192
add_executable(java-converter converter.cpp)
20-
21-
# create a target 'core-models.jar' that depends on all .java files in src/
22-
file(GLOB_RECURSE java_sources "src/*.java")
23-
add_jar("core-models" ${java_sources})
24-
25-
# copy 'core-models.jar' to '<PROJECT_ROOT>/jbmc/src/java_bytecode/library'.
26-
# This is needed to deal with unit tests that make use of the core-models
27-
# library. So that they can find the 'core-models.jar' in the same place as
28-
# if the project had been compiled with 'make'.
29-
add_custom_command(TARGET core-models
30-
POST_BUILD
31-
COMMAND ${CMAKE_COMMAND} -E copy "core-models.jar" ${PROJECT_SOURCE_DIR}/java_bytecode/library
32-
)

Diff for: ‎jbmc/src/java_bytecode/library/Makefile

+22-31
Original file line numberDiff line numberDiff line change
@@ -1,43 +1,34 @@
1-
.NOTPARALLEL:
2-
#javac compiles multiple classes for each source as it will compile dependent sources.
3-
#Thus we do not allow the make to run concurrently.
1+
SRC = converter.cpp \
2+
# Empty last line
43

5-
include ../../config.inc
6-
include ../../$(CPROVER_DIR)/src/config.inc
7-
include ../../$(CPROVER_DIR)/src/common
8-
9-
SOURCE_DIR := src/main/java
10-
BINARY_DIR := classes
11-
12-
FIND := find
4+
OBJ +=
135

14-
JAVAC := javac
15-
JFLAGS := -sourcepath $(SOURCE_DIR) -d $(BINARY_DIR) -XDignore.symbol.file
6+
INCLUDES=
167

17-
CLASSPATH := SOURCE_DIR
8+
LIBS =
189

19-
ALL_JAVAS := $(wildcard $(SOURCE_DIR)/*/*.java $(SOURCE_DIR)/*/*/*.java $(SOURCE_DIR)/*/*/*/*.java)
20-
ALL_CLASSES := $(patsubst $(SOURCE_DIR)/%.java,$(BINARY_DIR)/%.class,$(ALL_JAVAS))
10+
LIBRARY_DIR = ../../../lib/java-models-library
2111

22-
$(BINARY_DIR):
23-
mkdir -p $(BINARY_DIR)
24-
25-
.SUFFIXES: .java .class
12+
include ../../config.inc
13+
include ../../$(CPROVER_DIR)/src/config.inc
14+
include ../../$(CPROVER_DIR)/src/common
2615

27-
$(BINARY_DIR)/%.class: $(SOURCE_DIR)/%.java $(BINARY_DIR)
28-
$(JAVAC) $(JFLAGS) $(patsubst $(BINARY_DIR)/%.class,$(SOURCE_DIR)/%.java,$@)
16+
CLEANFILES = converter$(EXEEXT)
2917

30-
JAR := jar
31-
JARFLAGS := -cf
18+
all: library converter$(EXEEXT)
3219

33-
core-models.jar: $(BINARY_DIR) $(ALL_CLASSES)
34-
$(JAR) $(JARFLAGS) $@ -C $(BINARY_DIR) .
20+
clean: clean_library
3521

36-
CLEANFILES = core-models.jar
22+
.PHONY: clean_library
23+
clean_library:
24+
rm -rf core-models.jar
25+
if [ -d $(LIBRARY_DIR) ]; then cd $(LIBRARY_DIR); mvn clean; fi
3726

38-
all: core-models.jar
27+
.PHONY: library
28+
library:
29+
if [ -d $(LIBRARY_DIR) ]; then (cd $(LIBRARY_DIR); mvn package); cp $(LIBRARY_DIR)/target/core-models.jar .; fi
3930

40-
clean: clean_
31+
###############################################################################
4132

42-
clean_:
43-
$(RM) -Rf $(BINARY_DIR)
33+
converter$(EXEEXT): $(OBJ)
34+
$(LINKBIN)

0 commit comments

Comments
 (0)