Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.


[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] arbitrary buffers in analysis



Hello Tim,

Le 20/08/2015 18:58, Tim Newsham a écrit :
> It doesn't seem that will work to verify all buffer
> sizes (for example, l=0xffffffffffffffff on 64-bit memory spaces).

Yes. For such big values, you might have more success with Deductive 
Verification, thus WP or Jessie plug-ins. But it is also a lot of more 
work to prove, e.g., absence of Run Time Error.

The main advantage of Frama-C is that you can combine both techniques, 
i.e. Value Analysis and WP.

Best regards,
david