Celina G. Val

We should update the rust toolchain version once every release. For 0.9, we will try to update to version nightly-2022-08-16.

RMC doesn't seem to handle stack unwind logic correctly

3

I was playing with the assertion codegen to understand how we were handling cleanup after a failure. I created the following test case: ```rust // Copyright Amazon.com, Inc. or its...

Follow up work for executable trace

1

- [ ] Use `?` to propagate the error up. - [ ] Don't use `return` at the end of the function. - [ ] Refactor `parser::parse_results` to stop using...

We should update the rust toolchain version once every release. For 0.7, we will try to update to version nightly-2022-08-02.

Kani implementation of drop for Struct<dyn T> is broken

1

We were handling `drop_in_place` incorrectly when the object to be dropped had type Struct like in the example below. For now, we are going to codegen unimplemented, so if this...

Create custom derive macro for Arbitrary type.

1

Requested feature: Create a proc_macro that allows users to annotate their structs and enums with #[derive(Invariant)] Use case: Allow users to easily generate implementation of the Invariant types for their...

In RMC, users can use special functions to generate a symbolic variable, create assumptions and expect failures. The naming schema that was initially used was C like and it didn't...

Clean up code related to broken --gen-c-runnable

3

I would like to propose that we clean the code related to the broken `--gen-c-runnable` flag. In fact, we have never enabled this flag in `kani-driver`. Please let me know...

Create a benchmark workflow

3

We don't have any reliable mechanism to assess Kani's performance. This makes trade-off assessment very challenging, since the performance cost of any change is unknown. ## Requirements: - The benchmark...

Implement checks for unchecked_* operations

1

**Requested feature:** RMC should detect failures when dealing with unchecked arithmetic operations. **Use case:** Unchecked arithmetic operations assume that the operands respect some invariant. If they don't, the result has...