Skip to content

Commit

Permalink
Apply suggestions from code review
Browse files Browse the repository at this point in the history
Co-authored-by: Celina G. Val <celinval@amazon.com>
  • Loading branch information
JustusAdam and celinval authored Jun 28, 2023
1 parent be13831 commit cc0e7d7
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions library/kani_macros/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream {
///
/// This is part of the function contract API, together with [`ensures`].
///
/// The contents of the attribute is a condtition over the input values to the
/// The contents of the attribute is a condition over the input values to the
/// annotated function. All Rust syntax is supported, even calling other
/// functions, but the computations must be side effect free, e.g. it cannot
/// perform I/O or use mutable memory.
Expand Down Expand Up @@ -245,11 +245,11 @@ mod sysroot {
/// Is rewritten to
///
/// ```rs
/// fn foo_enusres_<hash of foo>(x: u32, result: u32) {
/// fn foo_ensures_<hash of foo>(x: u32, result: u32) {
/// x < result
/// }
///
/// #[kanitook::ensures = "foo_ensures_<hash of foo>"]
/// #[kanitool::ensures = "foo_ensures_<hash of foo>"]
/// fn foo(x: u32) -> u32 { .. }
/// ```
///
Expand Down

0 comments on commit cc0e7d7

Please sign in to comment.