Skip to content

location_invariant should not be at switch case label #1925

@sim642

Description

@sim642

As discovered by @jprotopopov-ut, Goblint can output location_invariant at a switch case label.
This is not allowed by the YAML witness format: it's not be first character of a statement.

Also, inserting an assertion there would not mean the right thing: the assertion would be the last thing in the previous case.
Internally, these probably come from internal if branching nodes from a CIL-converted switch.
Not sure if we have enough information available in Goblint to distinguish the original source of the branchings.

Metadata

Metadata

Assignees

No one assigned

    Labels

    sv-compSV-COMP (analyses, results), witnesses

    Type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions