-
Notifications
You must be signed in to change notification settings - Fork 97
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
add tests for markdown and printing filepaths
- Loading branch information
1 parent
fa5627b
commit 3836818
Showing
24 changed files
with
303 additions
and
20 deletions.
There are no files selected for viewing
This file was deleted.
Oops, something went wrong.
File renamed without changes.
File renamed without changes.
File renamed without changes.
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,22 @@ | ||
#!/usr/bin/env bash | ||
# Copyright Kani Contributors | ||
# SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
||
# Check that the json file produced by `kani list` is correct. | ||
# Note that the list.expected file omits the value for "kani-version" | ||
# to avoid having to update the test every time we bump versions. | ||
|
||
output=$(kani list -Z list -Z function-contracts src/lib.rs --format json) | ||
|
||
# Check that Kani prints the absolute path to kani-list.json | ||
absolute_path="$(cd "$(dirname "kani-list.json")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.json")" | ||
expected_last_line="Wrote list results to $absolute_path" | ||
last_line=$(echo "$output" | tail -n 1) | ||
|
||
if [ "$last_line" = "$expected_last_line" ]; then | ||
cat kani-list.json | ||
exit 0 | ||
else | ||
echo "Test failed: Absolute path to kani-list.json is missing from printed output" | ||
exit 1 | ||
fi |
File renamed without changes.
File renamed without changes.
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 = "cargo_list" | ||
version = "0.1.0" | ||
edition = "2021" | ||
|
||
[lints.rust] | ||
unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } |
File renamed without changes.
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,14 @@ | ||
|
||
Contracts: | ||
| | Function | Contract Harnesses (#[kani::proof_for_contract]) | | ||
| ----- | ----------------------------- | -------------------------------------------------------------- | | ||
| | example::implementation::bar | example::verify::check_bar | | ||
| | example::implementation::foo | example::verify::check_foo_u32, example::verify::check_foo_u64 | | ||
| | example::implementation::func | example::verify::check_func | | ||
| | example::prep::parse | NONE | | ||
| Total | 4 | 4 | | ||
|
||
|
||
Standard Harnesses (#[kani::proof]): | ||
1. standard_harnesses::example::verify::check_modify | ||
2. standard_harnesses::example::verify::check_new |
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,14 @@ | ||
|
||
Contracts: | ||
| | Function | Contract Harnesses (#[kani::proof_for_contract]) | | ||
| ----- | ----------------------------- | -------------------------------------------------------------- | | ||
| | example::implementation::bar | example::verify::check_bar | | ||
| | example::implementation::foo | example::verify::check_foo_u32, example::verify::check_foo_u64 | | ||
| | example::implementation::func | example::verify::check_func | | ||
| | example::prep::parse | NONE | | ||
| Total | 4 | 4 | | ||
|
||
|
||
Standard Harnesses (#[kani::proof]): | ||
1. standard_harnesses::example::verify::check_modify | ||
2. standard_harnesses::example::verify::check_new |
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,22 @@ | ||
#!/usr/bin/env bash | ||
# Copyright Kani Contributors | ||
# SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
||
# Check that the MD file produced by `kani list` is correct. | ||
# Note that the list.expected file omits the value for "kani-version" | ||
# to avoid having to update the test every time we bump versions. | ||
|
||
output=$(kani list -Z list -Z function-contracts src/lib.rs --format markdown) | ||
|
||
# Check that Kani prints the absolute path to kani-list.md | ||
absolute_path="$(cd "$(dirname "kani-list.md")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.md")" | ||
expected_last_line="Wrote list results to $absolute_path" | ||
last_line=$(echo "$output" | tail -n 1) | ||
|
||
if [ "$last_line" = "$expected_last_line" ]; then | ||
cat kani-list.md | ||
exit 0 | ||
else | ||
echo "Test failed: Absolute path to kani-list.md is missing from printed output" | ||
exit 1 | ||
fi |
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,68 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
// | ||
//! This test replicates the module structure from the running example in the list RFC. | ||
//! It ensures that the list command works across modules, and with modifies clauses, history expressions, and generic functions. | ||
mod standard_harnesses; | ||
|
||
#[cfg(kani)] | ||
mod example { | ||
mod prep { | ||
#[kani::requires(s.len() < 10)] | ||
fn parse(s: &str) -> u32 { | ||
s.parse().unwrap() | ||
} | ||
} | ||
|
||
pub mod implementation { | ||
#[kani::requires(*x < 4)] | ||
#[kani::requires(*x > 2)] | ||
#[kani::ensures(|_| old(*x - 1) == *x)] | ||
#[kani::ensures(|_| *x == 4)] | ||
#[kani::modifies(x)] | ||
pub fn bar(x: &mut u32) { | ||
*x += 1; | ||
} | ||
|
||
#[kani::requires(*x < 100)] | ||
#[kani::modifies(x)] | ||
pub fn func(x: &mut i32) { | ||
*x *= 1; | ||
} | ||
|
||
#[kani::requires(true)] | ||
#[kani::ensures(|_| old(*x) == *x)] | ||
pub fn foo<T: Copy + std::cmp::PartialEq>(x: &mut T) -> T { | ||
*x | ||
} | ||
} | ||
|
||
mod verify { | ||
use crate::example::implementation; | ||
|
||
#[kani::proof_for_contract(implementation::bar)] | ||
fn check_bar() { | ||
let mut x = 7; | ||
implementation::bar(&mut x); | ||
} | ||
|
||
#[kani::proof_for_contract(implementation::foo)] | ||
fn check_foo_u32() { | ||
let mut x: u32 = 7; | ||
implementation::foo(&mut x); | ||
} | ||
|
||
#[kani::proof_for_contract(implementation::foo)] | ||
fn check_foo_u64() { | ||
let mut x: u64 = 7; | ||
implementation::foo(&mut x); | ||
} | ||
|
||
#[kani::proof_for_contract(implementation::func)] | ||
fn check_func() { | ||
let mut x = 7; | ||
implementation::func(&mut x); | ||
} | ||
} | ||
} |
15 changes: 15 additions & 0 deletions
15
tests/script-based-pre/cargo_list_md/src/standard_harnesses.rs
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,15 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
// | ||
//! Test that the cargo list command can find Kani attributes across multiple files. | ||
#[cfg(kani)] | ||
mod example { | ||
mod verify { | ||
#[kani::proof] | ||
fn check_modify() {} | ||
|
||
#[kani::proof] | ||
fn check_new() {} | ||
} | ||
} |
This file was deleted.
Oops, something went wrong.
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,4 @@ | ||
# Copyright Kani Contributors | ||
# SPDX-License-Identifier: Apache-2.0 OR MIT | ||
script: list.sh | ||
expected: list.expected |
File renamed without changes.
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,22 @@ | ||
#!/usr/bin/env bash | ||
# Copyright Kani Contributors | ||
# SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
||
# Check that the JSON file produced by `kani list` is correct. | ||
# Note that the list.expected file omits the value for "kani-version" | ||
# to avoid having to update the test every time we bump versions. | ||
|
||
output=$(kani list -Z list -Z function-contracts src/lib.rs --format json) | ||
|
||
# Check that Kani prints the absolute path to kani-list.json | ||
absolute_path="$(cd "$(dirname "kani-list.json")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.json")" | ||
expected_last_line="Wrote list results to $absolute_path" | ||
last_line=$(echo "$output" | tail -n 1) | ||
|
||
if [ "$last_line" = "$expected_last_line" ]; then | ||
cat kani-list.json | ||
exit 0 | ||
else | ||
echo "Test failed: Absolute path to kani-list.json is missing from printed output" | ||
exit 1 | ||
fi |
File renamed without changes.
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 @@ | ||
kani-list.md |
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,4 @@ | ||
# Copyright Kani Contributors | ||
# SPDX-License-Identifier: Apache-2.0 OR MIT | ||
script: list.sh | ||
expected: list.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,14 @@ | ||
|
||
Contracts: | ||
| | Function | Contract Harnesses (#[kani::proof_for_contract]) | | ||
| ----- | ----------------------------- | -------------------------------------------------------------- | | ||
| | example::implementation::bar | example::verify::check_bar | | ||
| | example::implementation::foo | example::verify::check_foo_u32, example::verify::check_foo_u64 | | ||
| | example::implementation::func | example::verify::check_func | | ||
| | example::prep::parse | NONE | | ||
| Total | 4 | 4 | | ||
|
||
|
||
Standard Harnesses (#[kani::proof]): | ||
1. example::verify::check_modify | ||
2. example::verify::check_new |
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,22 @@ | ||
#!/usr/bin/env bash | ||
# Copyright Kani Contributors | ||
# SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
||
# Check that the MD file produced by `kani list` is correct. | ||
# Note that the list.expected file omits the value for "kani-version" | ||
# to avoid having to update the test every time we bump versions. | ||
|
||
output=$(kani list -Z list -Z function-contracts src/lib.rs --format markdown) | ||
|
||
# Check that Kani prints the absolute path to kani-list.md | ||
absolute_path="$(cd "$(dirname "kani-list.md")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.md")" | ||
expected_last_line="Wrote list results to $absolute_path" | ||
last_line=$(echo "$output" | tail -n 1) | ||
|
||
if [ "$last_line" = "$expected_last_line" ]; then | ||
cat kani-list.md | ||
exit 0 | ||
else | ||
echo "Test failed: Absolute path to kani-list.md is missing from printed output" | ||
exit 1 | ||
fi |
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,71 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
// | ||
//! This test replicates the module structure from the running example in the list RFC. | ||
//! It ensures that the list command across modules, and with modifies clauses, history expressions, and generic functions. | ||
mod example { | ||
mod prep { | ||
#[kani::requires(s.len() < 10)] | ||
fn parse(s: &str) -> u32 { | ||
s.parse().unwrap() | ||
} | ||
} | ||
|
||
pub mod implementation { | ||
#[kani::requires(*x < 4)] | ||
#[kani::requires(*x > 2)] | ||
#[kani::ensures(|_| old(*x - 1) == *x)] | ||
#[kani::ensures(|_| *x == 4)] | ||
#[kani::modifies(x)] | ||
pub fn bar(x: &mut u32) { | ||
*x += 1; | ||
} | ||
|
||
#[kani::requires(true)] | ||
#[kani::ensures(|_| old(*x) == *x)] | ||
pub fn foo<T: Copy + std::cmp::PartialEq>(x: &mut T) -> T { | ||
*x | ||
} | ||
|
||
#[kani::requires(*x < 100)] | ||
#[kani::modifies(x)] | ||
pub fn func(x: &mut i32) { | ||
*x *= 1; | ||
} | ||
} | ||
|
||
mod verify { | ||
use crate::example::implementation; | ||
|
||
#[kani::proof_for_contract(implementation::bar)] | ||
fn check_bar() { | ||
let mut x = 7; | ||
implementation::bar(&mut x); | ||
} | ||
|
||
#[kani::proof_for_contract(implementation::foo)] | ||
fn check_foo_u32() { | ||
let mut x: u32 = 7; | ||
implementation::foo(&mut x); | ||
} | ||
|
||
#[kani::proof_for_contract(implementation::foo)] | ||
fn check_foo_u64() { | ||
let mut x: u64 = 7; | ||
implementation::foo(&mut x); | ||
} | ||
|
||
#[kani::proof_for_contract(implementation::func)] | ||
fn check_func() { | ||
let mut x = 7; | ||
implementation::func(&mut x); | ||
} | ||
|
||
#[kani::proof] | ||
fn check_modify() {} | ||
|
||
#[kani::proof] | ||
fn check_new() {} | ||
} | ||
} |