Skip to content

Commit

Permalink
Improve std-lib-regression script (#1360)
Browse files Browse the repository at this point in the history
Add a dummy proof-harness to it and fix the issue with duplicated lang
items that was triggered when trying to resolve the dependencies. The
issues seemed to be related to the fact that `kani` crate was built with
a different version of the `std` library.

For now, we explicitly add the `kani` crate as a dependency so it gets
rebuilt with the fresh std.
  • Loading branch information
celinval authored Jul 12, 2022
1 parent 69a021f commit 5941fbb
Showing 1 changed file with 14 additions and 1 deletion.
15 changes: 14 additions & 1 deletion scripts/std-lib-regression.sh
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ fi

# Get Kani root
SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
KANI_DIR=$SCRIPT_DIR/..
KANI_DIR=$(dirname "$SCRIPT_DIR")

echo
echo "Starting Kani codegen for the Rust standard library..."
Expand All @@ -39,6 +39,19 @@ fi
cargo new std_lib_test --lib
cd std_lib_test

# Add some content to the rust file including an std function that is non-generic.
echo '
#[kani::proof]
fn check_format() {
assert!("2021".parse::<u32>().unwrap() == 2021);
}
' > src/lib.rs

# Until we add support to this via our bundle, rebuild the kani library too.
echo "
kani = {path=\"${KANI_DIR}/library/kani\"}
" >> Cargo.toml

# Use same nightly toolchain used to build Kani
cp ${KANI_DIR}/rust-toolchain.toml .

Expand Down

0 comments on commit 5941fbb

Please sign in to comment.