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] 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