Merge commit '6f386e5eeffa223e7213b596403085f8b497023e' into pull-support-20170908-2

Author: smowton

src/.dir-locals.el renamed to .dir-locals.el

@@ -1,23 +1,61 @@
 language: cpp
 
-matrix:
+jobs:
   include:
 
+    - &linter-stage
+      stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
+      env: NAME="CPP-LINT"
+      install:
+      script: scripts/travis_lint.sh
+      before_cache:
+
+    - stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
+      env: NAME="DOXYGEN-CHECK"
+      addons:
+        apt:
+          packages:
+            - doxygen
+      install:
+      script: scripts/travis_doxygen.sh
+      before_cache:
+
+    # Ubuntu Linux with glibc using g++-5
+    - stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
+      os: linux
+      sudo: false
+      compiler: gcc
+      cache: ccache
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+          packages:
+            - libwww-perl
+            - g++-5
+            - libubsan0
+      before_install:
+        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
+      # 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++
-    - os: linux
+    - 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.1
+        - 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.1"
+        - 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++
-    - os: osx
+    - stage: Test different OS/CXX/Flags
+      os: osx
       sudo: false
       compiler: gcc
       cache: ccache
@@ -26,42 +64,24 @@ matrix:
         - 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
-        - ccache -M 1G
-      env: COMPILER=g++
+      env: COMPILER="ccache g++"
 
     # OS X using clang++
-    - os: osx
+    - 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
-        - ccache -M 1G
       env:
         - COMPILER="ccache clang++ -Qunused-arguments -fcolor-diagnostics"
         - CCACHE_CPP2=yes
 
-    # Ubuntu Linux with glibc using g++-5
-    - os: linux
-      sudo: false
-      compiler: gcc
-      cache: ccache
-      addons:
-        apt:
-          sources:
-            - ubuntu-toolchain-r-test
-          packages:
-            - libwww-perl
-            - g++-5
-            - libubsan0
-      before_install:
-        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
-      # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
-      env: COMPILER="g++-5"
-
     # Ubuntu Linux with glibc using g++-5, debug mode
-    - os: linux
+    - stage: Test different OS/CXX/Flags
+      os: linux
       sudo: false
       compiler: gcc
       cache: ccache
@@ -77,12 +97,13 @@ matrix:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
       # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
       env:
-        - COMPILER="g++-5"
+        - COMPILER="ccache g++-5"
         - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
     # Ubuntu Linux with glibc using clang++-3.7
-    - os: linux
+    - stage: Test different OS/CXX/Flags
+      os: linux
       sudo: false
       compiler: clang
       cache: ccache
@@ -105,7 +126,8 @@ matrix:
         - CCACHE_CPP2=yes
 
     # Ubuntu Linux with glibc using clang++-3.7, debug mode
-    - os: linux
+    - stage: Test different OS/CXX/Flags
+      os: linux
       sudo: false
       compiler: clang
       cache: ccache
@@ -129,31 +151,17 @@ matrix:
         - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
-    - env: NAME="CPP-LINT"
-      install:
-      script: scripts/travis_lint.sh
-      before_cache:
-
-    - env: NAME="DOXYGEN-CHECK"
-      addons:
-        apt:
-          packages:
-            - doxygen
-      install:
-      script: scripts/travis_doxygen.sh
-      before_cache:
-
   allow_failures:
-    - env: NAME="CPP-LINT"
-      install:
-      script: scripts/travis_lint.sh
-      before_cache:
+    - <<: *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" &&

.travis.yml

@@ -10,6 +10,7 @@
 * GOTO-INSTRUMENT: New option --remove-function-body
 * GOTO-INSTRUMENT: New option --use-all-headers, changed --use-system-headers to
   --no-system-headers
+* GOTO-INSTRUMENT: dump-c can output the generated environment via --harness
 
 
 5.7

CHANGELOG

@@ -15,6 +15,31 @@ and passing the resulting equation to a decision procedure.
 
 For full information see [cprover.org](http://www.cprover.org/cbmc).
 
+Versions
+========
+
+Get the [latest release](https://github.com/diffblue/cbmc/releases)
+* Releases are tested and for production use.
+
+Get the current *develop* version: `git clone https://github.com/diffblue/cbmc.git`
+* Develop versions are not recommended for production use.
+
+Report bugs
+===========
+
+If you encounter a problem please file a bug report:
+* Create an [issue](https://github.com/diffblue/cbmc/issues)
+
+Contributing to the code base
+=============================
+
+1. Fork the repository
+2. Clone the repository `git clone [email protected]:YOURNAME/cbmc.git`
+3. Create a branch from the `develop` branch (default branch)
+4. Make your changes (follow the [coding guidelines](https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md))
+5. Push your changes to your branch
+6. Create a Pull Request targeting the `develop` branch
+
 License
 =======
 4-clause BSD license, see `LICENSE` file.

README.md

@@ -109,6 +109,7 @@ test_script:
     rmdir /s /q cbmc-java\classpath1
     rmdir /s /q cbmc-java\jar-file3
     rmdir /s /q cbmc-java\tableswitch2
+    rmdir /s /q goto-gcc
     rmdir /s /q goto-instrument\slice08
 
     make test

appveyor.yml

@@ -0,0 +1 @@
+tests.log

regression/.gitignore

@@ -1,18 +1,28 @@
 DIRS = ansi-c \
        cbmc \
-       cpp \
+       cbmc-cover \
        cbmc-java \
+       cbmc-java-inheritance \
+       cpp \
        goto-analyzer \
+       goto-diff \
+       goto-gcc \
        goto-instrument \
        goto-instrument-typedef \
-       goto-diff \
        invariants \
+       strings \
+       strings-smoke-tests \
        test-script \
        # Empty last line
 
-
+# Check for the existence of $dir. Tests under goto-gcc cannot be run on
+# Windows, so appveyor.yml unlinks the entire directory under Windows.
 test:
-	$(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;)
+	@for dir in $(DIRS); do \
+	  if [ -d "$$dir" ]; then \
+	    $(MAKE) -C "$$dir" test || exit 1; \
+	  fi; \
+	done;
 
 clean:
 	@for dir in *; do \

regression/Makefile

@@ -62,6 +62,33 @@ STATIC_ASSERT(sizeof(union some_union4)==3);
 
 #endif
 
+#ifdef _MSC_VER
+
+union some_union5
+{
+  int i;
+};
+
+STATIC_ASSERT(__alignof(union some_union5)==1);
+
+#else
+
+union some_union5
+{
+  int i;
+};
+
+union some_union6
+{
+  int i;
+} __attribute__((__packed__));
+
+// Packing may affect alignment
+STATIC_ASSERT(_Alignof(union some_union5)==4);
+STATIC_ASSERT(_Alignof(union some_union6)==1);
+
+#endif
+
 int main()
 {
 }

regression/ansi-c/Union_Padding1/main.c

@@ -0,0 +1,34 @@
+static unsigned bar()
+{
+  unsigned r;
+  return r;
+}
+
+#ifdef _MSC_VER
+
+static void foo()
+{
+}
+
+#else
+
+static void foo()
+{
+ unsigned len=bar();
+ struct {
+   int a;
+   union {
+     int s;
+     unsigned char b[len];
+   } __attribute__ (( packed )) S;
+   int c;
+ } __attribute__ (( packed )) *l;
+}
+
+#endif
+
+int main()
+{
+  foo();
+  return 0;
+}

regression/ansi-c/Union_Padding2/main.c

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

regression/ansi-c/Union_Padding2/test.desc

@@ -0,0 +1,12 @@
+extern char src_start[];
+extern char src_end[];
+extern char dst_start[];
+
+void *memcpy(void *dest, void *src, unsigned n){
+  return (void *)0;
+}
+
+int main(){
+  memcpy(dst_start, src_start, (unsigned)src_end - (unsigned)src_start);
+  return 0;
+}

regression/ansi-c/linker_script_start+end/main.c

@@ -0,0 +1,22 @@
+MEMORY {
+  RAM : ORIGIN = 0x0, LENGTH = 25M
+}
+
+SECTIONS
+{
+  /* GCC insists on having these */
+  .note.gnu.build-id : { } > RAM
+  .text : { } > RAM
+
+  .src_section : {
+    src_start = .;
+    *(.text*)
+    src_end = .;
+  } > RAM
+
+  .dst_section : {
+    dst_start = .;
+    *(.text*)
+    dst_end = .;
+  } > RAM
+}

regression/ansi-c/linker_script_start+end/script.ld

@@ -0,0 +1,17 @@
+CORE
+main.c
+-o out.gb -T script.ld -nostdlib
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+Tesing the functionality of goto-cc's linker script parsing
+functionality, ensuring that it can get the values of symbols that are
+defined in linker scripts.
+
+This test ensures that goto-cc and ls-parse can:
+
+- get the value of a symbol whose value indicates the start of a section;
+- get the value of a symbol whose value indicates the end of a section.