Skip to content

Commit e906cde

Browse files
authored
Remove is-a-parameter from gen_stack_variable (rust-lang#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.
1 parent 43475da commit e906cde

File tree

1 file changed

+3
-5
lines changed
  • kani-compiler/src/codegen_cprover_gotoc/context

1 file changed

+3
-5
lines changed

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

+3-5
Original file line numberDiff line numberDiff line change
@@ -137,7 +137,7 @@ impl<'tcx> GotocCtx<'tcx> {
137137

138138
// Generate a Symbol Expression representing a function variable from the MIR
139139
pub fn gen_function_local_variable(&mut self, c: u64, fname: &str, t: Type) -> Symbol {
140-
self.gen_stack_variable(c, fname, "var", t, Location::none(), false)
140+
self.gen_stack_variable(c, fname, "var", t, Location::none())
141141
}
142142

143143
/// 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> {
149149
prefix: &str,
150150
t: Type,
151151
loc: Location,
152-
is_param: bool,
153152
) -> Symbol {
154153
let base_name = format!("{prefix}_{c}");
155154
let name = format!("{fname}::1::{base_name}");
156-
let symbol = Symbol::variable(name, base_name, t, loc).with_is_parameter(is_param);
155+
let symbol = Symbol::variable(name, base_name, t, loc);
157156
self.symbol_table.insert(symbol.clone());
158157
symbol
159158
}
@@ -167,8 +166,7 @@ impl<'tcx> GotocCtx<'tcx> {
167166
loc: Location,
168167
) -> (Expr, Stmt) {
169168
let c = self.current_fn_mut().get_and_incr_counter();
170-
let var =
171-
self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc, false).to_expr();
169+
let var = self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc).to_expr();
172170
let value = value.or_else(|| self.codegen_default_initializer(&var));
173171
let decl = Stmt::decl(var.clone(), value, loc);
174172
(var, decl)

0 commit comments

Comments
 (0)