forked from model-checking/kani
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Documentation: Updates for Installation (model-checking#972)
* Documentation: Updates for Installation * Add `kani::proof` tag to test * Move note up
- Loading branch information
1 parent
189b7f2
commit 8366bc7
Showing
1 changed file
with
28 additions
and
14 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,32 +1,40 @@ | ||
# Kani Installation Guide | ||
# Installation | ||
|
||
Kani must currently be built from source. | ||
|
||
In general, the following dependencies are required. Note: These dependencies may be installed by running the CI scripts shown below and there is no need to install them separately, for their respective OS. | ||
In general, the following dependencies are required. | ||
|
||
1. Cargo installed via rustup | ||
> **Note:** These dependencies may be installed by running the CI scripts shown | ||
> below and there is no need to install them separately, for their respective | ||
> OS. | ||
1. Cargo installed via [rustup](https://rustup.rs/) | ||
2. [CBMC](https://github.com/diffblue/cbmc) (>= 5.53.1) | ||
3. [CBMC Viewer](https://github.com/awslabs/aws-viewer-for-cbmc) (>= 2.10) | ||
|
||
## Installing on Ubuntu 20.04 | ||
Kani has been tested in [Ubuntu](#install-dependencies-on-ubuntu) and [macOS](##install-dependencies-on-macos) platforms. | ||
|
||
## Install dependencies on Ubuntu | ||
|
||
The simplest way to install (especially if you're using a fresh VM) is following our CI scripts: | ||
Support is available for Ubuntu 18.04 and 20.04. | ||
The simplest way to install dependencies (especially if you're using a fresh VM) | ||
is following our CI scripts: | ||
|
||
``` | ||
# git clone [email protected]:model-checking/kani.git | ||
git clone https://github.com/model-checking/kani.git | ||
cd kani | ||
git submodule update --init | ||
./scripts/setup/ubuntu-20.04/install_deps.sh | ||
./scripts/setup/ubuntu-20.04/install_cbmc.sh | ||
./scripts/setup/ubuntu/install_deps.sh | ||
./scripts/setup/ubuntu/install_cbmc.sh | ||
./scripts/setup/install_viewer.sh 2.10 | ||
./scripts/setup/install_rustup.sh | ||
source $HOME/.cargo/env | ||
``` | ||
|
||
## Installing on Mac OS | ||
## Install dependencies on macOS | ||
|
||
You need to have [Homebrew](https://brew.sh/) installed already. | ||
Support is available for macOS 10.15. You need to have [Homebrew](https://brew.sh/) installed already. | ||
|
||
``` | ||
# git clone [email protected]:model-checking/kani.git | ||
|
@@ -40,9 +48,9 @@ git submodule update --init | |
source $HOME/.cargo/env | ||
``` | ||
|
||
## Building and testing Kani | ||
## Build and test Kani | ||
|
||
Build Kani's packages: | ||
Build the Kani package: | ||
|
||
``` | ||
cargo build | ||
|
@@ -62,7 +70,7 @@ All Kani regression tests completed successfully. | |
|
||
## Try running Kani | ||
|
||
Get the Kani script in your path: | ||
Add the Kani script to your path: | ||
|
||
```bash | ||
export PATH=$(pwd)/scripts:$PATH | ||
|
@@ -72,6 +80,7 @@ Create a test file: | |
|
||
```rust | ||
// File: test.rs | ||
#[kani::proof] | ||
fn main() { | ||
assert!(1 == 2); | ||
} | ||
|
@@ -86,7 +95,7 @@ kani test.rs | |
You should get a result like this one: | ||
|
||
``` | ||
[snipped output] | ||
[...] | ||
RESULTS: | ||
Check 1: main.assertion.1 | ||
- Status: FAILURE | ||
|
@@ -95,4 +104,9 @@ Check 1: main.assertion.1 | |
VERIFICATION:- FAILED | ||
``` | ||
|
||
Fix the test and you should see `kani` succeed. | ||
Fix the test and you should see a result like this one: | ||
|
||
``` | ||
[...] | ||
VERIFICATION:- SUCCESSFUL | ||
``` |