File tree Expand file tree Collapse file tree 2 files changed +26
-0
lines changed Expand file tree Collapse file tree 2 files changed +26
-0
lines changed Original file line number Diff line number Diff line change
1
+ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2
+ // SPDX-License-Identifier: Apache-2.0 OR MIT
3
+
4
+ // Failing example from https://github.com/model-checking/kani/issues/702
5
+ // Push 5 elements to force the vector to resize, then check that the values were correctly copied.
6
+ fn main ( ) {
7
+ let mut v = Vec :: new ( ) ;
8
+ v. push ( 72 ) ;
9
+ v. push ( 2 ) ;
10
+ v. push ( 3 ) ;
11
+ v. push ( 4 ) ;
12
+ v. push ( 5 ) ;
13
+ assert ! ( v[ 0 ] == 72 ) ;
14
+ assert ! ( v[ 1 ] == 2 ) ;
15
+ assert ! ( v[ 2 ] == 3 ) ;
16
+ assert ! ( v[ 3 ] == 4 ) ;
17
+ assert ! ( v[ 4 ] == 5 ) ;
18
+ }
Original file line number Diff line number Diff line change
1
+ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2
+ // SPDX-License-Identifier: Apache-2.0 OR MIT
3
+
4
+ // Failing example from https://github.com/model-checking/kani/issues/763
5
+ fn main ( ) {
6
+ let x = Vec :: < i32 > :: new ( ) ;
7
+ for i in x { }
8
+ }
You can’t perform that action at this time.
0 commit comments