GNATStudio plugin

[Jellix]

It could be handy to have a plug-in in GNATStudio so that the user can run the tool after a prove and see the information possibly interspersed with the actual source code.

Not clear yet, though, how the output should be displayed in the IDE.

[yannickmoy]

IMO the simplest integration is to have the tool display a sorted list of all checks, starting with the unproved and then the proved ones, ordered by decreasing proof time. Possibly with a cut-off at 1s to not display proofs that are faster than that. If you use the "file:line:col msg" format, the standard output parser in GNAT Studio will readily add links to the source code.

Something more involved would require plotting the proof effort. I can imagine having a 2-dimensional plot with steps/time as axes and a dot for each check, on which you can zoom and click on a given dot to bring you to the corresponding line-of-code and message. Just a product of imagination right now, as it probably requires extending Cairo binding in GNAT Studio. Not sure it's worth the effort, compared to the simple integration above.

[Jellix]

The plug-in sorts the times in a binary logarithmic manner, so there is possibly no need for using the --cut-off parameter.