From e906cde630dc4d9105fda37b636a39328c34641c Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 10 Apr 2024 15:22:15 +0200
Subject: [PATCH] Remove is-a-parameter from gen_stack_variable (#3137)

A function-local variable cannot at the same time be a parameter. Alas,
all uses of gen_stack_variable passed in `false` for `is_param`, so this
wasn't making a difference anyway.
---
 .../src/codegen_cprover_gotoc/context/goto_ctx.rs         | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
index 3a6501d544d8..095f907228a4 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -137,7 +137,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     // Generate a Symbol Expression representing a function variable from the MIR
     pub fn gen_function_local_variable(&mut self, c: u64, fname: &str, t: Type) -> Symbol {
-        self.gen_stack_variable(c, fname, "var", t, Location::none(), false)
+        self.gen_stack_variable(c, fname, "var", t, Location::none())
     }
 
     /// Given a counter `c` a function name `fname, and a prefix `prefix`, generates a new function local variable
@@ -149,11 +149,10 @@ impl<'tcx> GotocCtx<'tcx> {
         prefix: &str,
         t: Type,
         loc: Location,
-        is_param: bool,
     ) -> Symbol {
         let base_name = format!("{prefix}_{c}");
         let name = format!("{fname}::1::{base_name}");
-        let symbol = Symbol::variable(name, base_name, t, loc).with_is_parameter(is_param);
+        let symbol = Symbol::variable(name, base_name, t, loc);
         self.symbol_table.insert(symbol.clone());
         symbol
     }
@@ -167,8 +166,7 @@ impl<'tcx> GotocCtx<'tcx> {
         loc: Location,
     ) -> (Expr, Stmt) {
         let c = self.current_fn_mut().get_and_incr_counter();
-        let var =
-            self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc, false).to_expr();
+        let var = self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc).to_expr();
         let value = value.or_else(|| self.codegen_default_initializer(&var));
         let decl = Stmt::decl(var.clone(), value, loc);
         (var, decl)