search

goblint / cil

C Intermediate Language
https://goblint.github.io/cil/
Other
136 stars 20 forks source link

Fix `intKindForValue` for `IBool` #111

Closed sim642 closed 2 years ago

sim642 commented 2 years ago

Upstream fix for the second issue in https://github.com/goblint/analyzer/pull/827.

Technically the fix could even be moved up into truncateCilint, where IBool is already specially handled, but for some reason as never truncating. Since truncateCilint is transitively used all over the place, I didn't want to change it as the old logic might be there for some reason.

fitsInInt is used little enough to see that it isn't used with IBool anywhere previously, so no accidental behavior changes would occur.

michael-schwarz commented 2 years ago

Could this cause issues with non-c99 code that does not expose a bool type?

sim642 commented 2 years ago

I don't think it can in Goblint because in other cases it could also return smaller ikinds than the program variables have, e.g. char for some value involved in int-typed variables, but that doesn't happen (it would lead to a mismatching ikind error), I suppose because we eventually cast this to a type that the program actually uses.

Another reason why this shouldn't be an issue is that we just use it for def_exc range, which is essentially an interval that may be smaller than the type's range if only small values are ever stored in such variable. The ID.t tracks the ikind (coming from the program) separately from def_exc range, so the range being tighter should be fine.

The only way I see this being a problem is if intKindForValue is used explicitly to generate some CIL AST for outputting as C code, then that ends up with _Bool being used in a program that originally might've been C99. But the same happens with any other C11 feature if used in such way.