Codegen Stmt:decl when seeing StorageLive

model-checking · Mar 12, 2024 · d4a82ab · d4a82ab
1 parent 39a1c59
commit d4a82ab
Showing 1 changed file with 3 additions 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,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 },