JBMC: Added java-library models dependency

This commit adds a dependency to the java-models-library
(https://github.com/diffblue/java-models-library). This repository contains
models for number of classes derived from the java standard library These models
are needed to support concurrency.

This commit also contains a minor fix that removes superfluous padding
from the java_bytecode converter.

Note: src/org/cprover/CProver.java has been removed as this has been
superseded by the CProver.java in java-models-library.

Author: Degiorgio

.travis.yml

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

appveyor.yml

@@ -42,12 +42,17 @@ 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)) {
+     & appveyor downloadfile https://github.com/diffblue/java-models-library/archive/master.zip
+     & 7z x java-models-library-master.zip
+    }
     cd ..
 
 cache: deps
 
 build_script:
 - cmd: |
+    cp -r deps/java-models-library-master/src jbmc/src/java_bytecode/library
     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.yml

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

jbmc/src/Makefile

@@ -48,3 +48,13 @@ $(patsubst %, %_clean, $(DIRS)):
 .PHONY: cprover_clean
 cprover_clean:
 	$(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/src clean
+
+# extended JBMC models download, for your convenience
+
+java-models-library-download:
+	@echo "Downloading java models library"
+	@curl -L https://github.com/diffblue/java-models-library/archive/master.zip > java-models-library.tar.gz
+	@unzip java-models-library.tar.gz
+	@rm java-models-library.tar.gz
+	@cp -r java-models-library-master/src java_bytecode/library
+	@rm -r java-models-library-master

jbmc/src/java_bytecode/library/.gitignore

@@ -0,0 +1,5 @@
+src
+classes
+converter
+core-models.jar
+java_core_models.inc

jbmc/src/java_bytecode/library/CMakeLists.txt

@@ -22,3 +22,11 @@ add_custom_command(OUTPUT ${JAVA_CORE_MODELS_INC}
 # create a target 'core-models-inc' that depends on the .inc file
 add_custom_target(java-core-models-inc
     DEPENDS ${JAVA_CORE_MODELS_INC})
+
+message(STATUS "Downloading java-models-library...")
+include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake")
+download_project(PROJ java_models_library
+    URL https://github.com/diffblue/java-models-library/archive/master.zip
+    PATCH_COMMAND cmake -E copy_directory "${JBMC_BINARY_DIR}/../../java_models_library-src/src"
+      "${JBMC_SOURCE_DIR}/java_bytecode/library/src"
+)

jbmc/src/java_bytecode/library/Makefile

@@ -8,7 +8,7 @@ include ../../config.inc
 include ../../$(CPROVER_DIR)/src/config.inc
 include ../../$(CPROVER_DIR)/src/common
 
-SOURCE_DIR := src
+SOURCE_DIR := src/main/java
 BINARY_DIR := classes
 
 FIND := find

jbmc/src/java_bytecode/library/converter.cpp

@@ -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";
   src.close();
   return 0;
 }