The current implementation of modeling a loop is quite simple in the Clang Static Analyzer. This simple approach results a loss of coverage, which indicates false negatives. There is already an implemented loop widening method in the Clang Static Analyzer.[1] However, it comes at the price that (almost) all of the MemRegions values will be invalidated. Hence, the false positive rate is relatively high in these paths. That is the reason it is not turned on by default but hidden behind a flag. My project would aim to improve the simulation of the loops in general. Moreover, it would provide an extensible and incremental way of loop widening in which only the relevant regions are invalidated, and thus can be turned on by default.



Péter Szécsi


  • Anna Zaks
  • Devin Coughlin
  • Artem Dergachev