From d4a82ab81759234090628a9bc8f9d5924b2e8584 Mon Sep 17 00:00:00 2001
From: Kareem Khazem <karkhaz@amazon.com>
Date: Mon, 11 Mar 2024 20:32:11 +0000
Subject: [PATCH] Codegen Stmt:decl when seeing StorageLive

---
 kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 1c830fda438d..6379a023423f 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -75,7 +75,9 @@ 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 },