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

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

@@ -81,6 +81,8 @@ impl<'tcx> GotocCtx<'tcx> {
             tracing::info!("Double codegen of {:?}", old_sym);
         } else if self.should_skip_current_fn() {
             debug!("Skipping function {}", self.current_fn().readable_name());
+            self.codegen_function_prelude();
+            self.codegen_declare_variables();
             let body = self.codegen_fatal_error(
                 PropertyClass::UnsupportedConstruct,
                 &GotocCtx::unsupported_msg(

scripts/std-lib-regression.sh

@@ -66,8 +66,16 @@ export RUSTC_LOG=error
 export KANIFLAGS="--goto-c --ignore-global-asm"
 export RUSTFLAGS="--kani-flags"
 export RUSTC="$KANI_DIR/target/debug/kani-compiler"
+# Compile rust to iRep
 $WRAPPER cargo build --verbose -Z build-std --lib --target $TARGET
 
+# Generate goto-program. This will make sure the representation is well formed.
+cd target/${TARGET}/debug/deps
+for symtab in *.symtab.json; do
+    echo "======== File: $symtab"
+    symtab2gb ${symtab} --out ${symtab}.out
+done
+
 echo
 echo "Finished Kani codegen for the Rust standard library successfully..."
 echo