Skip to content

RMC unwinding-assertions should be on by default #156

Closed
#263
Closed
RMC unwinding-assertions should be on by default#156
#263
Assignees
adpaco
Labels
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.[F] SoundnessKani failed to detect an issue

Description

@nchong-at-aws
nchong-at-aws
opened on May 27, 2021

RMC should use --unwinding-assertions by default and have an option to disable the checks. The tool should suggest increasing loop bounds or disabling unwinding assertions if these assertions fail.

Activity

  1. adpaco
    added
    Area: verification
    [C] Feature / EnhancementA new feature request or enhancement to an existing feature.
    [F] SoundnessKani failed to detect an issue
    on May 31, 2021

  2. adpaco commented on May 31, 2021

    @adpaco
    adpaco
    on May 31, 2021
    Contributor

    @danielsn suggested having a few flags on by default (--unwinding-assertions being one of them), and provide a new flag (e.g., --no-safe-options) to disable them manually.

  3. danielsn
    assigned
    adpaco
    on Jun 22, 2021
  4. adpaco
    closed this as completedin #263on Jul 13, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.[F] SoundnessKani failed to detect an issue

Type

No type

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions