--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on May 2012 ---
Hi Pascal, On 05/05/2012 06:53 PM, Pascal Cuoq wrote: > the option works as described: for a given program, increasing > the value of -slevel makes the analysis more precise (you said > something about 10000). You do not need to understand what > it does to use it. You need to know that a higher level usually > means more resources consumed and better precision. I disagree. Users of static analyzers need to interact with the tool in a clever way, not blindly pushing buttons here and there to make the analysis "pass" by some miracle. BTW, the Frama-C manual already explains -slevel so that a user can understand where it applies or not. > I would be delighted to know what single global option you used > to make PolySpace or Astr?e analyse your example(s), if only > to mention their respective names casually at parties. Looking at the reduced example of David, I think PolySpace could prove the absence of run-time errors, because it has a domain of linear relations between variables. For PolySpace precision options, their manual is doing a good job I think: http://www.mathworks.fr/help/toolbox/polyspace/ada_ref/brid6de.html Not to say that you know exactly what is going on at precision level 0, 1, 2 or 3, but it gives some clues. -- Yannick Moy, Senior Software Engineer, AdaCore