--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on August 2015 ---
[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