In this talk, I will present the work AdaCore has been doing to add Ada support to Infer. Right now, our main deployed analysis is BufferOverrun. However, we use it in a non-standard way, which forced us to modify it significantly. I will survey those changes and their implications. Another impactful change is a deep modification of the Restart scheduler, which was struggling on the very dense call-graphs our frontend generates. This year, we also started to tackle the issue of determinism; this led us to write a new scheduler, which we are in the process of deploying. Finally, we are very interested in using Pulse. As a consequence, we rewrote our frontend to use a closures-based representation – and adapted BufferOverrun accordingly. Finally, if time permits, I will also discuss the state of the MinGW port of Infer, as well as various more minor patches that we maintain.
Program Display Configuration
Mon 13 Jun
Displayed time zone: Pacific Time (US & Canada)change