--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on November 2012 ---
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