Skip to content

Autoharness generates harnesses for tuple struct constructors #4189

@carolynzech

Description

@carolynzech

Apparently for tuple structs, Rust will insert a constructor function in MIR, e.g.

struct TupleStruct(u32);

generates:

fn TupleStruct(_1: u32) -> TupleStruct {
    let mut _0: TupleStruct;

    bb0: {
        _0 = TupleStruct(move _1);
        return;
    }
}

(see playground).

This means that in autoharness, we find and verify this function:

Autoharness Summary:
+-------------------+---------------------------+---------------------+
| Selected Function | Kind of Automatic Harness | Verification Result |
+=====================================================================+
| TupleStruct       | #[kani::proof]            | Success             |
+-------------------+---------------------------+---------------------+
Complete - 1 successfully verified functions, 0 failures, 1 total.

The correct behavior would be to skip over these constructors entirely, since they are inserted by the Rust compiler.

Metadata

Metadata

Assignees

Labels

Z-AutoharnessIssue related to autoharness subcommand[C] BugThis is a bug. Something isn't working.

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions