Cannot find macro `__kani__workaround_core_assert`

[weaversa]

I'm running cargo kani version 0.39.0 in a project that has a dependency (apparently) on theunicode-bidi package. The error I get during cargo kani compilation is:

...
Compiling unicode-bidi v0.3.13
error: cannot find macro `__kani__workaround_core_assert` in this scope
   --> .cargo/registry/src/index.crates.io/unicode-bidi-0.3.13/src/implicit.rs:494:13
    |
494 | / ...   std::debug_assert!(
495 | | ...       false,
496 | | ...       "Found broken indices in level run: found indices {}.....
497 | | ...       level_run.start,
498 | | ...       level_run.end,
499 | | ...       text.len()
500 | | ...   );
    | |_______^
    |
    = note: this error originates in the macro `$crate::assert` which comes from the expansion of the macro `std::debug_assert` (in Nightly builds, run\
 with -Z macro-backtrace for more info)

Any assistance would be appreciated.

[zhassan-aws]

Thanks for reporting the issue @weaversa. This is a duplicate of #2187. We've attempted a fix in #2194, but unfortunately, this broke other things.

Unfortunately, there is no easy fix as we need to change the mechanism by which Kani overrides std macros (tracked by https://github.com/model-checking/kani/issues/2275).

You can try editing ~/.kani/kani-0.39.0/library/std/src/lib.rs and apply the same patch that was applied in #2194. I'm not sure if doing that will work though.

[weaversa]

Thanks for reporting the issue @weaversa. This is a duplicate of #2187. We've attempted a fix in #2194, but unfortunately, this broke other things.

Unfortunately, there is no easy fix as we need to change the mechanism by which Kani overrides std macros (tracked by #2275).

You can try editing ~/.kani/kani-0.39.0/library/std/src/lib.rs and apply the same patch that was applied in #2194. I'm not sure if doing that will work though.

Thank you for looking into it. I'll track #2275. Is there some way to use your newish stubbing capability here? I gather not since the issue happens during initial compilation.

[zhassan-aws]

I gather not since the issue happens during initial compilation.

Correct: the issue happens during expansion of the debug_assert macro, so stubbing won't help.