goblint/analyzer

Audit for missing type unrollings

Opened this issue · 0 comments

#1519 (comment) highlights an issue in our codebase: we do a lot of pattern matching on Cil.typ to handle particular cases, but the type isn't unrolled beforehand with Cil.unrollType. This can cause some logic to fall back to imprecise behavior due to TNamed instead of TInt/etc, although the TNamed (or a nesting of them!) unrolls to one of the desired types.

I'm not sure how to best find all such places in the codebase, but pattern matching, etc should in most cases probably happen on unrolled types. That is, our analysis should be invariant under extracting/inlining typedefs in the program.