Celina G. Val

Add vacuity test for contradictory requires clause

2

Requested feature: Contract verification should fail if the requires clause can never be satisfied Use case: Detect user mistakes when writing contracts Link to relevant documentation (Rust reference, Nomicon, RFC):...

Tracking Issue: Automatically ensure validity invariants of unsafe operations

1

Requested feature: Kani should automatically check if unsafe operations can break validity invariants which can trigger UB. According to the Rust reference, producing an invalid value, even in private fields...

Support harness partition

2

Requested feature: Users should be able to partition a harness which will be verified as if it was two or more harnesses. Use case: One way to mitigate the cost...

Users should be able to create contracts suitable for verification but not stubbing

2

Requested feature: Enable contract verification for functions that Kani cannot use as stub today. Use case: Verification of functions that return types that do not implement `Arbitrary`. Link to relevant...

Add proper support to C-FFI calls

13

Requested feature: Add support to verifying combination of Rust and C code. Use case: Users have C legacy code or external libraries that they would like to verify against their...

Invalid path reported for Rust toolchain

6

I got this error: ``` Errors File [/Users/ec2-user/.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/unix/thread_local_dtor.rs] Function [std::sys::unix::thread_local_dtor::register_dtor] Line [69] [[trace] call to foreign "C" function `_tlv_atexit` is not currently supported by Kani. Please post your example at...

Requested feature: Optimize code generation of constants Use case: Improve solver performance due to better constant propagation. We currently generate an allocation when initializing an ADT with more than one...

Requested feature: Users should be able to define types that have no safety and validity restrictions, allowing Kani to optimize arbitrary value generation. Use case: Users that have an array...

**Proposed change:** Our build bundle CI job always rebuild CBMC for Ubuntu 18, since DiffBlue no longer releases a compatible version. This adds a 20min overhead and can be easily...

Add methods to create StableMIR constant

1

I've been experimenting with transforming the StableMIR to instrument the code with potential UB checks. The modified body will only be used by our analysis tool, however, constants in StableMIR...