Skip to content

Commit

Permalink
Remove is-a-parameter from gen_stack_variable (model-checking#3137)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
tautschnig committed Apr 10, 2024
1 parent 43475da commit e906cde
Showing 1 changed file with 3 additions and 5 deletions.
8 changes: 3 additions & 5 deletions kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
}
Expand All @@ -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)
Expand Down

0 comments on commit e906cde

Please sign in to comment.