kani: temporary patch to model-checking/kani#4312

Author: zjp-CN

.github/gen_core.json.sh

@@ -4,7 +4,7 @@ set -o pipefail
 
 export WORKSPACE="${WORKSPACE:-$(pwd)}"
 
-export RUST_LOG=off
+export DV_LOG=off
 export OUTPUT_DIR=$WORKSPACE/assets
 export KANI_DIR=$WORKSPACE/kani/target/kani
 export VERIFY_RUST_STD_LIBRARY=$WORKSPACE/verify-rust-std/library

.github/install-kani.sh

@@ -1,11 +1,15 @@
-set -ex
+#!/usr/bin/bash
+set -exo pipefail
 
 # NOTE: verify-rust-std pins its kani commit, and
 # distributed-verification pins another.
 # So this means for verify-rust-std jobs,
 # distributed-verification may be broken to compile.
 git submodule update --init kani
 
+# Temporary patch to https://github.com/model-checking/kani/pull/4312
+cp .github/kani_contract_mode.patch kani
+
 # Install kani
 pushd kani
 git submodule update --init charon
@@ -14,7 +18,7 @@ git submodule update --init charon
 cargo build-dev -- --release
 
 export PATH=$(pwd)/scripts:$PATH
-echo PATH=$PATH >>$GITHUB_ENV
+echo PATH="$PATH" >>"$GITHUB_ENV"
 kani --version
 
 popd

.github/kani_contract_mode.patch

@@ -0,0 +1,13 @@
+diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
+index ed8bde7f8..d8f2eae87 100644
+--- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs
++++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
+@@ -71,7 +71,7 @@ const fn kani_register_contract<T, F: FnOnce() -> T>(f: F) -> T {
+                 }
+                 // Dummy function that we replace to pick the contract mode.
+                 // By default, return ORIGINAL
+-                #[inline(never)]
++                #[inline]
+                 #[kanitool::fn_marker = "kani_contract_mode"]
+                 const fn kani_contract_mode() -> kani::internal::Mode {
+                     kani::internal::ORIGINAL