Use submodule to download java-models-library

.gitmodules

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

.travis.yml

@@ -229,6 +229,7 @@ jobs:
         - ccache -z
         - ccache --max-size=1G
         - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5'
+        - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
 
@@ -254,6 +255,7 @@ jobs:
         - ccache -z
         - ccache --max-size=1G
         - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7'
+        - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
 
@@ -287,6 +289,7 @@ jobs:
         - ccache -z
         - ccache --max-size=1G
         - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/clang++-6.0' '-DCMAKE_CXX_FLAGS=-Qunused-arguments'
+        - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
 
@@ -305,6 +308,7 @@ jobs:
         - ccache -z
         - ccache --max-size=1G
         - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
+        - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
 
@@ -328,7 +332,7 @@ jobs:
             name: "diffblue/cbmc"
             description: "Travis build of ${TRAVIS_COMMIT}"
           notification_email: "[email protected]"
-          build_command_prepend: "make -C jbmc/src java-models-library-download"
+          build_command_prepend: "make -C jbmc/src setup-submodules"
           build_command_prepend: "make -C src minisat2-download"
           build_command: "make -C src -j2; make -C jbmc/src -j2"
           branch_pattern: "develop"
@@ -349,7 +353,7 @@ jobs:
 install:
   - ccache -z
   - ccache --max-size=1G
-  - make -C jbmc/src java-models-library-download
+  - make -C jbmc/src setup-submodules
   - make -C src minisat2-download
   - make -C src/ansi-c library_check
   - make -C src/cpp library_check

CMakeLists.txt

@@ -81,6 +81,7 @@ set_target_properties(
     xml
 
     java_bytecode
+    java-models-library
     jbmc
     jbmc-lib
     janalyzer

appveyor.yml

@@ -42,17 +42,13 @@ install:
      & 7z x minisat2_2.2.1.orig.tar.gz
      &7z x minisat2_2.2.1.orig.tar
     }
-    if (!(Test-Path java-models-library-master\.gitignore)) {
-     & appveyor downloadfile https://github.com/diffblue/java-models-library/archive/master.zip -FileName jml.zip
-     & 7z x jml.zip
-    }
     cd ..
 
 cache: deps
 
 build_script:
 - cmd: |
-    cp -r deps/java-models-library-master/src jbmc/src/java_bytecode/library
+    make -C jbmc/src setup-submodules
     cp -r deps/minisat2-2.2.1 minisat-2.2.1
     patch -d minisat-2.2.1 -p1 < scripts/minisat-2.2.1-patch
     call "C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\vcvarsall.bat" x64

buildspec-windows.yml

@@ -19,7 +19,7 @@ phases:
 
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
-        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" '
+        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" '
         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" '
 
   post_build:

buildspec.yml

@@ -15,7 +15,7 @@ phases:
     commands:
       - echo Build started on `date`
       - make -C src minisat2-download
-      - make -C jbmc/src java-models-library-download
+      - make -C jbmc/src setup-submodules
       - make -C src CXX="ccache g++" -j2
       - make -C unit CXX="ccache g++" -j2
       - make -C jbmc/src CXX="ccache g++" -j2

jbmc/CMakeLists.txt

@@ -1,3 +1,9 @@
 add_subdirectory(regression)
 add_subdirectory(src)
 add_subdirectory(unit)
+
+add_custom_target(java-models-library ALL
+    COMMAND mvn package
+    COMMAND cp target/core-models.jar ${CMAKE_CURRENT_SOURCE_DIR}/src/java_bytecode/library/
+    WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library
+)

jbmc/regression/jbmc-generics/type_erasure/test.desc

@@ -1,6 +1,6 @@
 CORE
 TestClass.class
---function TestClass.testFunction --classpath ../../../src/java_bytecode/library/core-models.jar:.
+--function TestClass.testFunction --classpath `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 EXIT=0
 SIGNAL=0
 VERIFICATION SUCCESSFUL

jbmc/src/Makefile

@@ -54,19 +54,13 @@ cprover_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
+setup-submodules:
+	git submodule update --init --recursive
 
 .PHONY: dist
-dist: java-models-library-download all
+dist: setup-submodules all
 	mkdir -p $(ROOT)dist/lib
-	cp java_bytecode/library/core-models.jar $(ROOT)dist/lib
+	cp ../lib/java-models-library/target/core-models.jar $(ROOT)dist/lib
 	mkdir -p $(ROOT)dist/bin
 	cp jbmc/jbmc $(ROOT)dist/bin
 	cp janalyzer/janalyzer $(ROOT)dist/bin

jbmc/src/java_bytecode/library/CMakeLists.txt

@@ -1,32 +1,2 @@
-message(STATUS "Downloading java-models-library...")
-include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake")
-
-#  Note: 'PATCH_COMMAND' is being used instead of 'COMMAND' as
-# 'download_project' does not work as expected if called without
-# 'PATCH_COMMAND'.
-download_project(PROJ java_models_library
-    URL https://github.com/diffblue/java-models-library/archive/master.zip
-    PATCH_COMMAND cmake -E copy_directory "${CMAKE_BINARY_DIR}/java_models_library-src/src"
-      "${JBMC_SOURCE_DIR}/java_bytecode/library/src"
-)
-
-find_package(Java REQUIRED)
-include(UseJava)
-
-set(CMAKE_JAVA_COMPILE_FLAGS -sourcepath "src" -d "classes" -XDignore.symbol.file)
-
 # create a target for the executable performing the .jar -> .inc conversion
 add_executable(java-converter converter.cpp)
-
-# create a target 'core-models.jar' that depends on all .java files in src/
-file(GLOB_RECURSE java_sources "src/*.java")
-add_jar("core-models" ${java_sources})
-
-# 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. So that they can find the 'core-models.jar' in the same place as
-# if the project had been compiled with 'make'.
-add_custom_command(TARGET core-models
-                   POST_BUILD
-                   COMMAND ${CMAKE_COMMAND} -E copy "core-models.jar" ${PROJECT_SOURCE_DIR}/java_bytecode/library
-                  )

jbmc/src/java_bytecode/library/Makefile

@@ -1,43 +1,34 @@
-.NOTPARALLEL:
-#javac compiles multiple classes for each source as it will compile dependent sources.
-#Thus we do not allow the make to run concurrently.
+SRC = converter.cpp \
+      # Empty last line
 
-include ../../config.inc
-include ../../$(CPROVER_DIR)/src/config.inc
-include ../../$(CPROVER_DIR)/src/common
-
-SOURCE_DIR := src/main/java
-BINARY_DIR := classes
-
-FIND := find
+OBJ +=
 
-JAVAC := javac
-JFLAGS := -sourcepath $(SOURCE_DIR) -d $(BINARY_DIR) -XDignore.symbol.file
+INCLUDES=
 
-CLASSPATH := SOURCE_DIR
+LIBS =
 
-ALL_JAVAS := $(wildcard $(SOURCE_DIR)/*/*.java $(SOURCE_DIR)/*/*/*.java $(SOURCE_DIR)/*/*/*/*.java)
-ALL_CLASSES := $(patsubst $(SOURCE_DIR)/%.java,$(BINARY_DIR)/%.class,$(ALL_JAVAS))
+LIBRARY_DIR = ../../../lib/java-models-library
 
-$(BINARY_DIR):
-	mkdir -p $(BINARY_DIR)
-
-.SUFFIXES: .java .class
+include ../../config.inc
+include ../../$(CPROVER_DIR)/src/config.inc
+include ../../$(CPROVER_DIR)/src/common
 
-$(BINARY_DIR)/%.class: $(SOURCE_DIR)/%.java $(BINARY_DIR)
-	$(JAVAC) $(JFLAGS) $(patsubst $(BINARY_DIR)/%.class,$(SOURCE_DIR)/%.java,$@)
+CLEANFILES = converter$(EXEEXT)
 
-JAR := jar
-JARFLAGS := -cf
+all: library converter$(EXEEXT)
 
-core-models.jar: $(BINARY_DIR) $(ALL_CLASSES)
-	$(JAR) $(JARFLAGS) $@ -C $(BINARY_DIR) .
+clean: clean_library
 
-CLEANFILES = core-models.jar
+.PHONY: clean_library
+clean_library:
+	rm -rf core-models.jar
+	if [ -d $(LIBRARY_DIR) ]; then cd $(LIBRARY_DIR); mvn clean; fi
 
-all: core-models.jar
+.PHONY: library
+library:
+	if [ -d $(LIBRARY_DIR) ]; then (cd $(LIBRARY_DIR); mvn package); cp $(LIBRARY_DIR)/target/core-models.jar .; fi
 
-clean: clean_
+###############################################################################
 
-clean_:
-	$(RM) -Rf $(BINARY_DIR)
+converter$(EXEEXT): $(OBJ)
+	$(LINKBIN)