Merge develop 20170914

.travis.yml

@@ -39,20 +39,6 @@ jobs:
       # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
       env: COMPILER="ccache g++-5"
 
-    # Alpine Linux with musl-libc using g++
-    - stage: Test different OS/CXX/Flags
-      os: linux
-      sudo: required
-      compiler: gcc
-      cache: ccache
-      services:
-        - docker
-      before_install:
-        - docker pull diffblue/cbmc-builder:alpine-0.0.3
-      env:
-        - PRE_COMMAND="docker run -v ${TRAVIS_BUILD_DIR}:/cbmc -v ${HOME}/.ccache:/root/.ccache diffblue/cbmc-builder:alpine-0.0.3"
-        - COMPILER="ccache g++"
-
     # OS X using g++
     - stage: Test different OS/CXX/Flags
       os: osx
@@ -151,29 +137,50 @@ jobs:
         - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
+    - stage: Test different OS/CXX/Flags
+      os: linux
+      cache: ccache
+      env:
+        - BUILD_SYSTEM=cmake
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+          packages:
+            - g++-5
+      install:
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=g++-5'
+        - cmake --build build -- -j4
+      script: (cd build; ctest -V -L CORE)
+
+    - stage: Test different OS/CXX/Flags
+      os: osx
+      cache: ccache
+      env:
+        - BUILD_SYSTEM=cmake
+        - CCACHE_CPP2=yes
+      install:
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
+        - cmake --build build -- -j4
+      script: (cd build; ctest -V -L CORE)
+
+
   allow_failures:
     - <<: *linter-stage
 
 install:
   - ccache --max-size=1G
-  - COMMAND="make -C src minisat2-download" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C src boost-download" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C src/ansi-c library_check" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g -DUSE_BOOST $EXTRA_CXXFLAGS\" -j2" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2 clobber.dir memory-models.dir musketeer.dir" &&
-    eval ${PRE_COMMAND} ${COMMAND}
+  - make -C src minisat2-download
+  - make -C src boost-download
+  - make -C src/ansi-c library_check
+  - make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g -DUSE_BOOST ${EXTRA_CXXFLAGS}" -j2
+  - make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2 clobber.dir memory-models.dir
 
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-    COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\"" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C unit CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C unit test" && eval ${PRE_COMMAND} ${COMMAND}
+  - env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}"
+  - make -C unit "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2
+  - make -C unit test
 
 before_cache:
   - ccache -s

CMakeLists.txt

@@ -0,0 +1,41 @@
+cmake_minimum_required(VERSION 3.2)
+
+find_program(CCACHE_PROGRAM ccache)
+if(CCACHE_PROGRAM)
+    set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE "${CCACHE_PROGRAM}")
+    message(STATUS "Rule launch compile: ${CCACHE_PROGRAM}")
+ endif()
+
+set(CMAKE_OSX_DEPLOYMENT_TARGET 10.9)
+
+include(GNUInstallDirs)
+
+set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
+
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
+   "${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU"
+)
+    #   Ensure NDEBUG is not set for release builds
+    set(CMAKE_CXX_FLAGS_RELEASE "-O2")
+    #   Enable lots of warnings
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror")
+elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+    #   This would be the place to enable warnings for Windows builds, although
+    #   config.inc doesn't seem to do that currently
+endif()
+
+set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")
+
+set(sat_impl "minisat2" CACHE STRING
+    "This setting controls the SAT library which is used. Valid values are 'minisat2' and 'glucose'"
+)
+
+add_subdirectory(src)
+
+if(${enable_cbmc_tests})
+    enable_testing()
+endif()
+add_subdirectory(unit)
+add_subdirectory(regression)

COMPILING

@@ -171,7 +171,7 @@ Follow these instructions:
    BUILD_ENV = MSVC
 
    Open the Visual Studio Command prompt, and then bash.exe -login from
-   Cygwin from in there. 
+   Cygwin from in there.
 
 3) Type cd src; make - that should do it.
 
@@ -183,6 +183,53 @@ can be used for building with MSBuild.  Note that you still need to run
 flex/bison using "make generated_files" before opening the project.
 
 
+WORKING WITH CMAKE (EXPERIMENTAL)
+---------------------------------
+
+There is an experimental build based on CMake instead of hand-written
+makefiles. It should work on a wider variety of systems than the standard
+makefile build, and can integrate better with IDEs and static-analysis tools.
+
+0) Run `cmake --version`. If you get a command-not-found error, or the installed
+   version is lower than 3.2, go and install a new version. Most Linux
+   distributions have a package for CMake, and Mac users can get it through
+   Homebrew.  Windows users should download it manually from cmake.org.
+
+1) Create a directory to store your build:
+   `mkdir build`
+   Run this from the *top level* folder of the project. This is different from
+   the other builds, which require you to `cd src` first.
+
+2) Generate build files with CMake:
+   `cmake -H. -Bbuild`
+   This command tells CMake to use the configuration in the current directory,
+   and to generate build files into the `build` directory.
+   This is the point to specify custom build settings, such as compilers and
+   build back-ends. You can use clang (for example) by adding the argument
+   `-DCMAKE_CXX_COMPILER=clang++` to the command line. You can also tell
+   CMake to generate IDE projects by supplying the `-G` flag.
+   Run `cmake -G` for a comprehensive list of supported back-ends.
+
+   Generally it is not necessary to manually specify individual compiler or
+   linker flags, as CMake defines a number of "build modes" including Debug
+   and Release modes. To build in a particular mode, add the flag
+   `-DCMAKE_BUILD_TYPE=Debug` (or `Release`) to the initial invocation.
+
+   If you *do* need to manually add flags, use `-DCMAKE_CXX_FLAGS=...` and
+   `-DCMAKE_EXE_LINKER_FLAGS=...`. This is useful for enabling clang's
+   sanitizers.
+
+   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.
+
+3) Run the build:
+   `cmake --build build`
+   This command tells CMake to invoke the correct tool to run the build in the
+   `build` directory. You can also use the build back-end directly by invoking
+   `make`, `ninja`, or opening the generated IDE project as appropriate.
+
+
 WORKING WITH ECLIPSE
 --------------------
 

appveyor.yml

@@ -60,19 +60,21 @@ build_script:
 test_script:
 - cmd: |
     cd regression
-    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" ansi-c/Makefile
-    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" cpp/Makefile
-    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-instrument/chain.sh
-    sed -i "15s/.*/$goto_cc $name.c/" goto-instrument/chain.sh
-    sed -i "16i mv $name.exe $name.gb" goto-instrument/chain.sh
-    sed -i "23s/.*/  $goto_cc ${name}-mod.c/" goto-instrument/chain.sh
-    sed -i "24i   mv ${name}-mod.exe $name-mod.gb" goto-instrument/chain.sh
-    cat goto-instrument/chain.sh
 
-    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-instrument-typedef/chain.sh || true
-    sed -i "12s/.*/$GC $NAME.c --function fun/" goto-instrument-typedef/chain.sh || true
-    sed -i "13i mv $NAME.exe $NAME.gb" goto-instrument-typedef/chain.sh || true
-    cat goto-instrument-typedef/chain.sh || true
+    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-cbmc/chain.sh || true
+    sed -i "11s/.*/$GC $NAME.c/" goto-cc-cbmc/chain.sh || true
+    sed -i "12i mv $NAME.exe $NAME.gb" goto-cc-cbmc/chain.sh || true
+    cat goto-cc-cbmc/chain.sh || true
+
+    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-goto-analyzer/chain.sh || true
+    sed -i "11s/.*/$gc $name.c/" goto-cc-goto-analyzer/chain.sh || true
+    sed -i "12i mv $name.exe $name.gb" goto-cc-goto-analyzer/chain.sh || true
+    cat goto-cc-goto-analyzer/chain.sh || true
+
+    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-symex/chain.sh || true
+    sed -i "11s/.*/$gc $name.c/" goto-cc-symex/chain.sh || true
+    sed -i "12i mv $name.exe $name.gb" goto-cc-symex/chain.sh || true
+    cat goto-cc-symex/chain.sh || true
 
     rem HACK disable failing tests
     rmdir /s /q ansi-c\arch_flags_mcpu_bad
@@ -111,6 +113,11 @@ test_script:
     rmdir /s /q cbmc-java\tableswitch2
     rmdir /s /q goto-gcc
     rmdir /s /q goto-instrument\slice08
+    rmdir /s /q symex\va_args_10
+    rmdir /s /q symex\va_args_2
+    rmdir /s /q symex\va_args_3
+    rmdir /s /q symex\va_args_5
+    rmdir /s /q symex\va_args_6
 
     make test
 

regression/CMakeLists.txt

@@ -0,0 +1,36 @@
+set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_STANDARD_REQUIRED true)
+
+set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
+
+macro(add_test_pl_profile name cmdline flag profile)
+    add_test(
+        NAME "${name}-${profile}"
+        COMMAND ${test_pl_path} -c ${cmdline} ${flag}
+        WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
+    )
+    set_tests_properties("${name}-${profile}" PROPERTIES
+        LABELS "${profile}"
+    )
+endmacro(add_test_pl_profile)
+
+macro(add_test_pl_tests name cmdline)
+    add_test_pl_profile("${name}" "${cmdline}" -C CORE)
+    add_test_pl_profile("${name}" "${cmdline}" -T THOROUGH)
+    add_test_pl_profile("${name}" "${cmdline}" -F FUTURE)
+    add_test_pl_profile("${name}" "${cmdline}" -K KNOWNBUG)
+endmacro(add_test_pl_tests)
+
+add_subdirectory(ansi-c)
+add_subdirectory(cbmc)
+add_subdirectory(cbmc-java)
+add_subdirectory(cbmc-java-inheritance)
+add_subdirectory(cpp)
+add_subdirectory(goto-analyzer)
+add_subdirectory(goto-diff)
+add_subdirectory(goto-instrument)
+add_subdirectory(goto-instrument-typedef)
+add_subdirectory(invariants)
+add_subdirectory(strings)
+add_subdirectory(strings-smoke-tests)
+add_subdirectory(test-script)

regression/Makefile

@@ -5,13 +5,17 @@ DIRS = ansi-c \
        cbmc-java-inheritance \
        cpp \
        goto-analyzer \
+       goto-cc-cbmc \
+       goto-cc-goto-analyzer \
+       goto-cc-goto-symex \
        goto-diff \
        goto-gcc \
        goto-instrument \
        goto-instrument-typedef \
        invariants \
        strings \
        strings-smoke-tests \
+       symex \
        test-script \
        # Empty last line
 

regression/ansi-c/CMakeLists.txt

@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "ansi-c"
+    "$<TARGET_FILE:goto-cc>"
+)

regression/ansi-c/Initializer_cast2/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  int A[(sizeof((int[]){1, 2, 3})==3*sizeof(int))?1:-1];
+
+  return 0;
+}

regression/ansi-c/Initializer_cast2/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^CONVERSION ERROR$

regression/ansi-c/Makefile

@@ -1,13 +1,22 @@
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+else
+	exe=../../../src/goto-cc/goto-cc
+endif
+
 test:
-	@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
+	@if ! ../test.pl -c $(exe) ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi
 
 tests.log: ../test.pl
-	@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
+	@if ! ../test.pl -c $(exe) ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi

regression/ansi-c/arch_flags_mcpu_good/test.desc

@@ -14,6 +14,10 @@ command line:
 
   goto-cc --native-compiler=arm-none-eabi-gcc -mcpu=cortex-a15 -c source.c
 
+On Ubuntu, you can get a suitable compiler using:
+
+  sudo apt install gcc-arm-none-eabi
+
 preproc.i is already pre-processed so that it can be linked in without
 needing to invoke a pre-processor from a cross-compile toolchain on your
 local machine. Linking it together with the ARM object file, while

regression/ansi-c/arch_flags_mthumb_good/test.desc

@@ -14,6 +14,10 @@ line:
 
   goto-cc --native-compiler=arm-none-eabi-gcc -mthumb -c source.c
 
+On Ubuntu, you can get a suitable compiler using:
+
+  sudo apt install gcc-arm-none-eabi
+
 preproc.i is already pre-processed so that it can be linked in without
 needing to invoke a pre-processor from a cross-compile toolchain on your
 local machine. Linking it together with the ARM object file, while

regression/ansi-c/array_initialization3/main.c

@@ -0,0 +1,13 @@
+#define STATIC_ASSERT_sizeof(condition) \
+  int[(condition) ? 1 : -1]
+
+int A[];
+int B[];
+
+int A[1]={sizeof(A)};
+int B[1]={sizeof(STATIC_ASSERT_sizeof(sizeof(B)==sizeof(int)))};
+
+int main()
+{
+  return 0;
+}

regression/ansi-c/array_initialization3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/ansi-c/sizeof5/main.c

@@ -0,0 +1,15 @@
+#define STATIC_ASSERT(condition) \
+  int some_array##__LINE__[(condition) ? 1 : -1];
+
+struct S
+{
+  int x;
+};
+
+int main()
+{
+  struct S s;
+  __typeof__(*((void *)&s.x)) *_s=&s.x;
+  STATIC_ASSERT(sizeof(*_s)==1);
+  return 0;
+}