--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on February 2011 ---
Hello St?phane, 2011/2/1 DUPRAT Stephane <STEPHANE.DUPRAT at atosorigin.com>: > If it helps, here's my point of view about these remarks, which are from the side of an industrial user. It helps! Thanks a lot. > An other strategy for industrial (or not) developpers is to apply value analysis on sub-components of the program during its development. How do you proceed in practice to do such analysis? Are you writing a stub that generates required values with the Frama_C_* functions and then call the top functions of the analysed sub-component (as in Skein tutorial for example)? Are you using -lib-entry -main options? A combination of both? [...] > About the remark about the size of annotation: > Deductive proof is made for functional verification that are traditionnaly made by tests. > And we have to know that tests are larger thant source code. And formal specification are smaller thant tests scripts. Interesting point of view. I'll reused it. ;-) >> Overall, I already asked for it but having some examples (or >> better an article that could be cited!) detailing how Frama-C >> is applied on some industrial code (size of code, most >> important issues and approaches used to work around them, >> results obtained) would be very useful. > > I will try to export more concrete exemple. I'm looking forward to see them. And I would also be interested in experience report on people integrating Frama-C analyses in their development cycle, e.g. regular call of Frama-C in batch mode on a source version control checkout. Thanks a lot for the information, Best regards, david