Skip to content
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

Remember if cast is explicit or implicit #179

Open
sim642 opened this issue Mar 6, 2025 · 0 comments
Open

Remember if cast is explicit or implicit #179

sim642 opened this issue Mar 6, 2025 · 0 comments

Comments

@sim642
Copy link
Member

sim642 commented Mar 6, 2025

Currently, all casts look the same in CIL, i.e. explicit casts in the parsed program and various implicit casts inserted by CIL (depending on some configuration). This makes it impossible to know later which casts are explicit and which implicit.

It might be useful to remember this. In particular, for pretty-printing purposes: perhaps we could have a CIL expression pretty-printer which only prints the explicit ones, but not the implicit ones.
This might be a way to produce human-readable witness invariants in Goblint while keeping them internally with implicit casts for evaluation purposes. Although I'm not totally sure this would solve all the issues.

If this information is added to CastE or whatnot, then it might be a good idea to not just make it a implicit: bool but use some kind of enum to also remember the kind of implicit cast, if possible. For example, to know what's integer promotion or arithmetic conversion or whatever else.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant