Update toolchain to 2024-09-23 (#3544)

Changes required due to: - rust-lang/rust#130593 Sync from rustfmt - rust-lang/rust#124895 Disallow hidden references to mutable static With the exception of changes to `rust-toolchain.toml`, `rustfmt.toml`, and `library/kani/src/futures.rs` all changes were automatically created by running `scripts/kani-fmt.sh`. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
model-checking · Sep 24, 2024 · 9dc09e7 · 9dc09e7
1 parent 2755592
commit 9dc09e7
Show file tree

Hide file tree

Showing 131 changed files with 503 additions and 546 deletions.
diff --git a/cprover_bindings/src/cbmc_string.rs b/cprover_bindings/src/cbmc_string.rs
@@ -3,9 +3,9 @@
 
 use lazy_static::lazy_static;
 use std::sync::Mutex;
+use string_interner::StringInterner;
 use string_interner::backend::StringBackend;
 use string_interner::symbol::SymbolU32;
-use string_interner::StringInterner;
 
 /// This class implements an interner for Strings.
 /// CBMC objects to have a large number of strings which refer to names: symbols, files, etc.

diff --git a/cprover_bindings/src/env.rs b/cprover_bindings/src/env.rs
@@ -8,8 +8,8 @@
 //! c.f. CBMC code [src/ansi-c/ansi_c_internal_additions.cpp].
 //! One possible invocation of this insertion in CBMC can be found in \[ansi_c_languaget::parse\].
 
-use super::goto_program::{Expr, Location, Symbol, SymbolTable, Type};
 use super::MachineModel;
+use super::goto_program::{Expr, Location, Symbol, SymbolTable, Type};
 use num::bigint::BigInt;
 fn int_constant<T>(name: &str, value: T) -> Symbol
 where

diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
@@ -285,13 +285,10 @@ pub fn arithmetic_overflow_result_type(operand_type: Type) -> Type {
  // give the struct the name "overflow_result_<type>", e.g.
  // "overflow_result_Unsignedbv"
  let name: InternedString = format!("overflow_result_{operand_type:?}").into();
- Type::struct_type(
- name,
- vec![
- DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type),
- DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()),
- ],
- )
+ Type::struct_type(name, vec![
+ DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type),
+ DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()),
+ ])
 }
 
 ///////////////////////////////////////////////////////////////////////////////////////////////

diff --git a/cprover_bindings/src/goto_program/mod.rs b/cprover_bindings/src/goto_program/mod.rs
@@ -17,8 +17,8 @@ mod typ;
 
 pub use builtin::BuiltinFn;
 pub use expr::{
- arithmetic_overflow_result_type, ArithmeticOverflowResult, BinaryOperator, Expr, ExprValue,
- SelfOperator, UnaryOperator, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD,
+ ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, ArithmeticOverflowResult,
+ BinaryOperator, Expr, ExprValue, SelfOperator, UnaryOperator, arithmetic_overflow_result_type,
 };
 pub use location::Location;
 pub use stmt::{Stmt, StmtBody, SwitchCase};

diff --git a/cprover_bindings/src/goto_program/symbol_table.rs b/cprover_bindings/src/goto_program/symbol_table.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use super::super::{env, MachineModel};
+use super::super::{MachineModel, env};
 use super::{BuiltinFn, FunctionContract, Stmt, Symbol};
 use crate::InternedString;
 use std::collections::BTreeMap;

diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use self::DatatypeComponent::*;
 use self::Type::*;
-use super::super::utils::{aggr_tag, max_int, min_int};
 use super::super::MachineModel;
+use super::super::utils::{aggr_tag, max_int, min_int};
 use super::{Expr, SymbolTable};
 use crate::cbmc_string::InternedString;
 use std::collections::BTreeMap;
@@ -1598,10 +1598,10 @@ mod type_tests {
  fn check_typedef_struct_properties() {
  // Create a struct with a random field.
  let struct_name: InternedString = "MyStruct".into();
- let struct_type = Type::struct_type(
- struct_name,
- vec![DatatypeComponent::Field { name: "field".into(), typ: Double }],
- );
+ let struct_type = Type::struct_type(struct_name, vec![DatatypeComponent::Field {
+ name: "field".into(),
+ typ: Double,
+ }]);
  // Insert a field to the sym table to represent the struct field.
  let mut sym_table = SymbolTable::new(machine_model_test_stub());
  sym_table.ensure(struct_type.type_name().unwrap(), |_, name| {

diff --git a/cprover_bindings/src/irep/goto_binary_serde.rs b/cprover_bindings/src/irep/goto_binary_serde.rs
@@ -1205,12 +1205,12 @@ mod sharing_stats {
 mod tests {
  use super::GotoBinarySerializer;
  use super::IrepNumbering;
+ use crate::InternedString;
  use crate::cbmc_string::InternString;
- use crate::irep::goto_binary_serde::GotoBinaryDeserializer;
  use crate::irep::Irep;
  use crate::irep::IrepId;
+ use crate::irep::goto_binary_serde::GotoBinaryDeserializer;
  use crate::linear_map;
- use crate::InternedString;
  use linear_map::LinearMap;
  use std::io::BufWriter;
  /// Utility function : creates a Irep representing a single symbol.

diff --git a/cprover_bindings/src/irep/irep.rs b/cprover_bindings/src/irep/irep.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! The actual `Irep` structure, and associated constructors, getters, and setters.
 
-use super::super::goto_program::{Location, Type};
 use super::super::MachineModel;
+use super::super::goto_program::{Location, Type};
 use super::{IrepId, ToIrep};
 use crate::cbmc_string::InternedString;
 use crate::linear_map;

diff --git a/cprover_bindings/src/irep/serialize.rs b/cprover_bindings/src/irep/serialize.rs
@@ -1,10 +1,10 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! This crate implements irep serialization using serde Serializer.
-use crate::irep::{Irep, IrepId, Symbol, SymbolTable};
 use crate::InternedString;
-use serde::ser::{SerializeMap, Serializer};
+use crate::irep::{Irep, IrepId, Symbol, SymbolTable};
 use serde::Serialize;
+use serde::ser::{SerializeMap, Serializer};
 
 impl Serialize for Irep {
  fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
@@ -145,14 +145,16 @@ impl Serialize for Symbol {
 #[cfg(test)]
 mod test {
  use super::*;
- use serde_test::{assert_ser_tokens, Token};
+ use serde_test::{Token, assert_ser_tokens};
  #[test]
  fn serialize_irep() {
  let irep = Irep::empty();
- assert_ser_tokens(
- &irep,
- &[Token::Map { len: None }, Token::String("id"), Token::String("empty"), Token::MapEnd],
- );
+ assert_ser_tokens(&irep, &[
+ Token::Map { len: None },
+ Token::String("id"),
+ Token::String("empty"),
+ Token::MapEnd,
+ ]);
  }
 
  #[test]
@@ -187,80 +189,77 @@ mod test {
  is_weak: false,
  };
  sym_table.insert(symbol);
- assert_ser_tokens(
- &sym_table,
- &[
- Token::Map { len: None },
- Token::String("symbolTable"),
- Token::Map { len: Some(1) },
- Token::String("my_name"),
- // symbol start
- Token::Map { len: None },
- // type irep
- Token::String("type"),
- Token::Map { len: None },
- Token::String("id"),
- Token::String("empty"),
- Token::MapEnd,
- // value irep
- Token::String("value"),
- Token::Map { len: None },
- Token::String("id"),
- Token::String("empty"),
- Token::MapEnd,
- // value locaton
- Token::String("location"),
- Token::Map { len: None },
- Token::String("id"),
- Token::String("empty"),
- Token::MapEnd,
- Token::String("name"),
- Token::String("my_name"),
- Token::String("module"),
- Token::String(""),
- Token::String("baseName"),
- Token::String(""),
- Token::String("prettyName"),
- Token::String(""),
- Token::String("mode"),
- Token::String(""),
- Token::String("isType"),
- Token::Bool(false),
- Token::String("isMacro"),
- Token::Bool(false),
- Token::String("isExported"),
- Token::Bool(false),
- Token::String("isInput"),
- Token::Bool(false),
- Token::String("isOutput"),
- Token::Bool(false),
- Token::String("isStateVar"),
- Token::Bool(false),
- Token::String("isProperty"),
- Token::Bool(false),
- Token::String("isStaticLifetime"),
- Token::Bool(false),
- Token::String("isThreadLocal"),
- Token::Bool(false),
- Token::String("isLvalue"),
- Token::Bool(false),
- Token::String("isFileLocal"),
- Token::Bool(false),
- Token::String("isExtern"),
- Token::Bool(false),
- Token::String("isVolatile"),
- Token::Bool(false),
- Token::String("isParameter"),
- Token::Bool(false),
- Token::String("isAuxiliary"),
- Token::Bool(false),
- Token::String("isWeak"),
- Token::Bool(false),
- Token::MapEnd,
- Token::MapEnd,
- Token::MapEnd,
- ],
- );
+ assert_ser_tokens(&sym_table, &[
+ Token::Map { len: None },
+ Token::String("symbolTable"),
+ Token::Map { len: Some(1) },
+ Token::String("my_name"),
+ // symbol start
+ Token::Map { len: None },
+ // type irep
+ Token::String("type"),
+ Token::Map { len: None },
+ Token::String("id"),
+ Token::String("empty"),
+ Token::MapEnd,
+ // value irep
+ Token::String("value"),
+ Token::Map { len: None },
+ Token::String("id"),
+ Token::String("empty"),
+ Token::MapEnd,
+ // value locaton
+ Token::String("location"),
+ Token::Map { len: None },
+ Token::String("id"),
+ Token::String("empty"),
+ Token::MapEnd,
+ Token::String("name"),
+ Token::String("my_name"),
+ Token::String("module"),
+ Token::String(""),
+ Token::String("baseName"),
+ Token::String(""),
+ Token::String("prettyName"),
+ Token::String(""),
+ Token::String("mode"),
+ Token::String(""),
+ Token::String("isType"),
+ Token::Bool(false),
+ Token::String("isMacro"),
+ Token::Bool(false),
+ Token::String("isExported"),
+ Token::Bool(false),
+ Token::String("isInput"),
+ Token::Bool(false),
+ Token::String("isOutput"),
+ Token::Bool(false),
+ Token::String("isStateVar"),
+ Token::Bool(false),
+ Token::String("isProperty"),
+ Token::Bool(false),
+ Token::String("isStaticLifetime"),
+ Token::Bool(false),
+ Token::String("isThreadLocal"),
+ Token::Bool(false),
+ Token::String("isLvalue"),
+ Token::Bool(false),
+ Token::String("isFileLocal"),
+ Token::Bool(false),
+ Token::String("isExtern"),
+ Token::Bool(false),
+ Token::String("isVolatile"),
+ Token::Bool(false),
+ Token::String("isParameter"),
+ Token::Bool(false),
+ Token::String("isAuxiliary"),
+ Token::Bool(false),
+ Token::String("isWeak"),
+ Token::Bool(false),
+ Token::MapEnd,
+ Token::MapEnd,
+ Token::MapEnd,
+ ]);
  }
 
  #[test]
@@ -269,41 +268,38 @@ mod test {
  let one_irep = Irep::one();
  let sub_irep = Irep::just_sub(vec![empty_irep.clone(), one_irep]);
  let top_irep = Irep::just_sub(vec![sub_irep, empty_irep]);
- assert_ser_tokens(
- &top_irep,
- &[
- // top_irep
- Token::Map { len: None },
- Token::String("id"),
- Token::String(""),
- Token::String("sub"),
- Token::Seq { len: Some(2) },
- // sub_irep
- Token::Map { len: None },
- Token::String("id"),
- Token::String(""),
- Token::String("sub"),
- Token::Seq { len: Some(2) },
- // empty_irep
- Token::Map { len: None },
- Token::String("id"),
- Token::String("empty"),
- Token::MapEnd,
- // one_irep
- Token::Map { len: None },
- Token::String("id"),
- Token::String("1"),
- Token::MapEnd,
- Token::SeqEnd,
- Token::MapEnd,
- // empty_irep
- Token::Map { len: None },
- Token::String("id"),
- Token::String("empty"),
- Token::MapEnd,
- Token::SeqEnd,
- Token::MapEnd,
- ],
- );
+ assert_ser_tokens(&top_irep, &[
+ // top_irep
+ Token::Map { len: None },
+ Token::String("id"),
+ Token::String(""),
+ Token::String("sub"),
+ Token::Seq { len: Some(2) },
+ // sub_irep
+ Token::Map { len: None },
+ Token::String("id"),
+ Token::String(""),
+ Token::String("sub"),
+ Token::Seq { len: Some(2) },
+ // empty_irep
+ Token::Map { len: None },
+ Token::String("id"),
+ Token::String("empty"),
+ Token::MapEnd,
+ // one_irep
+ Token::Map { len: None },
+ Token::String("id"),
+ Token::String("1"),
+ Token::MapEnd,
+ Token::SeqEnd,
+ Token::MapEnd,
+ // empty_irep
+ Token::Map { len: None },
+ Token::String("id"),
+ Token::String("empty"),
+ Token::MapEnd,
+ Token::SeqEnd,
+ Token::MapEnd,
+ ]);
  }
 }