Qinheping Hu
Qinheping Hu
*Description of changes: the original implementation of the functions directly update the fields of ```*iter```, while the stub functions create a nondet object ```rval```, updates the fields of ```rval```, and...
After executing the for-loop in ```aws_array_list_mem_swap```, the pointers ```item1``` and ```item2``` could be one past the boundaries. Therefore, both pointers could be outside the address space of the program and...
RFC for loop contracts in Kani. Rendered version available [here](https://github.com/qinheping/kani/blob/rfc-loop-contracts/rfc/src/rfcs/0012-loop-contracts.md). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and...
This PR introduce the loop contracts annotation for while-loops using proc-macro. The A while loop of the form ``` rust #[kani::loop_invariant(inv)] while guard { body } ``` is annotated as...
Requested feature: Loop contracts Use case: Verify the provided loop contracts, and use the loop contracts to abstract out the loops from the verification process. Link to relevant documentation (Rust...
Adds a new regression test suite for core functions on which we will prove the safety with loop contracts. By submitting this pull request, I confirm that my contribution is...
Requested feature: Currently loop contracts implementation in #3151 doesn't support loop contracts in closures and coroutines. We want to allow loop contracts be correctly applied in closures and coroutines. Use...
Requested feature: The loop contracts support #3151 is based on CBMC's loop contracts, which doesn't support `malloc` and `free` in loops with loop contracts. We want to support it to...
I tried this code: ```rust// Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT use std::mem; extern crate kani; use kani::{kani_exists, kani_forall}; #[kani::proof] fn main() { let original_v = vec![kani::any::(); 3];...
Requested feature: Allowing users to specify loop modifies instead of inferring them. Link to relevant documentation (Rust reference, Nomicon, RFC): #3167 Test case: ```rust #![feature(stmt_expr_attributes)] #![feature(proc_macro_hygiene)] #[kani::proof] fn simple_while_loop_with_old_harness() {...