Skip to content

Commit 9d055e2

Browse files
peterschrammelpeterschrammel
committed
Use submodule to download java-models-library
1 parent 90c56b3 commit 9d055e2

File tree

10 files changed

+37
-53
lines changed

10 files changed

+37
-53
lines changed

‎.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

‎.travis.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -328,7 +328,7 @@ jobs:
328328
name: "diffblue/cbmc"
329329
description: "Travis build of ${TRAVIS_COMMIT}"
330330
notification_email: "[email protected]"
331-
build_command_prepend: "make -C jbmc/src java-models-library-download"
331+
build_command_prepend: "make -C jbmc/src setup-submodules"
332332
build_command_prepend: "make -C src minisat2-download"
333333
build_command: "make -C src -j2; make -C jbmc/src -j2"
334334
branch_pattern: "develop"
@@ -349,7 +349,7 @@ jobs:
349349
install:
350350
- ccache -z
351351
- ccache --max-size=1G
352-
- make -C jbmc/src java-models-library-download
352+
- make -C jbmc/src setup-submodules
353353
- make -C src minisat2-download
354354
- make -C src/ansi-c library_check
355355
- make -C src/cpp library_check

‎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

‎buildspec-windows.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ phases:
2020
2121
- |
2222
$env:Path = "C:\tools\cygwin\bin;$env:Path"
23-
cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/src" '
23+
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" '
2424
cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/unit all ; exit 0" '
2525
2626
post_build:

‎buildspec.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ phases:
1313
build:
1414
commands:
1515
- echo Build started on `date`
16-
- make -C jbmc/src java-models-library-download
16+
- make -C jbmc/src setup-submodules
1717
- (cd src ; make minisat2-download)
1818
- (cd src ; make CXX="ccache g++" -j2)
1919
- (cd regression ; make test)

‎jbmc/lib/java-models-library

Submodule java-models-library added at 5fd9020

‎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 ../../../lib/java-models-library/target/core-models.jar:.
44
EXIT=0
55
SIGNAL=0
66
VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc/coreModels/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
test.class
3-
--show-symbol-table --cp ../../../src/java_bytecode/library/core-models.jar:.
3+
--show-symbol-table --cp ../../../lib/java-models-library/target/core-models.jar:.
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Symbol\s*\.*\: java\:\:org\.cprover\.CProver\.\<clinit\>\:\(\)V$
6+
^Symbol\s*\.*\: java\:\:org\.cprover\.CProver\.\<init\>\:\(\)V$
77
--
88
--
99
tests that the core models are being loaded by checking if the static initializer for the CProver class was

‎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

‎jbmc/src/java_bytecode/library/Makefile

+21-31
Original file line numberDiff line numberDiff line change
@@ -1,43 +1,33 @@
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+
if [ -d $(LIBRARY_DIR) ]; then cd $(LIBRARY_DIR); mvn clean; fi
3725

38-
all: core-models.jar
26+
.PHONY: library
27+
library:
28+
if [ -d $(LIBRARY_DIR) ]; then cd $(LIBRARY_DIR); mvn package; fi
3929

40-
clean: clean_
30+
###############################################################################
4131

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

0 commit comments

Comments
 (0)