Skip to content

Commit

Permalink
Update toolchain to 2024-08-05 (model-checking#3416)
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.
* Mark `arg_count`, which was introduced in model-checking#3363, as `allow(dead_code)`
as it will soon be used.
* Mark `insert_bb`, which was introduced in model-checking#3382, as `allow(dead_code)`
as it will soon be 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

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
tautschnig authored Aug 5, 2024
1 parent f2831f4 commit 520cb3e
Show file tree
Hide file tree
Showing 4 changed files with 3 additions and 16 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
2 changes: 2 additions & 0 deletions kani-compiler/src/kani_middle/transform/body.rs
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@ impl MutableBody {
&self.locals
}

#[allow(dead_code)]
pub fn arg_count(&self) -> usize {
self.arg_count
}
Expand Down Expand Up @@ -330,6 +331,7 @@ impl MutableBody {
/// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as
/// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the
/// terminator of the newly inserted basic block.
#[allow(dead_code)]
pub fn insert_bb(
&mut self,
mut bb: BasicBlock,
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 520cb3e

Please sign in to comment.