Merge branch 'develop' into cbmc_trace_options

Author: polgreen

.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

CODING_STANDARD.md

@@ -95,6 +95,9 @@ Formatting is enforced using clang-format. For more information about this, see
 # Naming
 - Identifiers may use the characters `[a-z0-9_]` and should start with a
   lower-case letter (parameters in constructors may start with `_`).
+- Omit names of parameters or exception objects when they are not used. If
+  parameter names help documenting an interface, keep the name and use
+  `(void)parameter_name;` in the body of the method.
 - Use American spelling for identifiers.
 - Separate basic words by `_`
 - Avoid abbreviations (e.g. prefer `symbol_table` to `st`).

COMPILING.md

@@ -66,7 +66,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
 
 5. To compile JBMC, do
    ```
-   make -C jbmc/src java-models-library-download
+   make -C jbmc/src setup-submodules
    make -C jbmc/src
    ```
 
@@ -92,7 +92,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
    ```
 4. To compile JBMC, type
    ```
-   gmake -C jbmc/src java-models-library-download
+   gmake -C jbmc/src setup-submodules
    gmake -C jbmc/src
    ```
 
@@ -118,7 +118,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
    ```
 4. To compile JBMC, do
    ```
-   gmake -C jbmc/src java-models-library-download
+   gmake -C jbmc/src setup-submodules
    gmake -C jbmc/src
    ```
 
@@ -144,7 +144,7 @@ Follow these instructions:
    ```
 4. To compile JBMC, do
    ```
-   make -C jbmc/src java-models-library-download
+   make -C jbmc/src setup-submodules
    make -C jbmc/src
    ```
 
@@ -185,9 +185,9 @@ Follow these instructions:
    make -C src DOWNLOADER=wget minisat2-download
    make -C src
    ```
-5. To compile JMBC, open the Cygwin shell and type
+5. To compile JBMC, open the Cygwin shell and type
    ```
-   make -C jbmc/src java-models-library-download
+   make -C jbmc/src setup-submodules
    make -C jbmc/src
    ```
 
@@ -240,7 +240,11 @@ require manual modification of build files.
 2. Navigate to the *top level* folder of the project. This is different from
    the Makefile build, which requires you to navigate to the `src` directory
    first.
-3. Generate build files with CMake:
+3. Update git submodules:
+   ```
+   git submodule update --init
+   ```
+4. Generate build files with CMake:
    ```
    cmake -H. -Bbuild
    ```
@@ -264,7 +268,7 @@ require manual modification of build files.
    Finally, to enable building universal binaries on macOS, you can pass the
    flag `-DCMAKE_OSX_ARCHITECTURES=i386;x86_64`. If you don't supply this flag,
    the build will just be for the architecture of your machine.
-4. Run the build:
+5. Run the build:
    ```
    cmake --build build
    ```

appveyor.yml

@@ -2,7 +2,6 @@ version: 1.0.{build}
 image: Visual Studio 2013
 clone_depth: 50
 environment:
-  BUILD_ENV: MSVC
   PATH: C:\projects\cbmc\deps\bin;%PATH%
   INCLUDE: C:\projects\cbmc\deps\include
 install:
@@ -43,23 +42,18 @@ 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
-    sed -i "s/BUILD_ENV[ ]*=.*/BUILD_ENV = MSVC/" src/config.inc
-    make -C src -j2
-    make -C jbmc/src -j2
+    make -C src -j2 BUILD_ENV=MSVC
+    make -C jbmc/src -j2 BUILD_ENV=MSVC
 
 test_script:
 - cmd: |
@@ -81,19 +75,18 @@ test_script:
     rmdir /s /q goto-instrument\slice08
     cd ..
 
-    make -C regression test
+    make -C regression test BUILD_ENV=MSVC
 
-    make -C unit all -j2
-    make -C unit test
+    make -C unit all -j2 BUILD_ENV=MSVC
+    make -C unit test BUILD_ENV=MSVC
 
     cd jbmc/regression
     rmdir /s /q jbmc\VarLengthArrayTrace1
     rmdir /s /q jbmc\classpath1
     rmdir /s /q jbmc\jar-file3
-    rmdir /s /q jbmc\tableswitch2
     cd ../..
 
-    make -C jbmc/regression test
+    make -C jbmc/regression test BUILD_ENV=MSVC
 
-    make -C jbmc/unit all -j2
-    make -C jbmc/unit test
+    make -C jbmc/unit all -j2 BUILD_ENV=MSVC
+    make -C jbmc/unit test BUILD_ENV=MSVC

buildspec-windows.yml

@@ -8,20 +8,19 @@ phases:
 
   build:
     commands:
-      - 'C:\tools\cygwin\bin\sed -i "s/BUILD_ENV[ ]*=.*/BUILD_ENV = MSVC/" src/config.inc'
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
         C:\tools\cygwin\bin\bash -c "make -C src minisat2-download DOWNLOADER=wget"
 
       - |
         $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 src" '
-        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C unit all" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C 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 unit all BUILD_ENV=MSVC" '
 
       - |
         $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/unit all ; exit 0" '
+        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" '
 
   post_build:
     commands:
@@ -46,22 +45,27 @@ phases:
         Remove-Item goto-instrument\slice08 -Force -Recurse
         Remove-Item goto-analyzer/constant_propagation_nondet_rounding_mode -Force -Recurse
         cd ..
+        cd jbmc/regression
+        Remove-Item jbmc\VarLengthArrayTrace1 -Force -Recurse
+        Remove-Item jbmc\classpath1 -Force -Recurse
+        Remove-Item jbmc\jar-file3 -Force -Recurse
+        cd ../..
 
       - |
         $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 -C regression test" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression test BUILD_ENV=MSVC" '
 
       - |
         $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 -C unit test" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C unit test BUILD_ENV=MSVC" '
 
       - |
         $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 -C jbmc/regression test ; exit 0" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/regression test BUILD_ENV=MSVC" '
 
       - |
         $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 -C jbmc/unit test ; exit 0" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/unit test BUILD_ENV=MSVC" '
 
 artifacts:
   files:

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/README.md

@@ -27,10 +27,16 @@ JBMC compiles CBMC as part of its build process and as such has all the pre-requ
 Compilation
 ===========
 
-To compile you need to run the command:
+Before compilation, run the commands:
+
+```bash
+make -C src DOWNLOADER=wget minisat2-download
+make -C jbmc/src setup-submodules
+```
+
+Then compile using:
 
 ```bash
-make -C jbmc/src java-models-library-download
 make -C jbmc/src
 ```
 

jbmc/lib/java-models-library

@@ -1,32 +1,27 @@
 # For the best possible utilisation of multiple cores when
 # running tests in parallel, it is important that these directories are
 # listed with decreasing runtimes (i.e. longest running at the top)
-DIRS = janalzyer-taint \
+DIRS = janalyzer-taint \
        jbmc \
        jbmc-concurrency \
        jbmc-cover \
        jbmc-inheritance \
        jbmc-strings \
        jdiff \
-       string-smoke-tests \
+       strings-smoke-tests \
        jbmc-generics \
        # Empty last line
 
-# Tests under goto-gcc cannot be run on Windows, so appveyor.yml unlinks
-# the entire directory under Windows. This variable will contain the list
-# of directories that actually exist on the current platform.
-PLATFORM_DIRS = $(wildcard $(DIRS))
-
 # Run all test directories in sequence
 .PHONY: test
 test:
-	@for dir in $(PLATFORM_DIRS); do \
+	@for dir in $(DIRS); do \
 		$(MAKE) "$$dir" || exit 1; \
 	done;
 
 # Pattern to execute a single test suite directory
-.PHONY: $(PLATFORM_DIRS)
-$(PLATFORM_DIRS):
+.PHONY: $(DIRS)
+$(DIRS):
 	@echo "Running $@..." ;
 	$(MAKE) -C "$@" test || exit 1;
 
@@ -42,7 +37,7 @@ test-parallel:
 		--linebuffer \
 		--jobs $(JOBS) \
 		$(MAKE) "{}" \
-		::: $(PLATFORM_DIRS)
+		::: $(DIRS)
 
 
 .PHONY: clean

jbmc/regression/Makefile

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/get-current-thread/test.desc

@@ -7,5 +7,3 @@ file AbstractTest.java line 18 .* SATISFIED
 file AbstractTest.java line 19 .* SATISFIED
 file AbstractTest.java line 20 .* SATISFIED
 file AbstractTest.java line 21 .* SATISFIED
-
-

jbmc/regression/jbmc-cover/generics/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/regression/jbmc-generics/type_erasure/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file test.java line 8 .* SUCCESS$

jbmc/regression/jbmc-strings/CharacterGetNumericValue/test.desc

@@ -1,12 +1,12 @@
 CORE
 Test.class
---function Test.testme
+--no-refine-strings --function Test.testme
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 type mismatch
 --
 Before cbmc#2472 this would assume that StringBuilder's direct parent was
-java.lang.Object, causing a type mismatch when --refine-strings was not in use
+java.lang.Object, causing a type mismatch when --no-refine-strings was in use
 (which at the time would assume that parent-child relationship)

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 RegexMatches01.class
---refine-strings --string-max-length 1000 --unwind 100
+--max-nondet-string-length 1000 --unwind 100
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$