analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Audit for missing type unrollings

Open sim642 opened this issue 1 year ago • 0 comments

https://github.com/goblint/analyzer/pull/1519#issuecomment-2417032186 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.

sim642 avatar Oct 16 '24 15:10 sim642