search

goblint / analyzer

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

`DefExc`,`Enums`: More precise `of_interval` and `starting` and `ending` #1413

Closed michael-schwarz closed 2 months ago

michael-schwarz commented 2 months ago

Closes #1159

michael-schwarz commented 2 months ago

Interestingly enough, this causes a regression where the increased precision leads to a lower number of contexts, which in turn causes us to lose 5 tasks on termination.

sim642 commented 2 months ago

This is quite counter-intuitive: how do fewer contexts lead to us failing to prove termination?

michael-schwarz commented 2 months ago

Because the Context-sensitive callgraph becomes recursive: Earlier the partial(!) contexts happened to distinguish things by (happy) coincidence. This is no longer the case now.

sim642 commented 2 months ago

In that case something from #1340 should be able to distinguish the sufficient number of non-recursive cases in a less roundabout way.

michael-schwarz commented 2 months ago

Yes, either something from there or one of the ideas from #1422.