Skip to content

Commit

Permalink
test(s2n-quic-core): use a smaller length in the Kani test (#2128)
Browse files Browse the repository at this point in the history
  • Loading branch information
zhassan-aws authored Feb 15, 2024
1 parent cf0b40e commit 311ece3
Showing 1 changed file with 7 additions and 2 deletions.
9 changes: 7 additions & 2 deletions quic/s2n-quic-core/src/inet/checksum.rs
Original file line number Diff line number Diff line change
Expand Up @@ -401,13 +401,18 @@ mod tests {
}
}

// Reduce the length to 4 for Kani until
// https://github.com/model-checking/kani/issues/3030 is fixed
#[cfg(any(kani, miri))]
const LEN: usize = if cfg!(kani) { 4 } else { 32 };

/// * Compares the implementation to a port of the C code defined in the RFC
/// * Ensures partial writes are correctly handled, even if they're not at a 16 bit boundary
#[test]
#[cfg_attr(kani, kani::proof, kani::unwind(17), kani::solver(kissat))]
#[cfg_attr(kani, kani::proof, kani::unwind(9), kani::solver(cadical))]
fn differential() {
#[cfg(any(kani, miri))]
type Bytes = crate::testing::InlineVec<u8, 16>;
type Bytes = crate::testing::InlineVec<u8, LEN>;
#[cfg(not(any(kani, miri)))]
type Bytes = Vec<u8>;

Expand Down

0 comments on commit 311ece3

Please sign in to comment.