goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
160 stars 72 forks source link

Narrowing by fixed number of `meet`s #1494

Open sim642 opened 1 month ago

sim642 commented 1 month ago

Based on the delayed widening from #1483, we could easily implement a domain lifter for narrowing that applies meet at most a fixed number of times. This makes it possible to have a terminating narrow for domains that do not have narrowings. It is a standard technique.

Our current analysis for the polyhedral example that #1484 is fixing is even more imprecise than the old literature suggests. This is because Apron doesn't provide narrowing for polyhedra and thus we cannot make any decreasing iterations. But the standard implementation of narrowing for polyhedra is to do a fixed number of meets.