fix compilation instructions

kroening · kroening · commit 001f6845d297 · 2018-06-23T19:38:04.000+01:00
diff --git 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
@@ -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,20 +171,19 @@ 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`
       for BUILD_ENV = Cygwin.
       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.
