Skip to content

Commit 7c23c99

Browse files
zhassan-awstedinski
authored andcommitted
Added test for issue 703 (rust-lang#879)
1 parent 1e3a618 commit 7c23c99

File tree

1 file changed

+14
-0
lines changed

1 file changed

+14
-0
lines changed

tests/kani/Vectors/push_u8.rs

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
// Check that Kani doesn't get stuck on a program involving a Vector of u8
5+
// https://github.com/model-checking/kani/issues/703
6+
7+
fn main() {
8+
let mut v: Vec<u8> = Vec::new();
9+
v.push(5);
10+
v.push(255);
11+
assert_eq!(v.len(), 2);
12+
assert_eq!(v[0], 5);
13+
assert_eq!(v[1], 255);
14+
}

0 commit comments

Comments
 (0)