Ted Kaminski

--debug doesn't work anymore

1

``` $ cargo kani --debug --verbose KANIFLAGS="--goto-c --log-level=debug --assertion-reach-checks -C symbol-mangling-version=v0" RUSTC="/home/ubuntu/rmc/target/debug/kani-compiler" RUSTFLAGS="--kani-flags" cargo build --target x86_64-unknown-linux-gnu --target-dir target -v error: output of --print=file-names has changed in the compiler, cannot...

Buid Kani on arm linux

3

We've got Kani building on M1, now let's get it building on arm linux. Out of scope is CI/install, just like M1.

Single use of `type_map`

3

There is exactly one use of `type_map`: https://github.com/model-checking/kani/blob/89c1269fd163f4aa38b1ae475ce2b780bd229d43/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs#L120-L124 I believe this code (the function `virtual_call_with_restricted_fn_ptr`) could have its arguments changed to take the MIR type instead of the `cprover_bindings` `Type`,...

I don't think this is release blocking, but we should do a general audit of all the assertions we generate. I believe we're very inconsistent in how we do this....

Linking the Rust standard library

2

Rust toolchains come with a pre-built shared object file for the standard library, so it seems likely that what we need to do is ship a pre-built goto-c object file...

index out of bounds exceptions don't assume(false)

1

This is apparent in the `docs/src/tutorials/loops-unwinding` example. Where we get both a bounds and a pointer failure: ``` SUMMARY: ** 2 of 350 failed Failed Checks: index out of bounds:...

Unwinding assertion failures do not clearly indicate which loop is involved

1

``` Check 67: .unwind.0 - Status: FAILURE - Description: "unwinding assertion loop 0" SUMMARY: ** 1 of 67 failed (66 undetermined) Failed Checks: unwinding assertion loop 0 ``` What function?...

Ignore `workspace.default-members` when running `cargo install` on root package of a non-virtual workspace

1

### What does this PR try to resolve? * Fixes #11058 Two observable behaviors are fixed: 1. When running `cargo install` with `--path` or `--git` and specifically requesting the root...

`cargo install --git` builds `workspace.default-members` when it should not

2

### Problem * This affects `--path` as well. * It does not affect e.g. `crates.io` because the `Cargo.toml` there have `workspace` stripped from them. When running a command like: ```...

Tutorial: proof harness patterns

1

We should document common patterns for proof harnesses, along with explanations/justifications for why they're common or interesting to know about. For example: ## No assumptions or assertions ```rust fn check_fn()...