Skip to content

Commit d53296a

Browse files
authored
Update rustc to nightly-2022-08-30 (rust-lang#1624)
1 parent 4093b2d commit d53296a

File tree

7 files changed

+28
-18
lines changed

7 files changed

+28
-18
lines changed

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,7 @@ impl<'tcx> GotocCtx<'tcx> {
112112
self.codegen_function_prelude();
113113
self.codegen_declare_variables();
114114

115-
mir.basic_blocks().iter_enumerated().for_each(|(bb, bbd)| self.codegen_block(bb, bbd));
115+
mir.basic_blocks.iter_enumerated().for_each(|(bb, bbd)| self.codegen_block(bb, bbd));
116116

117117
let loc = self.codegen_span(&mir.span);
118118
let stmts = self.current_fn_mut().extract_block();
@@ -354,10 +354,13 @@ impl<'tcx> GotocCtx<'tcx> {
354354
/// If the attribute is named `kanitool::name`, this extracts `name`
355355
fn kanitool_attr_name(attr: &ast::Attribute) -> Option<String> {
356356
match &attr.kind {
357-
ast::AttrKind::Normal(ast::AttrItem { path: ast::Path { segments, .. }, .. }, _)
358-
if (!segments.is_empty()) && segments[0].ident.as_str() == "kanitool" =>
359-
{
360-
Some(segments[1].ident.as_str().to_string())
357+
ast::AttrKind::Normal(normal) => {
358+
let segments = &normal.item.path.segments;
359+
if (!segments.is_empty()) && segments[0].ident.as_str() == "kanitool" {
360+
Some(segments[1].ident.as_str().to_string())
361+
} else {
362+
None
363+
}
361364
}
362365
_ => None,
363366
}

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -296,7 +296,7 @@ impl<'tcx> GotocCtx<'tcx> {
296296
self,
297297
self.tcx
298298
.instance_mir(instance.def)
299-
.basic_blocks()
299+
.basic_blocks
300300
.indices()
301301
.map(|bb| format!("{:?}", bb))
302302
.collect(),

kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,7 @@ impl<'tcx> GotocCtx<'tcx> {
8181
for l in mir.args_iter().chain(mir.vars_and_temps_iter()) {
8282
debug!("let {:?}: {:?}", l, self.local_ty(l));
8383
}
84-
for (bb, bbd) in mir.basic_blocks().iter_enumerated() {
84+
for (bb, bbd) in mir.basic_blocks.iter_enumerated() {
8585
debug!("block {:?}", bb);
8686
for stmt in &bbd.statements {
8787
debug!("{:?}", stmt);

rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2022-08-16"
5+
channel = "nightly-2022-08-30"
66
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

tests/kani/Iterator/flat_map.rs

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,3 @@ pub fn check_flat_map_char() {
1313
assert_eq!(hi_flat.next(), Some('i'));
1414
assert_eq!(hi_flat.next(), None);
1515
}
16-
17-
#[kani::proof]
18-
#[kani::unwind(4)]
19-
fn check_flat_map_len() {
20-
let hello = ["Hi", "!"];
21-
let length = hello.iter().flat_map(|s| s.chars()).count();
22-
assert_eq!(length, 3);
23-
}
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
//
4+
// This test checks the result of using Iterator::flat_map. We had some projection
5+
// issues with this in the past.
6+
// This currently fails due to missing core::str::count::char_count_general_case
7+
// std function:
8+
// https://github.com/model-checking/kani/issues/1213
9+
10+
#[kani::proof]
11+
#[kani::unwind(4)]
12+
fn check_flat_map_len() {
13+
let hello = ["Hi", "!"];
14+
let length = hello.iter().flat_map(|s| s.chars()).count();
15+
assert_eq!(length, 3);
16+
}

tests/ui/code-location/expected

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
module/mod.rs:10:5 in function module::not_empty
22
main.rs:13:5 in function same_file
33
/toolchains/
4-
alloc/src/vec/mod.rs:2920:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
4+
alloc/src/vec/mod.rs:2921:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
55

66
VERIFICATION:- SUCCESSFUL
7-

0 commit comments

Comments
 (0)