Skip to content

Commit 5941fbb

Browse files
authored
Improve std-lib-regression script (rust-lang#1360)
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.
1 parent 69a021f commit 5941fbb

File tree

1 file changed

+14
-1
lines changed

1 file changed

+14
-1
lines changed

scripts/std-lib-regression.sh

+14-1
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ fi
2525

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

3030
echo
3131
echo "Starting Kani codegen for the Rust standard library..."
@@ -39,6 +39,19 @@ fi
3939
cargo new std_lib_test --lib
4040
cd std_lib_test
4141

42+
# Add some content to the rust file including an std function that is non-generic.
43+
echo '
44+
#[kani::proof]
45+
fn check_format() {
46+
assert!("2021".parse::<u32>().unwrap() == 2021);
47+
}
48+
' > src/lib.rs
49+
50+
# Until we add support to this via our bundle, rebuild the kani library too.
51+
echo "
52+
kani = {path=\"${KANI_DIR}/library/kani\"}
53+
" >> Cargo.toml
54+
4255
# Use same nightly toolchain used to build Kani
4356
cp ${KANI_DIR}/rust-toolchain.toml .
4457

0 commit comments

Comments
 (0)