Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value Analysis - assertion, slevel and sqrt function

> It has worked with the minimum value equal 32:
> >> frama-c -val sqrt.c /usr/share/frama-c/builtin.c /usr/share/frama-c/math.c -slevel 32

Your annotations, with their 6 disjunctions, define 2^6 (64) cases. 64 is therefore the minimal value of -slevel that will certainly make the analysis work. If you use less, it may work or not depending on the propagation order (which is inscrutable). It may work and then cease to work because of the slightest change in the program, such as one additional, unrelated statement. Conclusion: for this example, use 64 (or more). 

> 2- the program called the function Frama_C_show_each to verify the value of the variables, but we have observed that the function is called several times. Why does it occur?

Before the first assertion, there is one abstract state being propagated. The first assertion splits it in two. The second assertion splits each of these in two (there are now 4 abstract states). And so on until there are 64 at the end of the function, where they are finally gathered.

Frama_C_show_each_aa(aux); prints the value of aux in each of the 8 (if I count correctly) states already separated at that point. The values for aux is the same in some of these 8 states, so you may see several times the same line.

If you want to see the propagation process more clearly, replace one or several  Frama_C_show_each_? with Frama_C_dump_each(); 
This will allow you to see the complete states, and it will be clear why they are different although they have the same values for aux.