Skip to content

Commit

Permalink
Enable valid_ptr post_condition harnesses
Browse files Browse the repository at this point in the history
With model-checking#2997 resolved this is expected to work.
  • Loading branch information
tautschnig committed Jan 22, 2025
1 parent 3138a96 commit ed261e3
Showing 1 changed file with 0 additions and 4 deletions.
4 changes: 0 additions & 4 deletions tests/expected/function-contract/valid_ptr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,6 @@
// kani-flags: -Zfunction-contracts -Zmem-predicates

//! Test that it is sound to use memory predicates inside a contract pre-condition.
//! We cannot validate post-condition yet. This can be done once we fix:
//! <https://github.com/model-checking/kani/issues/2997>
mod pre_condition {
/// This contract should succeed only if the input is a valid pointer.
Expand Down Expand Up @@ -35,8 +33,6 @@ mod pre_condition {
}
}

/// TODO: Enable once we fix: <https://github.com/model-checking/kani/issues/2997>
#[cfg(not_supported)]
mod post_condition {

/// This contract should fail since we are creating a dangling pointer.
Expand Down

0 comments on commit ed261e3

Please sign in to comment.