Skip to content

Commit

Permalink
Add a regression test for no_std feature (#3837)
Browse files Browse the repository at this point in the history
Add a regression test to ensure that we can run Kani in crates with the
`no_std` feature enabled.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
carolynzech authored Jan 16, 2025
1 parent 72637ee commit 35015dc
Show file tree
Hide file tree
Showing 3 changed files with 35 additions and 0 deletions.
9 changes: 9 additions & 0 deletions tests/cargo-kani/no-std/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT

[package]
name = "no-std"
version = "0.1.0"
edition = "2024"

[dependencies]
1 change: 1 addition & 0 deletions tests/cargo-kani/no-std/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Complete - 2 successfully verified harnesses, 0 failures, 2 total.
25 changes: 25 additions & 0 deletions tests/cargo-kani/no-std/src/lib.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

// Ensure that "extern crate kani" is sufficient to run Kani when no_std is enabled.

#![no_std]
extern crate kani;

fn add(x: u8, y: u8) -> u8 {
x + y
}

#[kani::proof]
fn prove_add() {
let x = kani::any_where(|n| *n < u8::MAX / 2);
let y = kani::any_where(|n| *n < u8::MAX / 2);
add(x, y);
}

use kani::cover;

#[kani::proof]
fn verify_point() {
cover!(true)
}

0 comments on commit 35015dc

Please sign in to comment.