Re: GNATProve - interactions between units

[Martin <martin@thedowies.com>]

On Friday, October 23, 2015 at 11:25:21 AM UTC+1, Maciej Sobczak wrote:
> Hi,
> 
> My understanding of SPARK rules is that it is possible to reason about the correctness of the program by proving its units individually and the role of package specifications and subprogram contracts is to isolate units from each other in the sense that it is not necessary to look into other units in order to declare the correctness of the unit being analyzed.
> 
> In other words, we can run GNATProve on each unit separately.
> 
> On the other hand, running GNATProve on all program units allows the tool (apart from reusing the runtime infrastructure of the prover, which amortizes the startup time over many units) to get more information about how units use each other and from this additional information it can discharge more VCs than would be possible otherwise.
> If this is true, then running GNATProve on the whole program should produce the same or *smaller* amount of undischarged VCs.
> 
> I have a project where the opposite can be observed - that is, individual units prove clean, whereas the whole produces warning messages about range checks.
> 
> Is it acceptable to consider this to be a tool bug? Or are there any flaws in my reasoning above and in fact proving units separately is not sufficient for analyzing correctness of the program as a whole?
> 
> -- 
> Maciej Sobczak * http://www.inspirel.com

It may be down to the size of the problem space being analysed. It may have to 'loose' some of the information (i.e. make approximations) that it has room for in the unit analysis. Are there any 'depth of analysis' settings? It may be that you need to crank it up to 11 to ensure a "lossless" analysis and be prepared to wait for potentially very much longer to get results.

This is just a guess (I haven't used GNATProve), but it's a guess based on using other static (semantic) analysis tools for about 15 years now. ;-)

-- Martin