--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on February 2011 ---
Hello, All these different points of view are very interesting, and sometimes far from what we do "in-house" with Frama-C. So I hope this short message will also contribute to enlarge any newcomer's vision of the possible usages of the platform. In our industrial experiments, we use different Frama-C plug-ins, mainly Value Analysis and WP (1). Both have their own advantages and drawbacks. Either due to their underlying methods, or their implementations. It's true that Abstract Interpretation with Value Analysis (or certainly other tools of the same kind!) may lead to non-conclusive over-approximations wrt to the sought properties, or may be sometimes too much time-consuming. It's also true that Proof of Program needs a lot of annotations to obtain sometimes apparently "straightforward" proofs of properties. Fortunately, for *our* purpose (I do insist to avoid any misleading generality: for our classes of C codes and properties addressed in our use cases), these good and bad "points" do compensate one each other ... of course, only if the two approaches (Value Analysis and WP) are used jointly. Briefly, Value Analysis, as a context-sensitive analyzer, is from our point of view very well adapted to deal with a whole application analysis. When some analyzed C functions lead to too much time-consuming during their analysis, or if Value Analysis yields a non-conclusive over-approximation of these functions' outputs, then it is time to use a weakest-precondition approach (with WP or Jessie plug-ins). ACSL annotations will alleviate Value Analysis charge and improve its precision, and later on, will be discharged by WP (or Jessie). These two approaches are, on the basis of our lessons learnt on real industrial codes (on large parts generated from synchronous data-flow models (2)), definitely complementary. Value Analysis is a powerful tool, able to obtain "sufficiently" accurate results in a small amount of time (analysis on our codes are between 15 minutes and 1 hour). Annotations needed to help Value Analysis in obtaining this "sufficient" accuracy, are not so numerous (in comparison with the workload that would be necessary to do the whole job only by means of a deductive approach). As most of these annotations are asserts or quite simple statement contracts, i.e. "close" to the instructions that will be used to build the related proof-obligations, they can be discharged ... "almost" easily! Regards, D. (1) We also used Jessie in previous experiences. (2) A link in Frama-C publications page will point to our FoVeOOS'10 paper for more details.