Squashed 'cbmc/' changes from 2af8433..54f3731

54f3731 Merge pull request diffblue#2610 from smowton/smowton/fix/ssa-trace-unreachable-values
6397f62 Merge pull request diffblue#2626 from qaphla/local_bitvector_analysis_fix
0c0e288 Merge pull request diffblue#2423 from tautschnig/vs-negation
e90b61b Transform float_utils unit test to use CATCH and enable it
8b2bd7b Convert to signed type to make negation meaningful
7823d9c Merge pull request diffblue#2606 from diffblue/ms_cl_options
0f60b26 Merge pull request diffblue#2627 from diffblue/cleanup-ansi-c-scanner
f33459f Merge pull request diffblue#2529 from tautschnig/debian1
1927fb2 remove bitvector and bitvector_u rules
1e07546 Fixed secondary issues arising from local_bitvector_analysis fix.
131e525 Fixed a bug in local_bitvector_analysis wherein an expression's ID was used in place of the expression's type's ID.
501546a SSA trace: don't concretise steps that will subsequently be dropped
709b45f Merge pull request diffblue#2591 from allredj/log-suffix-in-testpl
f3630f0 Merge pull request diffblue#2612 from svorenova/multidim_arrays_tg3821_util
c010edb Merge pull request diffblue#2623 from diffblue/cbmc-empty-message
d5adef5 Merge pull request diffblue#2624 from diffblue/va_arg_mode
3e3303d symbols for va_args need a mode
398dd39 cbmc: avoid an empty message during result reporting
8bca5cd Merge pull request diffblue#2585 from smowton/smowton/admin/java-clean-deref-tests
a0e339d Disable broken string test
d0cf433 Strengthen local_safe_pointers to handle common Java operations
e7b1a8a Merge pull request diffblue#2616 from smowton/smowton/admin/ai-unit-test
738ecad Merge pull request diffblue#2621 from diffblue/amazon-linux-instructions
4156283 Add test for ait framework
08bd1a8 Merge pull request diffblue#2596 from martin-cs/feature/context-sensitive-ait-merge-1
c572866 Use can_cast_type instead of raw type id check
a1ab7a6 Improve documentation for java array types
745670b instructions for Amazon Linux
299417b Merge pull request diffblue#2614 from chrisr-diffblue/is_zero_bitfield_support
0c8eff6 Merge pull request diffblue#2598 from mmuesly/feature_posix_memalign
fad7735 Merge pull request diffblue#2613 from NathanJPhillips/cleanup/irep_ids-def-not-h
e34fc57 Merge pull request diffblue#2600 from peterschrammel/doxygen-graphviz
54cc818 clang-format fixups
9986ea1 Make exprt::is_zero() support bitfields
dbf4384 Merge pull request diffblue#2605 from NathanJPhillips/feature/cast-for-code_typet
7798aaa Updated comment for the fact that IDs are defined in def files now
b72b968 Remove unused function
e66f76f Add a check functions for (multi-dimensional) array types
f4f4190 Added can_cast_type implementation for code_typet
f6c34f2 Merge pull request diffblue#2603 from smowton/smowton/fix/stub-string-lengths
9c9c375 two further Visual Studio CL options
05bebb7 Merge pull request diffblue#2595 from thk123/doc/use-can-cast
9a75c65 Merge pull request diffblue#2597 from allredj/update-jbmc-gitignore
c98688b Fix stub string lengths
819560f Merge pull request diffblue#2601 from owen-jones-diffblue/owen-jones-diffblue/update-codeowners-3
39323e0 Remove code owners from low-risk files
8f8052a Make directories match from root
1a36a21 Install graphviz for doxygen job on travis
3e0b2a5 Doxygen the comments describing the abstract domain interface.
4f8d445 Upgrade from a warning in the comments to a protected constructor.
2b9c880 Clang format the domain files.
028d8b6 Add a method to convert the domain to a predicate to the basic domain API.
918e947 Expand the comments describing the base domain interface.
f60027b Move the interface of domains to it's own header file.
15aa61f Adding support for posix_memalign from the stdlib in c.
ba01589 Add guidelines for using irepts in the code base
37fc4e6 Update jbmc gitignore
ec79bdd Merge pull request diffblue#2385 from polgreen/aggressive_slicer_v2
78b7119 Merge pull request diffblue#2491 from diffblue/std_code_constructors
a99c4ff Merge pull request diffblue#2497 from diffblue/simplify_byte_extract_fix
8c7dc17 make comment // not /*
ea085d3 move aggressive slicer options into macro
aa4848d Apply clang format to includes in goto_instrument_parse_options
4ac9199 Aggressive slicer
2954205 aggressive slicer regression tests
de7e1af call graph helper functions
357358d remove mistake in grapht
c7457fb Merge pull request diffblue#2543 from tautschnig/vs-unsigned-byte-swap
0e72433 Merge pull request diffblue#2516 from polgreen/cbmc_trace_options
2e90035 Merge pull request diffblue#2590 from peterschrammel/use-proper-irep-ids
a354235 Merge pull request diffblue#2592 from NathanJPhillips/cleanup/fix-typo-in-comment
59b1a9e Fix a small typo in a comment that I happened to come across
282468c Print log suffix when running tests
c98c9df Merge branch 'develop' into cbmc_trace_options
12e970b Use irep ids for #comments
569c854 Merge pull request diffblue#2489 from diffblue/fix-empty-indexset
993735b Merge pull request diffblue#2507 from mgudemann/bugfix/java/keep-typecasts-on-stack
a63212e Add regression test for stack variables with typecasts
6f63050 Simplify stack element replacement loop
731c69e Keep expressions unchanged when adding temporary variables
d10e44d Merge pull request diffblue#2586 from hannes-steffenhagen-diffblue/fix-json_unit_test
8d6bfdd Merge pull request diffblue#2575 from nmanthey/upstream-ls_parse
2d14b22 Merge pull request diffblue#2545 from tautschnig/vs-unnecessary
ff0414e Merge pull request diffblue#2546 from tautschnig/vs-wmm-int
ed48122 Make json parser unit tests independent of working directory
14dc11e Merge pull request diffblue#2495 from diffblue/aws-codebuild-windows-jbmc-tests
cefdc21 Merge pull request diffblue#2579 from peterschrammel/clean-up-java-options
64a63a0 Merge pull request diffblue#2584 from diffblue/fp-constant-folding
44cfeb9 Clean up redundant specification of CBMC option
38fe61e Trim JBMC help text width to 80 chars
080fc91 Break overlong lines in help text
ebae090 Deactivate smt1 option in JBMC
04fcc5b Check that string options are used with strings turned on
0520732 Use default options in JBMC
e4cfb04 Remove built-in-assertions option from JBMC
0d924ce Remove error-label option from JBMC
35f69f0 Remove GOTO_CHECK options from JBMC
86d4fec Remove --refine-strings from tests
7ef8a0e Remove obsolete string-max-length option
e5e5e9e remove unneeded NOLINT
9449ac7 Encapsulate constraints for equals
d74672b Use const references in string_constraintt
fdf14f5 Add invariants on the sign of string_constraintt bounds
16052f8 Move string_constraintt constructor to cpp
f01c03c Fix string_constraintt bound values
8edc5ee C front-end: constant folding for floating-point
f795ef9 Remove trailing newlines that trip up regex on Windows
53d24e5 the jbmc tests now work on Windows
f9c5faf adjust_float_expressions can now take a rounding mode argument
6ccce5b Merge pull request diffblue#2521 from svorenova/array_element_type_util
201ba8c Merge pull request diffblue#2581 from romainbrenguier/refactor/to_code
e4b8c44 Clean-up in gen_nondet_instruction_info
bb7ea78 Merge pull request diffblue#2528 from tautschnig/dev-null
f10badb Add functions to retrieve a reference to the java array element type
7f8b2be Merge pull request diffblue#2582 from jeannielynnmoulton/jeannie/parse-bridge-flag-for-thk123
1f62596 Clean-up get_return_lhs
8966f09 Merge pull request diffblue#2560 from tautschnig/force-inline
cb587a9 Adding unit test for checking bridge methods attribute is parsed correctly
efadba2 Read the bride flag for methods
26781a6 Remove unnecessary cast to_code
a18b32d Merge pull request diffblue#2571 from jeannielynnmoulton/jeannie/InnerClassAccessibility
c959c3f Tests get_outer_class with deeply nested classes.
8201c19 Parse and capture outer class for inner classes.
87c2a68 Merge pull request diffblue#2577 from owen-jones-diffblue/owen-jones-diffblue/make-linter-happier
a1b9e07 Fix whitespace errors and a typo from diffblue#2505
45eae64 Merge pull request diffblue#2505 from owen-jones-diffblue/owen-jones-diffblue/fix/convert-nondet
6d9e805 Make convert_java_nondet more general
70887e2 Merge pull request diffblue#2564 from tautschnig/vs-java-parse-tree
6c5ecec Merge pull request diffblue#2570 from johnnonweiler/doc-git-submodule-update
d5ea306 ls_parse: improve debugging by printing a trace
17bc726 ls_parse: Allow handling unknown blocks
aad1692 Add minisat download to jbmc/README.md
f7ddb02 Remove --recursive from git submodule update
206f7fb Include submodule update in jbmc/README.md
d5f3c32 Fix a typo JMBC->JBMC
b5075d7 Document git submodule update in COMPILING.md
9b9aecf Remove unused macro BUFSIZE
0146874 Make all unicode operations use native endianness
8d93087 Move unicode unit test to CATCH and enable it
680227e Explicit unsigned -> uint16_t casts to avoid conversion warnings
ea9dc15 goto-gcc: run original compiler even when output is /dev/null
0a990ef Do not (unnecessarily) require preprocessing for fixed 32/64 bit regression tests
0c15fed Cleanup java_bytecode_parse_treet: all members are public, no virtual tables required
36d13f7 Support Visual Studio's __forceinline
5953f6a goto-instrument/wmm: explicit conversion of bool to 0/1
6dc6ea9 Avoid unncessary signed/unsigned conversion
081f743 use proper constructor for code_assertt
8e44191 use proper constructor for code_expressiont
47f5405 use proper constructor for side_effect_expr_function_callt
bf02ec7 use proper constructor for code_declt
9fa0733 use proper constructor for codet
dbbd568 mark various 'partial constructors' as deprecated, and introduce complete ones
180e066 add option to show code in CBMC trace
4fbc10d Add option to show function calls  and returns in CBMC trace
f532b4b allow unsigned long instead of unsigned in regression test for hex_trace
94cacc6 represent numerical values in CBMC trace in hex
fc4aab3 avoid non-termination of simplify_exprt::simplify_byte_extract when given array_of

git-subtree-dir: cbmc
git-subtree-split: 54f3731

Author: smowton

.gitignore

@@ -111,10 +111,10 @@ src/clobber/clobber
 src/clobber/clobber.exe
 src/big-int/test-bigint
 src/big-int/test-bigint.exe
-jbmc/src/jbmc/janalyzer
-jbmc/src/jbmc/janalyzer.exe
-jbmc/src/jbmc/jdiff
-jbmc/src/jbmc/jdiff.exe
+jbmc/src/janalyzer/janalyzer
+jbmc/src/janalyzer/janalyzer.exe
+jbmc/src/jdiff/jdiff
+jbmc/src/jdiff/jdiff.exe
 jbmc/src/jbmc/jbmc
 jbmc/src/jbmc/jbmc.exe
 

.travis.yml

@@ -57,6 +57,7 @@ jobs:
           packages:
             - cmake
             - google-cloud-sdk
+            - graphviz
       cache:
         directories:
           - ${TRAVIS_BUILD_DIR}/doxygen/build/bin
@@ -101,7 +102,6 @@ jobs:
             - g++-5
             - libubsan0
             - parallel
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -136,7 +136,6 @@ jobs:
             - libwww-perl
             - g++-5
             - libubsan0
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -165,7 +164,6 @@ jobs:
             - libstdc++-5-dev
             - libubsan0
             - parallel
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -194,7 +192,6 @@ jobs:
             - g++-5
             - libstdc++-5-dev
             - libubsan0
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -220,7 +217,6 @@ jobs:
             - ubuntu-toolchain-r-test
           packages:
             - g++-5
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
@@ -246,7 +242,6 @@ jobs:
             - ubuntu-toolchain-r-test
           packages:
             - g++-7
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         - ln -s /usr/bin/gcc-7 bin/gcc
@@ -278,7 +273,6 @@ jobs:
             - libstdc++-5-dev
             - libubsan0
             - parallel
-            - libc6-dev-i386
       before_install:
         - mkdir bin
         # Use gcc/g++ 5 for tests, as Clang doesn't work yet

CODEOWNERS

@@ -3,58 +3,58 @@
 
 # These files should rarely change
 
-src/big-int/ @kroening
-src/ansi-c/ @kroening @tautschnig
-src/assembler/ @kroening @tautschnig
-src/goto-cc/ @kroening @tautschnig
-src/linking/ @kroening @tautschnig
-src/memory-models/ @kroening @tautschnig
-src/goto-symex/ @kroening @tautschnig @peterschrammel
-src/json/ @kroening @tautschnig @peterschrammel
-src/langapi/ @kroening @tautschnig @peterschrammel
-src/xmllang/ @kroening @tautschnig @peterschrammel
-src/nonstd/ @smowton @peterschrammel
-src/solvers/cvc @martin-cs @kroening
-src/solvers/flattening @martin-cs @kroening @tautschnig @peterschrammel
-src/solvers/floatbv @martin-cs @kroening
-src/solvers/miniBDD @tautschnig @kroening
-src/solvers/prop @martin-cs @kroening @tautschnig @peterschrammel
-src/solvers/sat @martin-cs @kroening @tautschnig @peterschrammel
-src/solvers/smt2 @martin-cs @tautschnig @peterschrammel
-jbmc/src/miniz/ @smowton @mgudemann @peterschrammel
+/src/big-int/ @kroening
+/src/ansi-c/ @kroening @tautschnig
+/src/assembler/ @kroening @tautschnig
+/src/goto-cc/ @kroening @tautschnig
+/src/linking/ @kroening @tautschnig
+/src/memory-models/ @kroening @tautschnig
+/src/goto-symex/ @kroening @tautschnig @peterschrammel
+/src/json/ @kroening @tautschnig @peterschrammel
+/src/langapi/ @kroening @tautschnig @peterschrammel
+/src/xmllang/ @kroening @tautschnig @peterschrammel
+/src/nonstd/ @smowton @peterschrammel
+/src/solvers/cvc @martin-cs @kroening
+/src/solvers/flattening @martin-cs @kroening @tautschnig @peterschrammel
+/src/solvers/floatbv @martin-cs @kroening
+/src/solvers/miniBDD @tautschnig @kroening
+/src/solvers/prop @martin-cs @kroening @tautschnig @peterschrammel
+/src/solvers/sat @martin-cs @kroening @tautschnig @peterschrammel
+/src/solvers/smt2 @martin-cs @tautschnig @peterschrammel
+/jbmc/src/miniz/ @smowton @mgudemann @peterschrammel
 
 
 # These files change frequently and changes are high-risk
 
-src/cbmc/ @smowton @kroening @tautschnig @peterschrammel
-src/goto-programs/ @smowton @kroening @tautschnig @peterschrammel @pkesseli
-src/util/ @smowton @kroening @tautschnig @peterschrammel @pkesseli
-src/solvers/refinement @martin-cs @romainbrenguier @peterschrammel
-jbmc/src/java_bytecode/ @smowton @mgudemann @thk123 @cristina-david @cesaro @pkesseli @NathanJPhillips @peterschrammel
-src/analyses/ @martin-cs @peterschrammel @chrisr-diffblue @thk123 @smowton
-src/pointer-analysis/ @martin-cs @peterschrammel @chrisr-diffblue @smowton
+/src/cbmc/ @smowton @kroening @tautschnig @peterschrammel
+/src/goto-programs/ @smowton @kroening @tautschnig @peterschrammel @pkesseli
+/src/util/ @smowton @kroening @tautschnig @peterschrammel @pkesseli
+/src/solvers/refinement @martin-cs @romainbrenguier @peterschrammel
+/jbmc/src/java_bytecode/ @smowton @mgudemann @thk123 @cristina-david @cesaro @pkesseli @NathanJPhillips @peterschrammel
+/src/analyses/ @martin-cs @peterschrammel @chrisr-diffblue @thk123 @smowton
+/src/pointer-analysis/ @martin-cs @peterschrammel @chrisr-diffblue @smowton
 
 
 # These files change frequently and changes are medium-risk
 
-src/goto-analyzer/ @martin-cs @chrisr-diffblue @peterschrammel
-src/goto-instrument/ @martin-cs @chrisr-diffblue @peterschrammel
-src/goto-diff/ @tautschnig @peterschrammel
-jbmc/src/jbmc/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
-jbmc/src/janalyzer/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
-jbmc/src/jdiff/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
-src/cpp/ @kroening @tautschnig @peterschrammel
+/src/goto-analyzer/ @martin-cs @chrisr-diffblue @peterschrammel
+/src/goto-instrument/ @martin-cs @chrisr-diffblue @peterschrammel
+/src/goto-diff/ @tautschnig @peterschrammel
+/jbmc/src/jbmc/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
+/jbmc/src/janalyzer/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
+/jbmc/src/jdiff/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
+/src/cpp/ @kroening @tautschnig @peterschrammel
 
 
 # These files change frequently and changes are low-risk
 
-src/util/irep_ids.def @diffblue/cbmc-developers
+/src/util/irep_ids.def
 
-unit/ @diffblue/cbmc-developers
-regression/ @diffblue/cbmc-developers
-jbmc/unit/ @diffblue/cbmc-developers
-jbmc/regression/ @diffblue/cbmc-developers
+/unit/
+/regression/
+/jbmc/unit/
+/jbmc/regression/
 
-scripts/ @diffblue/devops @thk123 @forejtv @peterschrammel
-.travis.yml @diffblue/devops @thk123 @forejtv @peterschrammel
-appveyor.yml @diffblue/devops @thk123 @forejtv @peterschrammel
+/scripts/ @diffblue/devops @thk123 @forejtv @peterschrammel
+/.travis.yml @diffblue/devops @thk123 @forejtv @peterschrammel
+/appveyor.yml @diffblue/devops @thk123 @forejtv @peterschrammel

CODING_STANDARD.md

@@ -197,6 +197,12 @@ Formatting is enforced using clang-format. For more information about this, see
   which safely manages the pointer. As such, `new` should only be used in
   constructors, and `delete` in destructors. Never use `malloc` or `free`.
 
+# CProver conventions
+- Avoid if at all possible using irept methods like `get(ID_name)`, instead cast
+  to a derived type (e.g. `class_typet`) and use the wrapper method `get_name`
+- Use `can_cast_type`/`can_cast_expr` instead of directly checking the `id()`
+  of an `irept`.
+
 # Architecture-specific code
 - Avoid if possible.
 - Use `__LINUX__`, `__MACH__`, and `_WIN32` to distinguish the architectures.

COMPILING.md

@@ -29,6 +29,11 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
    ```
    Note that you need g++ version 5.0 or newer.
 
+   On Amazon Linux and similar distributions, do as root:
+   ```
+   yum install gcc72-c++ flex bison perl-libwww-perl patch
+   ```
+
    To compile JBMC, you additionally need the JDK and the java-models-library.
    For the JDK, on Debian-like distributions, do as root:
    ```
@@ -66,7 +71,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 +97,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 +123,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 +149,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 +190,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 +245,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 +273,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

@@ -84,7 +84,6 @@ test_script:
     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 BUILD_ENV=MSVC

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 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" '
+        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:
@@ -45,6 +45,11 @@ 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"
@@ -56,11 +61,11 @@ 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 -C jbmc/regression test BUILD_ENV=MSVC ; 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 BUILD_ENV=MSVC ; 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:

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/regression/jbmc-cover/generics/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-strings/CharacterGetNumericValue/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/NondetStringBuilderAndBuffer/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/RegexMatches01/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$

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

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

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

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

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

@@ -1,6 +1,6 @@
 FUTURE
 RegexSubstitution02.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$