Skip to content

Commit

Permalink
Update rustc to nightly-2022-08-30 (#1624)
Browse files Browse the repository at this point in the history
  • Loading branch information
zhassan-aws committed Sep 1, 2022
1 parent 4093b2d commit d53296a
Show file tree
Hide file tree
Showing 7 changed files with 28 additions and 18 deletions.
13 changes: 8 additions & 5 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ impl<'tcx> GotocCtx<'tcx> {
self.codegen_function_prelude();
self.codegen_declare_variables();

mir.basic_blocks().iter_enumerated().for_each(|(bb, bbd)| self.codegen_block(bb, bbd));
mir.basic_blocks.iter_enumerated().for_each(|(bb, bbd)| self.codegen_block(bb, bbd));

let loc = self.codegen_span(&mir.span);
let stmts = self.current_fn_mut().extract_block();
Expand Down Expand Up @@ -354,10 +354,13 @@ impl<'tcx> GotocCtx<'tcx> {
/// If the attribute is named `kanitool::name`, this extracts `name`
fn kanitool_attr_name(attr: &ast::Attribute) -> Option<String> {
match &attr.kind {
ast::AttrKind::Normal(ast::AttrItem { path: ast::Path { segments, .. }, .. }, _)
if (!segments.is_empty()) && segments[0].ident.as_str() == "kanitool" =>
{
Some(segments[1].ident.as_str().to_string())
ast::AttrKind::Normal(normal) => {
let segments = &normal.item.path.segments;
if (!segments.is_empty()) && segments[0].ident.as_str() == "kanitool" {
Some(segments[1].ident.as_str().to_string())
} else {
None
}
}
_ => None,
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -296,7 +296,7 @@ impl<'tcx> GotocCtx<'tcx> {
self,
self.tcx
.instance_mir(instance.def)
.basic_blocks()
.basic_blocks
.indices()
.map(|bb| format!("{:?}", bb))
.collect(),
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ impl<'tcx> GotocCtx<'tcx> {
for l in mir.args_iter().chain(mir.vars_and_temps_iter()) {
debug!("let {:?}: {:?}", l, self.local_ty(l));
}
for (bb, bbd) in mir.basic_blocks().iter_enumerated() {
for (bb, bbd) in mir.basic_blocks.iter_enumerated() {
debug!("block {:?}", bb);
for stmt in &bbd.statements {
debug!("{:?}", stmt);
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-2022-08-16"
channel = "nightly-2022-08-30"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
8 changes: 0 additions & 8 deletions tests/kani/Iterator/flat_map.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,3 @@ pub fn check_flat_map_char() {
assert_eq!(hi_flat.next(), Some('i'));
assert_eq!(hi_flat.next(), None);
}

#[kani::proof]
#[kani::unwind(4)]
fn check_flat_map_len() {
let hello = ["Hi", "!"];
let length = hello.iter().flat_map(|s| s.chars()).count();
assert_eq!(length, 3);
}
16 changes: 16 additions & 0 deletions tests/kani/Iterator/flat_map_count_fixme.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
// This test checks the result of using Iterator::flat_map. We had some projection
// issues with this in the past.
// This currently fails due to missing core::str::count::char_count_general_case
// std function:
// https://github.com/model-checking/kani/issues/1213

#[kani::proof]
#[kani::unwind(4)]
fn check_flat_map_len() {
let hello = ["Hi", "!"];
let length = hello.iter().flat_map(|s| s.chars()).count();
assert_eq!(length, 3);
}
3 changes: 1 addition & 2 deletions tests/ui/code-location/expected
Original file line number Diff line number Diff line change
@@ -1,7 +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:2920:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
alloc/src/vec/mod.rs:2921:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop

VERIFICATION:- SUCCESSFUL

0 comments on commit d53296a

Please sign in to comment.