--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on November 2012 ---
Hi Pascal, Thanks for your explanation. In fact, with Frama_C_dump_each() is easier to see what happens. Now, we will apply this in our case study, that is much more complex. Thanks a lot! Best regards, Rovedy/Nanci/Luciana 2012/11/22 Pascal Cuoq <pascal.cuoq at gmail.com> > > > 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. > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20121124/a5ee3798/attachment.html>