Skip to content

Re-enable support to binary crates verification #655

@celinval

Description

@celinval

We should be able to verify bin crates when the verification target is the main function. I.e., user should be able to verify the following program:

// my_main.rs
fn main() {
    // code goes here.
}

using the following command line invocation:

rmc my_main.rs

with RMC version:

I expected to see this happen: RMC verifies the main function.

Instead, this happened: RMC cannot find main function because it is not marked as public.

Metadata

Metadata

Assignees

Labels

[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