Implement lookahead widening - Githubissues

goblint / analyzer

Static analysis framework for C

https://goblint.in.tum.de

MIT License

160 stars 72 forks source link

Implement lookahead widening #1484

Open RonaldJudin opened 1 month ago

RonaldJudin commented 1 month ago

Lookahead widening from https://link.springer.com/chapter/10.1007/11817963_41

TODO

[x] Add option.
[x] Implement threadenter.
[x] Add @sim642's tests: https://github.com/goblint/analyzer/compare/master...ronald.
[x] Merge master.
[ ] Decide what to do about AnalysisState.widening.
[ ] Fix Invalid_argument exceptions on SV-COMP no-overflow.
[ ] Fix ERROR (verify)-s on SV-COMP no-overflow.