Skip to content

Commit 248fdb8

Browse files
authored
Fix codegen of skipped functions (rust-lang#1382)
We currently skip code generation of a few functions like ArgumentV1::as_usize(). We generate an unsuppported check instead. However, we still need to declare the parameters otherwise we end up with invalid symbol tables where the parameters are missing. Fixes rust-lang#1379
1 parent 913e273 commit 248fdb8

File tree

2 files changed

+10
-0
lines changed

2 files changed

+10
-0
lines changed

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

+2
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,8 @@ impl<'tcx> GotocCtx<'tcx> {
8181
tracing::info!("Double codegen of {:?}", old_sym);
8282
} else if self.should_skip_current_fn() {
8383
debug!("Skipping function {}", self.current_fn().readable_name());
84+
self.codegen_function_prelude();
85+
self.codegen_declare_variables();
8486
let body = self.codegen_fatal_error(
8587
PropertyClass::UnsupportedConstruct,
8688
&GotocCtx::unsupported_msg(

scripts/std-lib-regression.sh

+8
Original file line numberDiff line numberDiff line change
@@ -66,8 +66,16 @@ export RUSTC_LOG=error
6666
export KANIFLAGS="--goto-c --ignore-global-asm"
6767
export RUSTFLAGS="--kani-flags"
6868
export RUSTC="$KANI_DIR/target/debug/kani-compiler"
69+
# Compile rust to iRep
6970
$WRAPPER cargo build --verbose -Z build-std --lib --target $TARGET
7071

72+
# Generate goto-program. This will make sure the representation is well formed.
73+
cd target/${TARGET}/debug/deps
74+
for symtab in *.symtab.json; do
75+
echo "======== File: $symtab"
76+
symtab2gb ${symtab} --out ${symtab}.out
77+
done
78+
7179
echo
7280
echo "Finished Kani codegen for the Rust standard library successfully..."
7381
echo

0 commit comments

Comments
 (0)