Skip to content

Commit

Permalink
fmt
Browse files Browse the repository at this point in the history
  • Loading branch information
Matias Scharager committed Jul 9, 2024
1 parent f04cb09 commit 6cef19b
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions library/kani/src/internal.rs
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,7 @@ pub fn apply_closure<T, U: Fn(&T) -> bool>(f: U, x: &T) -> bool {
/// It behaves exaclty like `kani::any<T>()`, except it will check for the trait bounds
/// at compilation time. It allows us to avoid type checking errors while using function
/// contracts only for verification.
#[crate::unstable(feature="function-contracts", issue="none", reason="function-contracts")]
#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
#[rustc_diagnostic_item = "KaniAnyModifies"]
#[inline(never)]
#[doc(hidden)]
Expand All @@ -118,7 +118,7 @@ pub fn any_modifies<T>() -> T {
/// Recieves a reference to a pointer-like object and assigns kani::any_modifies to that object.
/// Only for use within function contracts and will not be replaced if the recursive or function stub
/// replace contracts are not used.
#[crate::unstable(feature="function-contracts", issue="none", reason="function-contracts")]
#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
#[rustc_diagnostic_item = "KaniWriteAny"]
#[inline(never)]
#[doc(hidden)]
Expand All @@ -130,21 +130,21 @@ pub fn write_any<T: ?Sized>(_pointer: &T) {
unreachable!()
}

#[crate::unstable(feature="function-contracts", issue="none", reason="function-contracts")]
#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
#[rustc_diagnostic_item = "KaniWriteAnySlice"]
#[inline(always)]
pub fn write_any_slice<T: Arbitrary>(slice: &mut [T]) {
slice.fill_with(T::any)
}

#[crate::unstable(feature="function-contracts", issue="none", reason="function-contracts")]
#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
#[rustc_diagnostic_item = "KaniWriteAnySlim"]
#[inline(always)]
pub fn write_any_slim<T: Arbitrary>(pointer: &mut T) {
*pointer = T::any()
}

#[crate::unstable(feature="function-contracts", issue="none", reason="function-contracts")]
#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
#[rustc_diagnostic_item = "KaniWriteAnyStr"]
#[inline(always)]
pub fn write_any_str(s: &mut str) {
Expand Down

0 comments on commit 6cef19b

Please sign in to comment.