Codegen Stmt:decl when seeing StorageLive

model-checking · Mar 11, 2024 · 76fa893 · 76fa893
1 parent baf0669
commit 76fa893
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -75,7 +75,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 .goto_expr;
                 self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location)
             }
-            StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me
+            StatementKind::StorageLive(var_id) => Stmt::decl(self.codegen_local(*var_id), None, location),
             StatementKind::StorageDead(var_id) => Stmt::dead(self.codegen_local(*var_id), location),
             StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(
                 CopyNonOverlapping { src, dst, count },