--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on November 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Need your help



Hello,

2012/11/30 intissar mzalouat <intissar_mzalouat at yahoo.fr>:
> I am going to verify a c code containing many functions.
> Do I have to split the code and verify each function seperately?
> Or verify the whole code?

Disclaimer: I'm a basic Frama-C user. Frama-C people will correct me.

It depends:
  * If you are using WP or Jessie (proof on code in a Hoare-like
framework), you can verify separately each function;

  * If you are using Value analysis, you'd better keep the whole code
and verify it in a whole, as Value analysis infers analysis from one
function call to the other. The main issue is to reproduce the way you
code is called. If you code include a main(), just start from it.
Otherwise you need to play make a main and code non deterministic
calls to your code.

In both cases, you need to give a precise contract on all your
analysed functions and functions called by those functions.

Frama-C blog as a lot of posts on how to do use Value analysis,
especially in old posts:

 * http://blog.frama-c.com/index.php?tag/value

 * http://blog.frama-c.com/index.php?tag/value/page/2
 * http://blog.frama-c.com/index.php?tag/value/page/4

My advices:
 * Don't forget to read the docs of WP and Value analysis, they
include tutorials!

 * Use Frama-C to compute the call graph of your code at the beginning
of your analysis, in order to better understand your code.

Regards,
david