You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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 aimplicit: 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.The text was updated successfully, but these errors were encountered: