macOS Monterey version 12.4: Test Cases failing with goto-cc type 'checking main failed'

[YoshikiTakashima]

I tried this code:

• cargo-kani/cbmc-unknown-lang-mode/test.expected
• cargo-kani/dependencies/check_dummy.expected

using the following command line invocation:

 ./scripts/kani-regression.sh

with Kani version: 0.6.0. Laptop: macOS Monterey version 12.4. This did not happen until I upgraded OS.

I expected this to succeed.

Instead, this happened: the script failed.

failures: [cargo-kani] cargo-kani/cbmc-unknown-lang-mode/test.expected [cargo-kani] cargo-kani/dependencies/check_dummy.expected

From goto-cc failing to type check the proof harness.

[sanjit-bhat]

I had this issue as well. I'm on macOS 12.4. Here's a snippet of the output error.

/Users/sanjitbh/.cargo/registry/src/github.com-1ecc6299db9ec823/ppv-lite86-0.2.16/src/generic.rs: In function 'guts::init_chacha':
/Users/sanjitbh/.cargo/registry/src/github.com-1ecc6299db9ec823/ppv-lite86-0.2.16/src/generic.rs:800:30: error: error: conflicting function declarations 'rand_chacha::guts::init_chacha'
old definition in module '' file /Users/sanjitbh/.cargo/registry/src/github.com-1ecc6299db9ec823/ppv-lite86-0.2.16/src/generic.rs line 800 column 30 function rand_chacha::guts::init_chacha
struct _16648511774447233669 (struct [_13358953601680865708; 32] *key, struct _17530144020178589568 nonce)
new definition in module '' file /Users/sanjitbh/.cargo/registry/src/github.com-1ecc6299db9ec823/ppv-lite86-0.2.16/src/generic.rs line 800 column 30 function guts::init_chacha
struct _16648511774447233669 (struct [_13358953601680865708; 32] *key, struct _17530144020178589568 nonce)
         $($pub$(($krate))*)* fn $name($($arg: $argty),*) -> $ret {
typechecking main failed
Error: goto-cc exited with status exit status: 1

[adpaco-aws]

I cannot reproduce this in my laptop (running macOS 12.4). Maybe because you're running on Apple silicon?

[YoshikiTakashima]

@adpaco-aws Yes, I am on Apple silicon.

[adpaco-aws]

Doesn't reproduce with a macOS 12 regression neither, see this run.

This error could be related to how we handle dependencies in Apple silicon, so I would like to loop in @tedinski here.

[adpaco-aws]

Reminder: As a workaround, you can define the environment variable KANI_REGRESSION_KEEP_GOING when launching the regression script.