Use submodule to download java-models-library

Author: peterschrammel

.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

@@ -328,7 +328,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 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 +349,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

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

@@ -20,7 +20,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" '
+        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" '
         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" '
 
   post_build:

buildspec.yml

@@ -13,7 +13,7 @@ phases:
   build:
     commands:
       - echo Build started on `date`
-      - make -C jbmc/src java-models-library-download
+      - make -C jbmc/src setup-submodules
       - (cd src ; make minisat2-download)
       - (cd src ; make CXX="ccache g++" -j2)
       - (cd regression ; make test)

jbmc/lib/java-models-library

@@ -1,6 +1,6 @@
 CORE
 TestClass.class
---function TestClass.testFunction --classpath ../../../src/java_bytecode/library/core-models.jar:.
+--function TestClass.testFunction --classpath ../../../lib/java-models-library/target/core-models.jar:.
 EXIT=0
 SIGNAL=0
 VERIFICATION SUCCESSFUL

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

@@ -1,9 +1,9 @@
 CORE
 test.class
---show-symbol-table --cp ../../../src/java_bytecode/library/core-models.jar:.
+--show-symbol-table --cp ../../../lib/java-models-library/target/core-models.jar:.
 ^EXIT=0$
 ^SIGNAL=0$
-^Symbol\s*\.*\: java\:\:org\.cprover\.CProver\.\<clinit\>\:\(\)V$
+^Symbol\s*\.*\: java\:\:org\.cprover\.CProver\.\<init\>\:\(\)V$
 --
 --
 tests that the core models are  being loaded by checking if the static initializer for the CProver class was

jbmc/regression/jbmc/coreModels/test.desc

@@ -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/Makefile

@@ -1,43 +1,33 @@
-.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:
+	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; fi
 
-clean: clean_
+###############################################################################
 
-clean_:
-	$(RM) -Rf $(BINARY_DIR)
+converter$(EXEEXT): $(OBJ)
+	$(LINKBIN)