File tree Expand file tree Collapse file tree 3 files changed +39
-0
lines changed
tests/perf/btreeset/insert_multi Expand file tree Collapse file tree 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