Kani failure

[hansonchar]

I tried to run Kani tests as part of my git repository CI/CD workflow but ran into the following failures:

   Compiling time v0.3.16
error: `std::fmt::Arguments::<'a>::new_v1` is not yet stable as a const fn
   --> /home/ec2-user/.cargo/registry/src/github.com-1ecc6299db9ec823/time-0.3.16/src/format_description/well_known/iso8601/adt_hack.rs:148:13
    |
148 |             assert!(bytes[idx] == 0, "invalid configuration");
    |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = help: add `#![feature(const_fmt_arguments_new)]` to the crate attributes to enable
    = note: this error originates in the macro `format_args` which comes from the expansion of the macro `assert` (in Nightly builds, run with -Z macro-backtrace for more info)
error[E0015]: cannot call non-const formatting macro in constant functions
   --> /home/ec2-user/.cargo/registry/src/github.com-1ecc6299db9ec823/time-0.3.16/src/lib.rs:351:18
    |
351 |     panic!("{}", message)
    |                  ^^^^^^^
    |
    = note: calls in constant functions are limited to constant functions, tuple structs and tuple variants
    = note: this error originates in the macro `format_args` which comes from the expansion of the macro `panic` (in Nightly builds, run with -Z macro-backtrace for more info)
error: `std::fmt::Arguments::<'a>::new_v1` is not yet stable as a const fn
   --> /home/ec2-user/.cargo/registry/src/github.com-1ecc6299db9ec823/time-0.3.16/src/lib.rs:351:5
    |
351 |     panic!("{}", message)
    |     ^^^^^^^^^^^^^^^^^^^^^
    |
    = help: add `#![feature(const_fmt_arguments_new)]` to the crate attributes to enable
    = note: this error originates in the macro `format_args` which comes from the expansion of the macro `panic` (in Nightly builds, run with -Z macro-backtrace for more info)
error[E0080]: erroneous constant used
   --> /home/ec2-user/.cargo/registry/src/github.com-1ecc6299db9ec823/time-0.3.16/src/format_description/well_known/iso8601/adt_hack.rs:148:38
    |
148 |             assert!(bytes[idx] == 0, "invalid configuration");
    |                                      ^^^^^^^^^^^^^^^^^^^^^^^ referenced constant has errors
error[E0080]: erroneous constant used
   --> /home/ec2-user/.cargo/registry/src/github.com-1ecc6299db9ec823/time-0.3.16/src/format_description/well_known/iso8601/adt_hack.rs:148:13
    |
148 |             assert!(bytes[idx] == 0, "invalid configuration");
    |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ referenced constant has errors
    |
    = note: this error originates in the macro `format_args` which comes from the expansion of the macro `assert` (in Nightly builds, run with -Z macro-backtrace for more info)
error[E0080]: erroneous constant used
   --> /home/ec2-user/.cargo/registry/src/github.com-1ecc6299db9ec823/time-0.3.16/src/lib.rs:351:12
    |
351 |     panic!("{}", message)
    |            ^^^^ referenced constant has errors
Some errors have detailed explanations: E0015, E0080.
For more information about an error, try `rustc --explain E0015`.
Error: "Failed to compile crate."

Sample Github workflow setup:

name: Makefile CI

env:
  RUST_BACKTRACE: 1
  PROJECT_DIR: xks-axum

on:
  pull_request:
  push:
    branches: [ "main_al2" ]

jobs:
  kani:
    name: Kani Check for Undefined Behavior
    strategy:
      matrix:
        os: [al2]
    runs-on: ${{ matrix.os }}

    steps:
      - uses: actions/checkout@v3

      - name: Kani run
        uses: model-checking/kani-github-action@v0.13
        with:
          working-directory: ${{ env.PROJECT_DIR }}
          args: --tests

[jhpratt]

I have no idea what Kani is, but the cause of the error is clear: you're using a Rust version that is too old. The current minimum supported Rust version is 1.60.

[hansonchar]

Kani is a Rust Verifier, useful for verifying unsafe code in Rust, and can be installed via:

cargo install --locked kani-verifier
cargo-kani setup

In this case, I just tried with the latest version of Rust:

$ rustc --version
rustc 1.64.0 (a55dd71d5 2022-09-19)

git clone git@github.com:time-rs/time.git
cd time
cargo kani

And you can see some reported failure.

[jhpratt]

Panicking in const contexts has been stable since last December in Rust 1.57. As such, the only explanation is that Kani is not using the system's default rustc.