Skip to content

Commit

Permalink
Update toolchain to 2024-08-05
Browse files Browse the repository at this point in the history
* Remove `gen_function_local_variable` and `initializer_fn_name`, the
  last uses of both of which were removed in model-checking#3305.
* Remove `arg_count`, which was introduced in model-checking#3363, but not actually
  used.
* Remove `insert_bb`, which was introduced in model-checking#3382, but not actually
  used.

The toolchain upgrade to 2024-08-04 includes several bugfixes to
dead-code analysis in rustc, explaining why we the recent PRs as listed
above weren't flagged before for introducing dead code.

Resolves: model-checking#3411
  • Loading branch information
tautschnig committed Aug 5, 2024
1 parent 03e2df3 commit 80cd280
Show file tree
Hide file tree
Showing 4 changed files with 4 additions and 35 deletions.
11 changes: 0 additions & 11 deletions kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
Original file line number Diff line number Diff line change
Expand Up @@ -139,17 +139,6 @@ impl<'tcx> GotocCtx<'tcx> {
sym
}

// 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,
loc: Location,
) -> Symbol {
self.gen_stack_variable(c, fname, "var", t, loc)
}

/// Given a counter `c` a function name `fname, and a prefix `prefix`, generates a new function local variable
/// It is an error to reuse an existing `c`, `fname` `prefix` tuple.
fn gen_stack_variable(
Expand Down
4 changes: 0 additions & 4 deletions kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
Original file line number Diff line number Diff line change
Expand Up @@ -45,10 +45,6 @@ impl<'tcx> GotocCtx<'tcx> {
(name, base_name)
}

pub fn initializer_fn_name(var_name: &str) -> String {
format!("{var_name}_init")
}

/// The name for a tuple field
pub fn tuple_fld_name(n: usize) -> String {
format!("{n}")
Expand Down
22 changes: 3 additions & 19 deletions kani-compiler/src/kani_middle/transform/body.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,14 +17,10 @@ pub struct MutableBody {

/// Declarations of locals within the function.
///
/// The first local is the return value pointer, followed by `arg_count`
/// locals for the function arguments, followed by any user-declared
/// variables and temporaries.
/// The first local is the return value pointer, followed by locals for the function arguments,
/// followed by any user-declared variables and temporaries.
locals: Vec<LocalDecl>,

/// The number of arguments this function takes.
arg_count: usize,

/// Debug information pertaining to user variables, including captures.
var_debug_info: Vec<VarDebugInfo>,

Expand Down Expand Up @@ -54,15 +50,10 @@ impl MutableBody {
&self.locals
}

pub fn arg_count(&self) -> usize {
self.arg_count
}

/// Create a mutable body from the original MIR body.
pub fn from(body: Body) -> Self {
MutableBody {
locals: body.locals().to_vec(),
arg_count: body.arg_locals().len(),
spread_arg: body.spread_arg(),
blocks: body.blocks,
var_debug_info: body.var_debug_info,
Expand All @@ -72,14 +63,7 @@ impl MutableBody {

/// Create the new body consuming this mutable body.
pub fn into(self) -> Body {
Body::new(
self.blocks,
self.locals,
self.arg_count,
self.var_debug_info,
self.spread_arg,
self.span,
)
Body::new(self.blocks, self.locals, self.var_debug_info, self.spread_arg, self.span)
}

/// Add a new local to the body with the given attributes.
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2024-08-03"
channel = "nightly-2024-08-05"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

0 comments on commit 80cd280

Please sign in to comment.