Skip to content

Commit

Permalink
Add tests for issues rust-lang#763 and rust-lang#702 (rust-lang#812)
Browse files Browse the repository at this point in the history
  • Loading branch information
danielsn authored and tedinski committed Feb 10, 2022
1 parent 726bd2d commit 4eea798
Show file tree
Hide file tree
Showing 2 changed files with 26 additions and 0 deletions.
18 changes: 18 additions & 0 deletions tests/kani/Vectors/fixme_702.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

// Failing example from https://github.com/model-checking/kani/issues/702
// Push 5 elements to force the vector to resize, then check that the values were correctly copied.
fn main() {
let mut v = Vec::new();
v.push(72);
v.push(2);
v.push(3);
v.push(4);
v.push(5);
assert!(v[0] == 72);
assert!(v[1] == 2);
assert!(v[2] == 3);
assert!(v[3] == 4);
assert!(v[4] == 5);
}
8 changes: 8 additions & 0 deletions tests/kani/Vectors/fixme_763.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

// Failing example from https://github.com/model-checking/kani/issues/763
fn main() {
let x = Vec::<i32>::new();
for i in x {}
}

0 comments on commit 4eea798

Please sign in to comment.