diff --git a/scripts/std-lib-regression.sh b/scripts/std-lib-regression.sh index 1381b4ba7f83..f3a2a7ac8a89 100755 --- a/scripts/std-lib-regression.sh +++ b/scripts/std-lib-regression.sh @@ -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..." @@ -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::().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 .