Skip to content

Running assess from a clean cargo workspace fails with irep not terminated issue #1797

@celinval

Description

@celinval

I tried the code from this workspace: https://github.com/model-checking/kani/tree/main/tests/cargo-ui/ws-integ-tests

using the following command line invocation:

cargo clean
cargo kani --legacy-linker assess

with Kani version: 0.13

I expected to see this happen: It works.

Instead, this happened: cargo-kani assess failed due to `irep not terminated` error.
cargo kani --legacy-linker assess
   Compiling integ_harness v0.1.0 (/tmp/kani/tests/cargo-ui/ws-integ-tests/integ_harness)
   Compiling in_src_harness v0.1.0 (/tmp/kani/tests/cargo-ui/ws-integ-tests/in_src_harness)
   Compiling all_harness v0.1.0 (/tmp/kani/tests/cargo-ui/ws-integ-tests/all_harness)
    Finished test [unoptimized + debuginfo] target(s) in 0.39s
   Compiling all_harness v0.1.0 (/tmp/kani/tests/cargo-ui/ws-integ-tests/all_harness)
    Finished test [unoptimized + debuginfo] target(s) in 0.20s
   Compiling in_src_harness v0.1.0 (/tmp/kani/tests/cargo-ui/ws-integ-tests/in_src_harness)
    Finished test [unoptimized + debuginfo] target(s) in 0.21s
   Compiling in_src_harness v0.1.0 (/tmp/kani/tests/cargo-ui/ws-integ-tests/in_src_harness)
    Finished test [unoptimized + debuginfo] target(s) in 0.58s
   Compiling integ_harness v0.1.0 (/tmp/kani/tests/cargo-ui/ws-integ-tests/integ_harness)
    Finished test [unoptimized + debuginfo] target(s) in 0.12s
   Compiling integ_harness v0.1.0 (/tmp/kani/tests/cargo-ui/ws-integ-tests/integ_harness)
    Finished test [unoptimized + debuginfo] target(s) in 0.64s
Analyzed 9 crates
No crates contained Rust features unsupported by Kani
Reading GOTO program from '/tmp/kani/tests/cargo-ui/ws-integ-tests/target/x86_64-unknown-linux-gnu/debug/deps/cbmc-linked.for-test_no_overflow-{closure#0}.out'
irep not terminated
Reading GOTO program from '/tmp/kani/tests/cargo-ui/ws-integ-tests/target/x86_64-unknown-linux-gnu/debug/deps/cbmc-linked.for-test_no_overflow-{closure#0}.out'
irep not terminated
Error: goto-instrument exited with status exit status: 6

This looks a lot like some synchronization issue. Re-running cargo --legacy-linker assess works without any problem.

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] BugThis is a bug. Something isn't working.

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions