Merge remote-tracking branch 'upstream/develop' into security-scanner-support

Author: smowton

.travis.yml

@@ -39,32 +39,6 @@ jobs:
       # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
       env: COMPILER="ccache g++-5"
 
-    # OS X using g++
-    - stage: Test different OS/CXX/Flags
-      os: osx
-      sudo: false
-      compiler: gcc
-      cache: ccache
-      before_install:
-          #we create symlink to non-ccache gcc, to be used in tests
-        - mkdir bin ; ln -s /usr/bin/gcc bin/gcc
-        - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
-        - export PATH=/usr/local/opt/ccache/libexec:$PATH
-      env: COMPILER="ccache g++"
-
-    # OS X using clang++
-    - stage: Test different OS/CXX/Flags
-      os: osx
-      sudo: false
-      compiler: clang
-      cache: ccache
-      before_install:
-        - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
-        - export PATH=/usr/local/opt/ccache/libexec:$PATH
-      env:
-        - COMPILER="ccache clang++ -Qunused-arguments -fcolor-diagnostics"
-        - CCACHE_CPP2=yes
-
     # Ubuntu Linux with glibc using g++-5, debug mode
     - stage: Test different OS/CXX/Flags
       os: linux
@@ -153,17 +127,42 @@ jobs:
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE)
 
+    # Run Coverity
     - stage: Test different OS/CXX/Flags
-      os: osx
+      os: linux
+      sudo: required
+      compiler: gcc
       cache: ccache
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+          packages:
+            - libwww-perl
+            - g++-5
+        coverity_scan:
+          project:
+            name: "diffblue/cbmc"
+            description: "Travis build of ${TRAVIS_COMMIT}"
+          notification_email: "[email protected]"
+          build_command_prepend: "make -C src minisat2-download"
+          build_command: "make -C src -j2"
+          branch_pattern: "develop"
+      before_install:
+        - |
+          if [[ "${TRAVIS_EVENT_TYPE}" != "cron" ]]
+          then
+            echo "This is not a cron build and build is not needed."
+            travis_terminate 0
+          fi
+        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
+        - sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 90
+        - g++ --version
+      # Coverity runs as part of before_script
       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)
-
+        - NAME="COVERITY_SCAN"
+        - COMPILER="ccache g++"
+      script: echo "This is coverity build. No need for tests."
 
   allow_failures:
     - <<: *linter-stage

CMakeLists.txt

@@ -6,6 +6,8 @@ if(CCACHE_PROGRAM)
     message(STATUS "Rule launch compile: ${CCACHE_PROGRAM}")
  endif()
 
+set(CMAKE_EXPORT_COMPILE_COMMANDS true)
+
 set(CMAKE_OSX_DEPLOYMENT_TARGET 10.9)
 
 include(GNUInstallDirs)

README.md

@@ -1,4 +1,5 @@
 [![Build Status][travis_img]][travis] [![Build Status][appveyor_img]][appveyor]
+[![Build Status][coverity_img]][coverity]
 
 [CProver Wiki](http://www.cprover.org/wiki)
 
@@ -47,4 +48,6 @@ License
 [travis]: https://travis-ci.org/diffblue/cbmc
 [travis_img]: https://travis-ci.org/diffblue/cbmc.svg?branch=master
 [appveyor]: https://ci.appveyor.com/project/diffblue/cbmc/
-[appveyor_img]: https://ci.appveyor.com/api/projects/status/github/diffblue/cbmc?svg=true&branch=master
+[appveyor_img]: https://ci.appveyor.com/api/projects/status/github/diffblue/cbmc?svg=true&branch=master
+[coverity]: https://scan.coverity.com/projects/diffblue-cbmc
+[coverity_img]: https://scan.coverity.com/projects/13552/badge.svg

appveyor.yml

@@ -61,21 +61,6 @@ test_script:
 - cmd: |
     cd regression
 
-    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
     rmdir /s /q ansi-c\arch_flags_mcpu_good
@@ -113,11 +98,6 @@ 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

@@ -14,11 +14,13 @@ macro(add_test_pl_profile name cmdline flag 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)
+macro(add_test_pl_tests cmdline)
+    get_filename_component(TEST_DIR_NAME ${CMAKE_CURRENT_SOURCE_DIR} NAME)
+    message(STATUS "Adding tests in directory: ${TEST_DIR_NAME}")
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -C CORE)
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -T THOROUGH)
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -F FUTURE)
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG)
 endmacro(add_test_pl_tests)
 
 add_subdirectory(ansi-c)
@@ -27,6 +29,8 @@ add_subdirectory(cbmc-java)
 add_subdirectory(cbmc-java-inheritance)
 add_subdirectory(cpp)
 add_subdirectory(goto-analyzer)
+add_subdirectory(goto-cc-cbmc)
+add_subdirectory(goto-cc-goto-analyzer)
 add_subdirectory(goto-diff)
 add_subdirectory(goto-instrument)
 add_subdirectory(goto-instrument-typedef)

regression/Makefile

@@ -7,15 +7,13 @@ DIRS = ansi-c \
        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

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

regression/cbmc-cover/branch3/test.desc

@@ -3,6 +3,7 @@ main.c
 --cover branch --unwind 6
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* .* of .* covered \(100.0%\)$
+^\*\* .* of .* covered \(.*\)$
 --
 ^warning: ignoring
+^\[main.coverage.*\] file main.c line .* function main block .* branch .*: FAILED$

regression/cbmc-cover/built-ins1/main.c

@@ -1,9 +1,11 @@
+#include <string.h>
+
 int main()
 {
   char a[10];
   __CPROVER_input("a[3]", a[3]);
 
-  int len = strlen(a);
+  int len=strlen(a);
 
   if(len==3)
   {
@@ -13,5 +15,6 @@ int main()
   {
     return -1;
   }
+
   return 1;
 }

regression/cbmc-cover/built-ins1/test.desc

@@ -3,7 +3,7 @@ main.c
 --cover location --unwind 1
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* 4 of 7 covered
+^\*\* 5 of 8 covered
 --
 ^warning: ignoring
 ^\[.*<builtin-library-

regression/cbmc-cover/built-ins3/main.c

@@ -5,6 +5,8 @@ int main()
   const char *s="test";
   int ret=puts(s); //return value is nondet (internal to built-in, thus non-controllable)
 
+  __CPROVER_input("return value puts", ret);
+
   if(ret<0)
   {
     return 1;

regression/cbmc-cover/built-ins3/test.desc

@@ -3,7 +3,7 @@ main.c
 --cover location --unwind 10
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* 4 of 4 covered
+^\*\* 5 of .* covered
 --
 ^warning: ignoring
 ^\[.*<builtin-library-

regression/cbmc-cover/built-ins4/main.c

@@ -1,3 +1,5 @@
+#include <string.h>
+
 int main()
 {
   char a[10];

regression/cbmc-cover/built-ins5/main.c

@@ -1,3 +1,5 @@
+#include <string.h>
+
 int main()
 {
   char a[10];

regression/cbmc-cover/built-ins6/main.c

@@ -1,3 +1,5 @@
+#include <string.h>
+
 int main()
 {
   char a[10];

regression/cbmc-cover/built-ins7/main.c

@@ -1,3 +1,5 @@
+#include <string.h>
+
 int main()
 {
   char a[10];

regression/cbmc-cover/inlining1/main.c

@@ -1,3 +1,5 @@
+// Discussion point: is the branch below one goal or two?
+
 inline void my_func(int x)
 {
   if(x)

regression/cbmc-cover/inlining1/test.desc

@@ -3,9 +3,9 @@ main.c
 --cover branch
 ^EXIT=0$
 ^SIGNAL=0$
-^\[my_func.coverage.1\] file main.c line 3 function my_func block 1 branch false: SATISFIED$
-^\[my_func.coverage.2\] file main.c line 3 function my_func block 1 branch true: FAILED$
-^\[my_func.coverage.3\] file main.c line 3 function my_func block 2 branch false: FAILED$
-^\[my_func.coverage.4\] file main.c line 3 function my_func block 2 branch true: SATISFIED$
+^\[main.coverage.1\] file main.c line 15 function main entry point: SATISFIED$
+^\[my_func.coverage.1\] file main.c line 5 function my_func entry point: SATISFIED$
+^\[my_func.coverage.2\] file main.c line 5 function my_func block 1 branch false: SATISFIED$
+^\[my_func.coverage.3\] file main.c line 5 function my_func block 1 branch true: SATISFIED$
 --
 ^warning: ignoring

regression/cbmc-java-inheritance/CMakeLists.txt

@@ -1,4 +1,3 @@
 add_test_pl_tests(
-    "cbmc-java-inheritance"
     "$<TARGET_FILE:cbmc>"
 )

regression/cbmc-java/CMakeLists.txt

@@ -1,4 +1,3 @@
 add_test_pl_tests(
-    "cbmc-java"
     "$<TARGET_FILE:cbmc>"
 )

regression/cbmc/CMakeLists.txt

@@ -1,4 +1,3 @@
 add_test_pl_tests(
-    "cbmc"
     "$<TARGET_FILE:cbmc>"
 )

regression/cbmc/Free2/test.desc

@@ -1,8 +1,10 @@
 CORE
 main.c
---pointer-check
+
 ^EXIT=10$
 ^SIGNAL=0$
+^.*free argument must be dynamic object: FAILURE$
+^.*free argument has offset zero: SUCCESS$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/String6/main.c

@@ -1,15 +1,19 @@
 #include <assert.h>
 #include <string.h>
-void free(void *);
+#include <stdlib.h>
 
 int main()
 {
   char str[500]="Hello";
 
   assert(strcmp(str, "Hello")==0);
   assert(strncmp(str, "Hello", 5)==0);
+
+  #ifndef _MSC_VER
   assert(strcasecmp(str, "HELLO")==0);
   assert(strncasecmp(str, "HELLO", 5)==0);
+  #endif
+
   assert(strcmp(str, "\xff")<0);
   assert(strncmp("ASDxx", "ASDyy", 3)==0);
 

regression/cbmc/va_list3/main.c

@@ -0,0 +1,29 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+void foo(int n, ...);
+
+int main()
+{
+  foo(1, 1u);
+  foo(2, 2l);
+  foo(3, 3.0);
+  return 0;
+}
+
+void foo(int n, ...)
+{
+  va_list vl;
+
+  va_start(vl,n);
+  
+  switch(n)
+  {
+  case 1: assert(va_arg(vl, unsigned)==1); break;
+  case 2: assert(va_arg(vl, long)==2); break;
+  case 3: assert(va_arg(vl, double)==3.0); break;
+  }
+  
+  va_end(vl);
+}

regression/symex-infeasibility/bst-safe/test.desc renamed to regression/cbmc/va_list3/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$

regression/cpp/CMakeLists.txt

@@ -1,4 +1,3 @@
 add_test_pl_tests(
-    "cpp"
     "$<TARGET_FILE:goto-cc>"
 )

regression/goto-analyzer/CMakeLists.txt

@@ -1,4 +1,3 @@
 add_test_pl_tests(
-    "goto-analyzer"
     "$<TARGET_FILE:goto-analyzer>"
 )

regression/goto-cc-cbmc/CMakeLists.txt

@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> ${is_windows}"
+)