-
Notifications
You must be signed in to change notification settings - Fork 89
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
17 changed files
with
220 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
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
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
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 |
---|---|---|
@@ -0,0 +1,10 @@ | ||
# Copyright Kani Contributors | ||
# SPDX-License-Identifier: Apache-2.0 OR MIT | ||
[package] | ||
name = "simple-lib" | ||
version = "0.1.0" | ||
edition = "2018" | ||
|
||
[dependencies] | ||
|
||
[workspace] |
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 |
---|---|---|
@@ -0,0 +1,25 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
pub mod pair; | ||
pub use pair::Pair; | ||
|
||
#[cfg(test)] | ||
mod tests { | ||
#[test] | ||
fn it_works() { | ||
assert_eq!(2 + 2, 4); | ||
} | ||
} | ||
|
||
#[cfg(kani)] | ||
mod kani_tests { | ||
use super::*; | ||
|
||
#[kani::proof] | ||
fn test_sum() { | ||
let a: u64 = kani::any(); | ||
let b: u64 = kani::any(); | ||
let p = Pair::new(a, b); | ||
assert!(p.sum() == a.wrapping_add(b)); | ||
} | ||
} |
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 |
---|---|---|
@@ -0,0 +1,33 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
pub struct Pair(pub u64, pub u64); | ||
|
||
impl Pair { | ||
pub fn new(a: u64, b: u64) -> Self { | ||
Pair(a, b) | ||
} | ||
pub fn sum(&self) -> u64 { | ||
self.0.wrapping_add(self.1) | ||
} | ||
} | ||
|
||
#[cfg(test)] | ||
mod tests { | ||
use super::*; | ||
#[test] | ||
fn one_plus_two() { | ||
let p = Pair::new(1, 2); | ||
assert_eq!(p.sum(), 3); | ||
} | ||
} | ||
|
||
#[cfg(kani)] | ||
mod kani_tests { | ||
use super::*; | ||
|
||
#[kani::proof] | ||
fn test_one_plus_two() { | ||
let p = Pair::new(1, 2); | ||
assert!(p.sum() == 3); | ||
} | ||
} |
10 changes: 10 additions & 0 deletions
10
tests/cargo-coverage/simple-lib/test_one_plus_two.expected
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 |
---|---|---|
@@ -0,0 +1,10 @@ | ||
Source-based code coverage results: | ||
|
||
src/pair.rs (pair::Pair::new)\ | ||
* 6:5 - 8:6 COVERED | ||
|
||
src/pair.rs (pair::Pair::sum)\ | ||
* 9:5 - 11:6 COVERED | ||
|
||
src/pair.rs (pair::kani_tests::test_one_plus_two)\ | ||
* 29:5 - 32:6 COVERED |
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 |
---|---|---|
@@ -0,0 +1,10 @@ | ||
Source-based code coverage results: | ||
|
||
src/lib.rs (kani_tests::test_sum)\ | ||
* 19:5 - 24:6 COVERED | ||
|
||
src/pair.rs (pair::Pair::new)\ | ||
* 6:5 - 8:6 COVERED | ||
|
||
src/pair.rs (pair::Pair::sum)\ | ||
* 9:5 - 11:6 COVERED |
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 |
---|---|---|
@@ -0,0 +1,11 @@ | ||
| | ||
| #[kani::requires(a + b)] | ||
| -----------------^^^^^-- | ||
| | | | ||
| | expected `bool`, found `u64` | ||
| arguments to this function are incorrect | ||
| | ||
|
||
| | ||
| #[kani::ensures(|result| a % *result && b % *result == 0 && *result != 0)] | ||
| ^^^^^^^^^^^ expected `bool`, found `u64` |
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 |
---|---|---|
@@ -0,0 +1,13 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
// kani-flags: -Zfunction-contracts | ||
|
||
// This tests that Kani reports the "ideal" error message when contracts are non-boolean expressions | ||
// By "ideal," we mean that the error spans are as narrow as possible | ||
// (c.f. https://github.com/model-checking/kani/issues/3009) | ||
|
||
#[kani::requires(a + b)] | ||
#[kani::ensures(|result| a % *result && b % *result == 0 && *result != 0)] | ||
fn gcd(a: u64, b: u64) -> u64 { | ||
0 | ||
} |
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 |
---|---|---|
@@ -0,0 +1,17 @@ | ||
error: only one '#[kani::proof_for_contract]' attribute is allowed per harness\ | ||
invalid.rs:\ | ||
|\ | ||
| #[kani::proof_for_contract(foo)]\ | ||
| ^^^^^^^^^^^^^^ | ||
|
||
error: functions used as harnesses cannot have any arguments\ | ||
invalid.rs:\ | ||
|\ | ||
| #[kani::proof_for_contract(foo)] | ||
| ^^^^^^^^^^^^^^ | ||
|
||
error: the '#[kani::proof_for_contract]' attribute cannot be applied to generic functions\ | ||
invalid.rs:\ | ||
|\ | ||
| #[kani::proof_for_contract(foo)]\ | ||
| ^^^^^^^^^^^^^^ |
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 |
---|---|---|
@@ -0,0 +1,25 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
// kani-flags: -Zfunction-contracts | ||
|
||
// This test is to check Kani's error handling of invalid usages of the `proof_for_contract` harness. | ||
// We also ensure that all errors and warnings are printed in one compilation. | ||
|
||
#[kani::requires(true)] | ||
fn foo() {} | ||
|
||
#[kani::proof_for_contract(foo)] | ||
#[kani::proof_for_contract(foo)] | ||
fn multiple_proof_annotations() { | ||
foo(); | ||
} | ||
|
||
#[kani::proof_for_contract(foo)] | ||
fn proof_with_arg(arg: bool) { | ||
foo(); | ||
} | ||
|
||
#[kani::proof_for_contract(foo)] | ||
fn generic_harness<T: Default>() { | ||
foo(); | ||
} |
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
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 +1 @@ | ||
error: the `proof` attribute cannot be applied to generic functions | ||
error: the '#[kani::proof]' attribute cannot be applied to generic functions |
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
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
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