-
Notifications
You must be signed in to change notification settings - Fork 40
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
Bug: C2Boogie translation crashes when pointers are subtracted #666
Comments
The source of error can be tracked down to a limitation in the The error can be fixed by replacing the strict check ( Is this a fix that really solves the issue, or does it introduce other problems? |
I just checked it, we have two different named-types in our translation for this example, but with the same underlying type. |
Is the relation Just because the example has two named types with the same underlying type, doesn't mean that this is the only case that can appear. Maybe an alternative solution would be to check equality of the underlying types instead. |
I think
Also I found out that the fix is the only place, where
|
The current C2Boogie translation crashes when pointers are subtracted. This issue can be reproduced with the latest version of Ultimate Automizer (0.2.4-dev-5afc37e with OpenJDK 11.0.22) using the following input:
Considering this example input, the C2Boogie translation crashes when trying to translate the subtraction of the two pointer addresses (
GPIOB - GPIOA
).The text was updated successfully, but these errors were encountered: