--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on February 2011 ---
Hello Benjamin, 2011/2/1 MONATE Benjamin 205998 <Benjamin.MONATE at cea.fr>: > Thanks a lot for making your slides available: they provide a nice and precise overview of two plugins of Frama-C. Thanks. > What kind of remarks/questions did you get? Regarding Value analysis (also presented in another lesson): mostly questions regarding lack of precision on values, especially regarding loops (and "all programs are loops", quoting a participant). I talked about the skein analysis in Value analysis tutorial which is able to provide some interesting result and the use of -slevel. But I lack first hand practice on applying value analysis to large code. Is it a real issue on control code, for example? Regarding Jessie: "annotations have the same size as code!" and "what about error in annotations?". For the former remark, I could only tell that this was the price to pay to be able to *prove* code in all its generality. Regarding the latter remark, I told it would not be possible to prove the goals, but a was lacking convincing arguments. One of the attendee followed a lesson on code proof using a functional approach and PVS powerful tactics made by a researcher at INRIA Rennes (Thomas Genet) and told the approach was more powerful and simple. I answered that the discussion between the two approaches is still on-going. :-) 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. Sincerely yours, david