Merge pull request diffblue#473 from diffblue/CBMC_merge_2018-06-26

SEC-518: Cbmc merge 2018-06-26

Author: owen-jones-diffblue

cbmc/.gitignore

@@ -28,6 +28,7 @@ Release/*
 *.obj
 *.a
 *.lib
+version.h
 src/ansi-c/arm_builtin_headers.inc
 src/ansi-c/clang_builtin_headers.inc
 src/ansi-c/cprover_builtin_headers.inc

cbmc/CMakeLists.txt

@@ -20,6 +20,7 @@ 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 "AppleClang" OR
    "${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU"
 )
     #   Ensure NDEBUG is not set for release builds
@@ -41,6 +42,48 @@ if(${enable_cbmc_tests})
     enable_testing()
 endif()
 
+# based on https://cmake.org/pipermail/cmake/2010-July/038015.html
+find_package(Git)
+if(GIT_FOUND)
+  file(WRITE ${CMAKE_BINARY_DIR}/version.cmake
+    "
+    file(STRINGS \${CBMC_SOURCE_DIR}/config.inc
+      config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\")
+    string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v})
+    execute_process(
+      COMMAND \"${GIT_EXECUTABLE}\" \"describe\" \"--tags\" \"--always\" \"--dirty\"
+      OUTPUT_VARIABLE GIT_INFO
+      OUTPUT_STRIP_TRAILING_WHITESPACE
+    )
+    configure_file(\${CUR}/version.h.in version.h)
+    "
+  )
+else()
+  file(WRITE ${CMAKE_BINARY_DIR}/version.cmake
+    "
+    file(STRINGS \${CBMC_SOURCE_DIR}/config.inc
+      config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\")
+    string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v})
+    set(GIT_INFO \"n/a\")
+    configure_file(\${CUR}/version.h.in version.h)
+    "
+  )
+endif()
+
+macro(git_revision target)
+  file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/version.h.in
+    "\#define CBMC_VERSION \"@CBMC_RELEASE@ (@GIT_INFO@)\"\n")
+  add_custom_target(
+    ${target}-version.h
+    COMMAND ${CMAKE_COMMAND}
+      -D CBMC_SOURCE_DIR=${CBMC_SOURCE_DIR}
+      -D CUR=${CMAKE_CURRENT_BINARY_DIR}
+      -P ${CMAKE_BINARY_DIR}/version.cmake
+  )
+ add_dependencies(${target} ${target}-version.h)
+endmacro()
+include_directories(${CMAKE_CURRENT_BINARY_DIR})
+
 add_subdirectory(src)
 add_subdirectory(regression)
 add_subdirectory(unit)

cbmc/CODING_STANDARD.md

@@ -240,3 +240,97 @@ or use a symbolic link. Then, when running git commit, you should get the
 linter output (if any) before being prompted to enter a commit message. To
 bypass the check (e.g. if there was a false positive), add the option
 `--no-verify`.
+
+# CODE COVERAGE
+
+Code coverage metrics are provided using gcov and lcov. Ensure that you have
+installed lcov from http://ltp.sourceforge.net/coverage/lcov.php note for
+ubuntu lcov is available in the standard apt-get repos.
+
+To get coverage metrics run the following script from the regression directory:
+```
+get_coverage.sh
+```
+This will:
+ 1) Rebuild CBMC with gcov enabled
+ 2) Run all the regression tests
+ 3) Collate the coverage metrics
+ 4) Provide an HTML report of the current coverage
+
+# USING CLANG-FORMAT
+
+CBMC uses clang-format to ensure that the formatting of new patches is readable
+and consistent. There are two main ways of running clang-format: remotely, and
+locally.
+
+## RUNNING CLANG-FORMAT REMOTELY
+
+When patches are submitted to CBMC, they are automatically run through
+continuous integration (CI). One of the CI checks will run clang-format over
+the diff that your pull request introduces. If clang-format finds formatting
+issues at this point, the build will be failed, and a patch will be produced
+in the CI output that you can apply to your code so that it conforms to the
+style guidelines.
+
+To apply the patch, copy and paste it into a local file (`patch.txt`) and then
+run:
+```
+patch -p1 -i patch.txt
+```
+Now, you can commit and push the formatting fixes.
+
+## RUNNING CLANG-FORMAT LOCALLY
+
+### INSTALLATION
+
+To avoid waiting until you've made a PR to find formatting issues, you can
+install clang-format locally and run it against your code as you are working.
+
+Different versions of clang-format have slightly different behaviors. CBMC uses
+clang-format-3.8 as it is available the repositories for Ubuntu 16.04 and
+Homebrew.
+To install on a Unix-like system, try installing using the system package
+manager:
+```
+apt-get install clang-format-3.8  # Run this on Ubuntu, Debian etc.
+brew install [email protected]     # Run this on a Mac with Homebrew installed
+```
+
+If your platform doesn't have a package for clang-format, you can download a
+pre-built binary, or compile clang-format yourself using the appropriate files
+from the [LLVM Downloads page](http://releases.llvm.org/download.html).
+
+An installer for Windows (along with a Visual Studio plugin) can be found at
+the [LLVM Snapshot Builds page](http://llvm.org/builds/).
+
+### FORMATTING A RANGE OF COMMITS
+
+Clang-format is distributed with a driver script called git-clang-format-3.8.
+This script can be used to format git diffs (rather than entire files).
+
+After committing some code, it is recommended to run:
+```
+git-clang-format-3.8 upstream/develop
+```
+*Important:* If your branch is based on a branch other than `upstream/develop`,
+use the name or checksum of that branch instead. It is strongly recommended to
+rebase your work onto the tip of the branch it's based on before running
+`git-clang-format` in this way.
+
+### RETROACTIVELY FORMATTING INDIVIDUAL COMMITS
+
+If your works spans several commits and you'd like to keep the formatting
+correct in each individual commit, you can automatically rewrite the commits
+with correct formatting.
+
+The following command will stop at each commit in the range and run
+clang-format on the diff at that point.  This rewrites git history, so it's
+*unsafe*, and you should back up your branch before running this command:
+```
+git filter-branch --tree-filter 'git-clang-format-3.8 upstream/develop' \
+  -- upstream/develop..HEAD
+```
+*Important*: `upstream/develop` should be changed in *both* places in the
+command above if your work is based on a different branch. It is strongly
+recommended to rebase your work onto the tip of the branch it's based on before
+running `git-clang-format` in this way.