Warning about unsupported caller_location intrinsic

[zhassan-aws]

Kani almost always emits the following annoying warning on any program:

warning: Found the following unsupported constructs:
             - caller_location (1)
         
         Verification will fail if one or more of these constructs is reachable.
         See https://model-checking.github.io/kani/rust-feature-support.html for more details.

warning: 1 warning emitted

for example, on this tiny program:

#[kani::proof]
fn main() {
    let _x: bool = kani::any();
}

using the following command line invocation:

kani test.rs

with Kani version: f4796ea

It's not clear what the source of this intrinsic is, so it might be worth investigating if this is coming from codegen itself.

[zhassan-aws]

This still occurs on programs involving panic!, e.g:

#[kani::proof]
fn main() {
    panic!("Some message");
}

$ kani simp_panic.rs 
warning: Found the following unsupported constructs:
             - caller_location (1)
         
         Verification will fail if one or more of these constructs is reachable.
         See https://model-checking.github.io/kani/rust-feature-support.html for more details.

warning: 1 warning emitted

Checking harness main...
...

Reopening.