Skip to content

Commit 5648fd2

Browse files
authored
Merge pull request #171 from coord-e/coord-e/exclude-zero-is_pos_neg
Return false for zero in i32::{is_positive,is_negative} specs
2 parents a36a534 + a1fc71a commit 5648fd2

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

std.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -705,14 +705,14 @@ fn _extern_spec_i32_signum(x: i32) -> i32 {
705705

706706
#[thrust::extern_spec_fn]
707707
#[thrust_macros::requires(true)]
708-
#[thrust_macros::ensures((x < 0 && result == false) || (x >= 0 && result == true))]
708+
#[thrust_macros::ensures((x <= 0 && result == false) || (x > 0 && result == true))]
709709
fn _extern_spec_i32_is_positive(x: i32) -> bool {
710710
i32::is_positive(x)
711711
}
712712

713713
#[thrust::extern_spec_fn]
714714
#[thrust_macros::requires(true)]
715-
#[thrust_macros::ensures((x <= 0 && result == true) || (x > 0 && result == false))]
715+
#[thrust_macros::ensures((x < 0 && result == true) || (x >= 0 && result == false))]
716716
fn _extern_spec_i32_is_negative(x: i32) -> bool {
717717
i32::is_negative(x)
718718
}

0 commit comments

Comments
 (0)