Skip to content

Invariant violation during goto conversion on C file with goto statements #8436

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
andreast271 opened this issue Sep 3, 2024 · 1 comment · Fixed by #8438
Closed

Invariant violation during goto conversion on C file with goto statements #8436

andreast271 opened this issue Sep 3, 2024 · 1 comment · Fixed by #8438
Labels
pending merge

Comments

@andreast271
Copy link
Contributor

label.c.txt

With the attached C file label.c, CBMC will fail during goto conversion with an invariant violation.
Specifically:

$ cbmc label.c 
CBMC version 6.2.0 (cbmc-6.2.0-dirty) 64-bit x86_64 linux
Type-checking label
Generating GOTO Program
--- begin invariant violation report ---
Invariant check failed
File: goto-conversion/goto_convert.cpp:351 function: finish_gotos
Condition: false
Reason: Unreachable

The file looks rather nonsensical. It started as an auto-generated C file (via Csmith). As far as I can tell it contains legal C and should not cause a crash.

CBMC version: 6.2.0
Operating system: Liunx x86_64
Exact command line resulting in the issue: cbmc label.c
What behaviour did you expect: cbmc to not crash
What happened instead: invariant violation
tautschnig added a commit to tautschnig/cbmc that referenced this issue Sep 3, 2024
@tautschnig
Fix Alpine's assert-statement conversion special case
26f030b 
In d44bfd3 we added a special case to catch Alpine Linux' assert
structure. The match, however, was not sufficiently specific as it just
accepted any statement that follows the actual assertion.

Fixes: diffblue#8436
@tautschnig tautschnig mentioned this issue Sep 3, 2024
Merged
3 tasks
@tautschnig
Copy link
Collaborator

Thank you, we seem to have carried this bug since 2017. Fix in #8438.

tautschnig added a commit to tautschnig/cbmc that referenced this issue Sep 5, 2024
@tautschnig
Fix Alpine's assert-statement conversion special case
4b5fae8 
In d44bfd3 we added a special case to catch Alpine Linux' assert
structure. The match, however, was not sufficiently specific as it just
accepted any statement that follows the actual assertion.

Fixes: diffblue#8436
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
pending merge
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix Alpine's assert-statement conversion special case tautschnig/cbmc
2 participants
@tautschnig @andreast271