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