-
Notifications
You must be signed in to change notification settings - Fork 273
goto-cc crashes on softfloat code using __int128 #5103
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.
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
Labels
Comments
This is caused by the implicit promotion of the boolean |
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Jan 17, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
3 tasks
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Jan 18, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Jan 19, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Jan 19, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Jan 19, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Jan 24, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Jan 28, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Jan 29, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 1, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 2, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 3, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 3, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 11, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 15, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Mar 3, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Mar 30, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
May 7, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
May 14, 2021
We use Booleans instead of int as type of binary predicates. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 9, 2022
We use Booleans instead of int as type of binary predicates, and enums don't convert to bitvector types directly either. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 9, 2022
We use Booleans instead of int as type of binary predicates, and enums don't convert to bitvector types directly either. This must not preclude mixing binary predicates with bitvector-typed expressions. Fixes: diffblue#5103
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
CBMC version: gcc (goto-cc 5.12 (crest.merged-48-gabe78fc77-dirty)) 7.4.0
Operating system: 4.15.0-45-generic x86_64 GNU/Linux
Exact command line resulting in the issue: goto-cc sf.c
What behaviour did you expect: no crash
What happened instead: invariant failure
The following is a reduced version of the softfloat code causing the crash:
file sf.c:
command:
goto-cc sf.c
output:
The text was updated successfully, but these errors were encountered: