File tree 3 files changed +39
-0
lines changed
tests/perf/btreeset/insert_multi
3 files changed +39
-0
lines changed Original file line number Diff line number Diff line change
1
+ # Copyright Kani Contributors
2
+ # SPDX-License-Identifier: Apache-2.0 OR MIT
3
+
4
+ [package ]
5
+ name = " insert_multi"
6
+ version = " 0.1.0"
7
+ edition = " 2021"
8
+
9
+ # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
10
+
11
+ [dependencies ]
Original file line number Diff line number Diff line change
1
+ ** 2 of 2 cover properties satisfied
2
+ VERIFICATION:- SUCCESSFUL
Original file line number Diff line number Diff line change
1
+ // Copyright Kani Contributors
2
+ // SPDX-License-Identifier: Apache-2.0 OR MIT
3
+
4
+ //! This test checks the performance of pushing multiple non-det elements onto a
5
+ //! `BtreeSet`
6
+
7
+ use kani:: cover;
8
+ use std:: collections:: BTreeSet ;
9
+
10
+ #[ kani:: proof]
11
+ #[ kani:: unwind( 3 ) ]
12
+ #[ kani:: solver( cadical) ]
13
+ fn insert_multi ( ) {
14
+ const N : usize = 2 ;
15
+ let mut set: BTreeSet < i32 > = BTreeSet :: new ( ) ;
16
+ for _i in 0 ..N {
17
+ set. insert ( kani:: any ( ) ) ;
18
+ }
19
+ assert ! ( !set. is_empty( ) ) ;
20
+ // all elements are the same
21
+ cover ! ( set. len( ) == 1 ) ;
22
+ // two unique elements
23
+ cover ! ( set. len( ) == 2 ) ;
24
+ }
25
+
26
+ fn main ( ) { }
You can’t perform that action at this time.
0 commit comments