Skip to content

Commit

Permalink
Update rust toolchain to nightly 1.66.0-nightly (rust-lang#1804)
Browse files Browse the repository at this point in the history
* update rust toolchain to nightly 1.66.0-nightly

* move to code block instead of escaping

* fix missing quote

* disable clippy check: clippy::uninlined-format-args

Co-authored-by: rahulku <luhark@a07817b4397e.ant.amazon.com>
  • Loading branch information
rahulku and rahulku authored Oct 27, 2022
1 parent 88859d8 commit 221fe3b
Show file tree
Hide file tree
Showing 7 changed files with 13 additions and 14 deletions.
1 change: 1 addition & 0 deletions .cargo/config.toml
Original file line number Diff line number Diff line change
Expand Up @@ -32,4 +32,5 @@ rustflags = [ # Global lints/warnings. Need to use underscore instead of -.
# New lints that we are not compliant yet
"-Aclippy::needless-borrow",
"-Aclippy::bool-to-int-with-if",
"-Aclippy::uninlined-format-args",
]
10 changes: 5 additions & 5 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -506,10 +506,10 @@ impl<'tcx> GotocCtx<'tcx> {
self.codegen_ty(typ).to_pointer()
}

/// A reference to a Struct<dyn T> { .., data: T} is translated to
/// A reference to a `Struct<dyn T>` { .., data: T} is translated to
/// struct RefToTrait {
/// Struct<dyn T>* data;
/// Metadata<dyn T>* vtable;
/// `Struct<dyn T>* data`;
/// `Metadata<dyn T>* vtable;`
/// }
/// Note: T is a `typedef` but data represents the space in memory occupied by
/// the concrete type. We just don't know its size during compilation time.
Expand Down Expand Up @@ -1264,8 +1264,8 @@ impl<'tcx> GotocCtx<'tcx> {
/// Dynamic function calls first parameter is self which must be one of the following:
///
/// As of Jul 2022:
/// P = &Self | &mut Self | Box<Self> | Rc<Self> | Arc<Self>
/// S = P | Pin<P>
/// `P = &Self | &mut Self | Box<Self> | Rc<Self> | Arc<Self>`
/// `S = P | Pin<P>`
///
/// See <https://doc.rust-lang.org/reference/items/traits.html#object-safety> for more details.
fn codegen_dynamic_function_sig(&mut self, sig: PolyFnSig<'tcx>) -> Type {
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
Original file line number Diff line number Diff line change
Expand Up @@ -112,15 +112,15 @@ impl<'tcx> GotocCtx<'tcx> {
}

/// Add a prefix of the form:
/// \[<prefix>\]
/// \[`<prefix>`\]
/// to the provided message
pub fn add_prefix_to_msg(msg: &str, prefix: &str) -> String {
format!("[{}] {}", prefix, msg)
}

/// Generate a message for the reachability check of an assert with ID
/// `check_id`. The message is of the form:
/// \[KANI_REACHABILITY_CHECK\] <ID of assert>
/// \[KANI_REACHABILITY_CHECK\] `<ID of assert>`
/// The check_id is generated using the GotocCtx::next_check_id method and
/// is a unique string identifier for that check.
pub fn reachability_check_message(check_id: &str) -> String {
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ impl<'tcx> GotocCtx<'tcx> {
RAW_PTR_FROM_BOX.iter().fold(box_expr, |expr, name| expr.member(name, &self.symbol_table))
}

/// Box<T> initializer
/// `Box<T>` initializer
///
/// Traverse over the Box representation and only initialize the raw_ptr field. All other
/// members are left uninitialized.
Expand Down Expand Up @@ -177,7 +177,7 @@ impl<'tcx> GotocCtx<'tcx> {
}
}

/// Best effort check if the struct represents a std::ptr::NonNull<T>.
/// Best effort check if the struct represents a `std::ptr::NonNull<T>`.
///
/// This assumes the following structure. Any changes to this will break this code.
/// ```
Expand Down
4 changes: 2 additions & 2 deletions 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-2022-10-11"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
channel = "nightly-2022-10-25"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
2 changes: 0 additions & 2 deletions scripts/kani-regression.sh
Original file line number Diff line number Diff line change
Expand Up @@ -70,8 +70,6 @@ for testp in "${TESTS[@]}"; do
suite=${testl[0]}
mode=${testl[1]}
echo "Check compiletest suite=$suite mode=$mode"
# Note: `cargo-kani` tests fail if we do not add `$(pwd)` to `--build-base`
# Tracking issue: https://github.com/model-checking/kani/issues/755
cargo run -p compiletest --quiet -- --suite $suite --mode $mode --quiet
done

Expand Down
2 changes: 1 addition & 1 deletion tests/ui/code-location/expected
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
module/mod.rs:10:5 in function module::not_empty
main.rs:13:5 in function same_file
/toolchains/
alloc/src/vec/mod.rs:3031:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
alloc/src/vec/mod.rs:3028:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop

VERIFICATION:- SUCCESSFUL

0 comments on commit 221fe3b

Please sign in to comment.