Skip to content

Fix cmake flag in COMPILING.md and other docs #5208

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jan 2, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions .travis.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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]")
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand Down
6 changes: 3 additions & 3 deletions COMPILING.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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:
```
Expand All @@ -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`
2 changes: 1 addition & 1 deletion buildspec-linux-cmake-gcc-cov.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
2 changes: 1 addition & 1 deletion buildspec-linux-cmake-gcc.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
2 changes: 1 addition & 1 deletion buildspec-windows-cmake.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion doc/architectural/compilation-and-development.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down