Skip to content

Investigate why mir-linker test requires an unwind annotation #1978

Closed
@zhassan-aws

Description

@zhassan-aws

This is concerned with the mir-linker test (tests/cargo-kani/mir-linker/src/lib.rs).

Before CBMC 5.72.0, this test did not require an unwind annotation.

With CBMC 5.72.0, not specifying an unwind value causes it to unwind forever (see #1941).

Investigate why.

Metadata

Metadata

Assignees

Labels

T-CBMCIssue related to an existing CBMC issueT-High PriorityTag issues that have high priority[C] InternalTracks some internal work. I.e.: Users should not be affected.

Type

No type

Projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions