Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Contracts and Harnesses for
unchecked_neg
(rust-lang#102)
Towards rust-lang#59 ### Changes * Added contracts for `unchecked_neg` (located in `library/core/src/num/int_macros.rs`) * Added a harness for `unchecked_neg` of each signed integer type * `i8`, `i16`, `i32`, `i64`, `i128`, `isize` --- 6 harnesses in total. * Fixed comments. ### Revalidation 1. Per the discussion in rust-lang#59, we have to **build and run Kani from `feature/verify-rust-std` branch**. 2. To revalidate the verification results, run the following command. `<harness_to_run>` can be either `num::verify` to run all harnesses or `num::verify::<harness_name>` (e.g. `check_unchecked_neg_i8`) to run a specific harness. ``` kani verify-std "path/to/library" \ --harness <harness_to_run> \ -Z unstable-options \ -Z function-contracts \ -Z mem-predicates ``` All default harnesses should pass. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: yew005 <yew005@ucsd.edu> Co-authored-by: Rajath Kotyal <53811196+rajathkotyal@users.noreply.github.com> Co-authored-by: rajathmCMU <rajathkotyal@gmail.com>
- Loading branch information