Merge pull request #5208 from karkhaz/kk-correct-cmake-invocation

Fix cmake flag in COMPILING.md and other docs

Author: karkhaz

.travis.yml

@@ -211,7 +211,7 @@ jobs:
       install:
         - ccache -z
         - ccache --max-size=1G
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_CXX_FLAGS=-DNAMED_SUB_IS_FORWARD_LIST' '-DWITH_MEMORY_ANALYZER=On'
+        - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_CXX_FLAGS=-DNAMED_SUB_IS_FORWARD_LIST' '-DWITH_MEMORY_ANALYZER=On'
         - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; bin/unit "[core][irept]")
@@ -240,7 +240,7 @@ jobs:
       install:
         - ccache -z
         - ccache --max-size=1G
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_USE_CUDD=true' -DCMAKE_CXX_FLAGS="-DBDD_GUARDS" '-DWITH_MEMORY_ANALYZER=On'
+        - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_USE_CUDD=true' -DCMAKE_CXX_FLAGS="-DBDD_GUARDS" '-DWITH_MEMORY_ANALYZER=On'
         - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
@@ -277,7 +277,7 @@ jobs:
       install:
         - ccache -z
         - ccache --max-size=1G
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/clang++-7' '-DCMAKE_CXX_FLAGS=-Qunused-arguments' '-DWITH_MEMORY_ANALYZER=On'
+        - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/clang++-7' '-DCMAKE_CXX_FLAGS=-Qunused-arguments' '-DWITH_MEMORY_ANALYZER=On'
         - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
@@ -297,7 +297,7 @@ jobs:
       install:
         - ccache -z
         - ccache --max-size=1G
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
+        - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
         - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)

COMPILING.md

@@ -245,7 +245,7 @@ require manual modification of build files.
    ```
 4. Generate build files with CMake:
    ```
-   cmake -H. -Bbuild
+   cmake -S . -Bbuild
    ```
    This command tells CMake to use the configuration in the current directory,
    and to generate build files into the `build` directory.  This is the point
@@ -314,7 +314,7 @@ If compiling with cmake:
 1. Add the `-DCMAKE_USE_CUDD=true` flag to the `cmake` configuration phase.
    For instance:
    ```
-   cmake -H. -Bbuild -DCMAKE_USE_CUDD=true
+   cmake -S . -Bbuild -DCMAKE_USE_CUDD=true
    ```
 2. Run the build:
    ```
@@ -336,6 +336,6 @@ compilation flag:
     ```
   * If compiling with CMake:
     ```
-    cmake -H. -Bbuild -DCMAKE_CXX_FLAGS="-DBDD_GUARDS"
+    cmake -S . -Bbuild -DCMAKE_CXX_FLAGS="-DBDD_GUARDS"
     ```
     and then `cmake --build build`

buildspec-linux-cmake-gcc-cov.yml

@@ -18,7 +18,7 @@ phases:
     commands:
       - echo Build started on `date`
       - git submodule update --init --recursive
-      - cmake -H. -Bbuild '-Denable_coverage=1' '-Dparallel_tests=2' '-DCMAKE_CXX_COMPILER=/usr/bin/g++'
+      - cmake -S . -Bbuild '-Denable_coverage=1' '-Dparallel_tests=2' '-DCMAKE_CXX_COMPILER=/usr/bin/g++'
       - cmake --build build --target coverage -- -j2
   post_build:
     commands:

buildspec-linux-cmake-gcc.yml

@@ -16,7 +16,7 @@ phases:
   build:
     commands:
       - echo Build started on `date`
-      - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++'
+      - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++'
       - git submodule update --init --recursive
       - cmake --build build -- -j2
   post_build:

buildspec-windows-cmake.yml

@@ -22,7 +22,7 @@ phases:
         $Env:PATH = "C:\tools\cygwin\bin;c:\tools\clcache\clcache-4.1.0;$Env:PATH"
         & .\scripts\vcvars64.ps1
         git submodule update --init --recursive
-        cmake "-H." -Bbuild -G Ninja "-DCMAKE_C_COMPILER=clcache.exe" "-DCMAKE_CXX_COMPILER=clcache.exe" -DCMAKE_BUILD_TYPE=Release
+        cmake -S . -Bbuild -G Ninja "-DCMAKE_C_COMPILER=clcache.exe" "-DCMAKE_CXX_COMPILER=clcache.exe" -DCMAKE_BUILD_TYPE=Release
         cmake --build build --config Release --target cbmc
         cmake --build build --config Release --target jbmc
         cmake --build build --config Release --target unit

doc/architectural/compilation-and-development.md

@@ -186,7 +186,7 @@ obtain an HTML report for the test and unit tests, first build the dedicated
 coverage configuration using CMake (setting `enable_coverage` and building the
 `coverage` target):
 
-    cmake -H. -Bcov-build -Denable_coverage=1 -Dparallel_tests=2
+    cmake -S . -Bcov-build -Denable_coverage=1 -Dparallel_tests=2
     make -C cov-build coverage
 
 This configures a build environment in the `cov-build/` folder with coverage