Skip to content
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
1 change: 1 addition & 0 deletions docs/src/build-from-source.md
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ is following our CI scripts:
git clone https://github.com/model-checking/kani.git
cd kani
git submodule update --init
# For Ubuntu 20.04, use: `./scripts/setup/ubuntu-20.04/install_deps.sh`
./scripts/setup/ubuntu/install_deps.sh
# If you haven't already (or from https://rustup.rs/):
./scripts/setup/install_rustup.sh
Expand Down
1 change: 0 additions & 1 deletion scripts/setup/ubuntu-20.04

This file was deleted.

32 changes: 32 additions & 0 deletions scripts/setup/ubuntu-20.04/install_cbmc.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
#!/bin/bash
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT

set -eu

# Source kani-dependencies to get CBMC_VERSION
source kani-dependencies

if [ -z "${CBMC_VERSION:-}" ]; then
echo "$0: Error: CBMC_VERSION is not specified"
exit 1
fi

# Binaries are not released for Ubuntu 20.04, so build from source
WORK_DIR=$(mktemp -d)
git clone \
--branch cbmc-${CBMC_VERSION} --depth 1 \
https://github.com/diffblue/cbmc \
"${WORK_DIR}"

pushd "${WORK_DIR}"

cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" \
-DCMAKE_C_COMPILER=gcc-10 -DCMAKE_CXX_COMPILER=g++-10 \
-DCMAKE_CXX_STANDARD_LIBRARIES=-lstdc++fs \
-DCMAKE_CXX_FLAGS=-Wno-error=register
cmake --build build -- -j$(nproc)
sudo make -C build install

popd
rm -rf "${WORK_DIR}"
40 changes: 40 additions & 0 deletions scripts/setup/ubuntu-20.04/install_deps.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
#!/bin/bash
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT

set -eu

# Dependencies.
DEPS=(
bison
cmake
curl
flex
# CBMC needs g++-10 which doesn't come by default on Ubuntu 20.04
g++-10
gcc
git
gpg-agent
make
patch
wget
zlib1g
zlib1g-dev
)

set -x

# Github promises weekly build image updates, but recommends running
# `sudo apt-get update` before installing packages in case the `apt`
# index is stale. This prevents package installation failures.
# https://docs.github.com/en/actions/using-github-hosted-runners/customizing-github-hosted-runners#installing-software-on-ubuntu-runners
sudo apt-get --yes update

sudo DEBIAN_FRONTEND=noninteractive apt-get install --no-install-recommends --yes "${DEPS[@]}"

# Get the directory containing this script
SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"

${SCRIPT_DIR}/install_cbmc.sh
# The Kissat installation script is platform-independent, so is placed one level up
${SCRIPT_DIR}/../install_kissat.sh
8 changes: 8 additions & 0 deletions scripts/setup/ubuntu-20.04/install_doc_deps.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
#!/bin/bash
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT

set -eux

cargo install mdbook-graphviz
DEBIAN_FRONTEND=noninteractive sudo apt-get install --no-install-recommends --yes graphviz
Loading