Zyad Hassan
Zyad Hassan
Related to https://github.com/diffblue/cbmc/issues/7014
No, this isn't fixed. I have an idea for fixing it, but I haven't had time for it.
Looks like the earlier fix in https://github.com/model-checking/kani/pull/1126 no longer works.
Same issue is reproducible with lib crates.
We can use `cargo test`'s `--lib` option to avoid running integration tests, e.g.: ``` $ git diff diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index f8624297f97..d7010adf323 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -48,6...
It is used in [s2n-quic](https://github.com/awslabs/s2n-quic/), e.g.: https://github.com/aws/s2n-quic/blob/main/quic/s2n-quic-core/tests/varint/fuzz_target.rs
Attempted to re-do the std library linking experiment using the following steps: 1. `cargo new --lib lstd` 2. Put the following in `src/lib.rs`: ```rustc #[kani::proof] fn check_format() { assert!("2021".parse::().unwrap() ==...
> To what extent is Kani controlling the code being generated here? Not much: the only thing Kani has control over is the codegen for the `mul_with_overflow` intrinsic (which is...
We should also attempt to replace Kani's implementation of the `mul_with_overflow` intrinsic with `overflow_result_exprt` that was added in https://github.com/diffblue/cbmc/pull/6903 (as you suggested in https://github.com/diffblue/cbmc/issues/6607#issuecomment-1146386176).
This sounds to me like a bug/limitation in the executable trace implementation? The underlying `u8` value is not supposed to be exposed outside `kani::any::()`.