Skip to content

Commit 9b625bb

Browse files
committed
add test to demonstrate problem with current approach to parsing closures
1 parent fc16198 commit 9b625bb

1 file changed

Lines changed: 17 additions & 0 deletions

File tree

tests/pattern_in_closure.rs

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
use anodized::contract;
2+
3+
#[contract(
4+
ensures: |(a, b)| a <= b,
5+
ensures: |(a, b)| (a, b) == pair || (b, a) == pair,
6+
)]
7+
fn sort_pair(pair: (i32, i32)) -> (i32, i32) {
8+
let (a, b) = pair;
9+
// Deliberately wrong implementation to trigger the contract.
10+
(b, a)
11+
}
12+
13+
#[test]
14+
#[should_panic(expected = "Postcondition failed: |(a, b)| a <= b")]
15+
fn test_sort_fail_postcondition() {
16+
sort_pair((2, 5));
17+
}

0 commit comments

Comments
 (0)