Skip to content

CBMC incorrectly identify nonexistent loop #7506

Open
@celinval

Description

@celinval

CBMC version: 5.75.0
Operating system: Ubuntu 22.04
Exact command line resulting in the issue: cbmc no_loops.c --unwind 1 --unwinding-assertions
What behaviour did you expect: The assertion main.assertion.1 in the code should fail.
What happened instead: The assertion main.assertion.1 succeeds, while there's a unexpected unwinding assertion failure.

Source code:

// no_loops.c
int loop_free() {
bb0:;
    int var_3 = 1;
    goto bb1;

exit:;
    return 10;

bb1:;
    goto exit;
}

int main() {
    assert(loop_free() == 0);
    return 0;
}

Output:

** Results:
no_loops.c function loop_free
[loop_free.unwind.0] line 11 unwinding assertion loop 0: FAILURE

no_loops.c function main
[main.assertion.1] line 16 assertion return_value_loop_free == 0: SUCCESS

** 1 of 2 failed (2 iterations)
VERIFICATION FAILED

Metadata

Metadata

Assignees

Labels

More info neededawsBugs or features of importance to AWS CBMC users

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions