# 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

*Subject*: [Frama-c-discuss] Value Analysis - assertion, slevel and sqrt function*From*: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)*Date*: Sat, 24 Nov 2012 15:03:43 -0200*In-reply-to*: <0E8EF4DA-3348-42B7-90D4-6C8B1549E319@gmail.com>*References*: <CAEtoXR1Xd9Ro+yKst64fonL__XYsuK2FWUq59W43EW+GCrn0ig@mail.gmail.com> <0E8EF4DA-3348-42B7-90D4-6C8B1549E319@gmail.com>

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>

**References**:**[Frama-c-discuss] Value Analysis - assertion, slevel and sqrt function***From:*rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)

**[Frama-c-discuss] Value Analysis - assertion, slevel and sqrt function***From:*pascal.cuoq at gmail.com (Pascal Cuoq)

- Prev by Date:
**[Frama-c-discuss] Value Analysis - assertion, slevel and sqrt function** - Next by Date:
**[Frama-c-discuss] using mathematical modulo in acsl specification** - Previous by thread:
**[Frama-c-discuss] Value Analysis - assertion, slevel and sqrt function** - Next by thread:
**[Frama-c-discuss] using mathematical modulo in acsl specification** - Index(es):