-
Notifications
You must be signed in to change notification settings - Fork 24
Description
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.