Skip to content

Commit 3256bfc

Browse files
committed
improve tests
1 parent 0dbeda7 commit 3256bfc

1 file changed

Lines changed: 10 additions & 8 deletions

File tree

crates/anodized/tests/trait_fn_patterns.rs

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -15,13 +15,13 @@ trait Trait {
1515
}
1616

1717
#[spec(
18-
requires: [
19-
lower < upper,
20-
i >= lower,
21-
i < upper,
18+
requires: lower < upper,
19+
ensures: [
20+
*output >= lower,
21+
*output < upper,
2222
],
2323
)]
24-
fn func_3((i, Bounds { lower, upper }): (i32, Bounds)) {
24+
fn func_3((i, Bounds { lower, upper }): (i32, Bounds)) -> i32 {
2525
unimplemented!()
2626
}
2727
}
@@ -37,7 +37,9 @@ struct Type;
3737
impl Trait for Type {
3838
fn func_1(_: (i32, i32)) {}
3939
fn func_2(_: Bounds) {}
40-
fn func_3(_: (i32, Bounds)) {}
40+
fn func_3((i, _): (i32, Bounds)) -> i32 {
41+
i
42+
}
4143
}
4244

4345
#[cfg(all(anodized_print, anodized_panic))]
@@ -61,8 +63,8 @@ fn test_2() {
6163

6264
#[cfg(all(anodized_print, anodized_panic))]
6365
#[test]
64-
#[should_panic(expected = r#"precondition failed:
65-
i < upper"#)]
66+
#[should_panic(expected = r#"postcondition failed:
67+
| output | * output < upper"#)]
6668
fn test_3() {
6769
let _ = Type::func_3((42, Bounds { lower: 1, upper: 5 }));
6870
}

0 commit comments

Comments
 (0)