diff --git a/CODING_STANDARD.md b/CODING_STANDARD.md index 002f5ad0dfc..1b234d30628 100644 --- a/CODING_STANDARD.md +++ b/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 clang-format@3.8 # 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. diff --git a/COMPILING.md b/COMPILING.md index 04a1f8967f2..38b5f9ec299 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -19,47 +19,36 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution. 1. You need a C/C++ compiler, Flex and Bison, and GNU make. The GNU Make needs to be version 3.81 or higher. - On Debian-like distributions, do + On Debian-like distributions, do as root: ``` - apt-get install g++ gcc flex bison make git libwww-perl patch openjdk-7-jdk + apt-get install g++ gcc flex bison make git libwww-perl patch ``` - On Red Hat/Fedora or derivates, do + On Red Hat/Fedora or derivates, do as root: ``` - yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6 java-1.7.0-openjdk-devel + dnf install gcc gcc-c++ flex bison perl-libwww-perl patch ``` Note that you need g++ version 5.0 or newer. To compile JBMC, you additionally need the JDK and the java-models-library. - - For the JDK, on Debian-like distributions, do - ``` - apt-get install openjdk-7-jdk + For the JDK, on Debian-like distributions, do as root: ``` - On Red Hat/Fedora or derivates, do + apt-get install openjdk-8-jdk ``` - yum install java-1.7.0-openjdk-devel + On Red Hat/Fedora or derivates, do as root: ``` - For the models library, do - ``` - make -C jbmc/src java-models-library-download + dnf install java-1.8.0-openjdk-devel ``` 2. As a user, get the CBMC source via ``` git clone https://github.com/diffblue/cbmc cbmc-git + cd cbmc-git ``` -3. On Debian or Ubuntu, do - ``` - cd cbmc-git/src - make minisat2-download - make - ``` - On Redhat/Fedora etc., do + +3. To compile, do ``` - cd cbmc-git/src - make minisat2-download - scl enable devtoolset-6 bash - make + make -C src minisat2-download + make -C src ``` 4. Linking against an IPASIR SAT solver @@ -75,10 +64,17 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution. make -C src IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a ``` +5. To compile JBMC, do + ``` + make -C jbmc/src java-models-library-download + make -C jbmc/src + ``` + # COMPILATION ON SOLARIS 11 1. As root, get the necessary development tools: ``` + pkg install system/header pkgadd -d http://get.opencsw.org/now /opt/csw/bin/pkgutil -U /opt/csw/bin/pkgutil -i gcc5g++ bison flex git @@ -87,43 +83,43 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution. ``` export PATH=/opt/csw/bin:$PATH git clone https://github.com/diffblue/cbmc cbmc-git + cd cbmc-git ``` -3. Get MiniSat2 by entering - ``` - cd cbmc-git/src - gmake minisat2-download DOWNLOADER=wget TAR=gtar - ``` -4. To compile, type +3. To compile CBMC, type ``` - gmake + gmake -C src minisat2-download DOWNLOADER=wget TAR=gtar + gmake -C src ``` - That should do it. To run, you will need +4. To compile JBMC, type ``` - export LD_LIBRARY_PATH=/usr/gcc/5.0/lib + gmake -C jbmc/src java-models-library-download + gmake -C jbmc/src ``` # COMPILATION ON FREEBSD 11 1. As root, get the necessary tools: ``` - pkg install bash gmake git www/p5-libwww patch flex bison openjdk + pkg install bash gmake git www/p5-libwww patch flex bison ``` To compile JBMC, additionally install ``` - pkg install openjdk + pkg install openjdk8 wget ``` - 2. As a user, get the CBMC source via +2. As a user, get the CBMC source via ``` git clone https://github.com/diffblue/cbmc cbmc-git + cd cbmc-git ``` -3. Do +3. To compile CBMC, do ``` - cd cbmc-git/src + gmake -C src minisat2-download + gmake -C src ``` -4. Do +4. To compile JBMC, do ``` - gmake minisat2-download - gmake + gmake -C jbmc/src java-models-library-download + gmake -C jbmc/src ``` # COMPILATION ON MACOS X @@ -139,12 +135,17 @@ Follow these instructions: 2. Then get the CBMC source via ``` git clone https://github.com/diffblue/cbmc cbmc-git + cd cbmc-git + ``` +3. To compile CBMC, do ``` -3. Then type + make -C src minisat2-download + make -C src ``` - cd cbmc-git/src - make minisat2-download - make +4. To compile JBMC, do + ``` + make -C jbmc/src java-models-library-download + make -C jbmc/src ``` # COMPILATION ON WINDOWS @@ -161,6 +162,7 @@ Follow these instructions: 2. Get the CBMC source via ``` git clone https://github.com/diffblue/cbmc cbmc-git + cd cbmc-git ``` 3. Depending on your choice of compiler: 1. To compile with Visual Studio, change the second line of `src/config.inc` @@ -169,10 +171,10 @@ Follow these instructions: BUILD_ENV = MSVC ``` Open the Developer Command Prompt for Visual Studio, then start the - Cygwin shell with - ``` - bash.exe -login - ``` + Cygwin shell with + ``` + bash.exe -login + ``` 2. To compile with MinGW, use Cygwin setup to install a mingw g++ compiler package, i.e. one of `mingw{32,64}-{x86_64,i686}-gcc-g++`. You may also have to adjust the section in `src/common` that defines `CC` and `CXX` @@ -180,9 +182,8 @@ Follow these instructions: Then start the Cygwin shell. 4. In the Cygwin shell, type ``` - cd cbmc-git/src - make DOWNLOADER=wget minisat2-download - make + make -C src DOWNLOADER=wget minisat2-download + make -C src ``` (Optional) A Visual Studio project file can be generated with the script @@ -277,96 +278,3 @@ To work with Eclipse, do the following: 5. Click "Finish" 6. Select Project -> Build All -# 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 clang-format@3.8 # 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.