Skip to content

Running --visualize still includes unnecessary CBMC checks in coverage run #368

@vecchiot-aws

Description

@vecchiot-aws

With working directory as src/test/cbmc/LoopLoop_NonReturning:

The following works fine:
rmc main.rs --cbmc-args --unwind 10

The following does not terminate:
rmc --visualize main.rs --cbmc-args --unwind 10

When I manually set cover_args to ["--unwind", "10"], it terminates successfully.

Possible solution: add --unwind as an RMC flag, and if present, add it to cover_args as well.

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] Feature / EnhancementA new feature request or enhancement to an existing feature.[E] PerformanceTrack performance improvement (Time / Memory / CPU)

    Type

    No type

    Projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions