--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on May 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds



Hello Yannick,

2012/5/7 Yannick Moy <moy at adacore.com>:
> I believe that it is clear once you understand that -slevel has only an
> effect on the number of states that are kept separate at join points. On
> your example, David, there are no join points at all, so no effect of
> -slevel.

That was my understanding. Until I fall on this issue with arrays. But
maybe I haven't looked hard enough at it. I'll try to remember that
next time.

> One thing I found quite effective at conveying how the tool works, without
> going into the details of how it is implemented, is to show/discuss the
> detailed results on small examples. I have done it for our static analyzer
> CodePeer, and this works very well in trainings.

Yes, I'm the kind of people that learn through examples.

> Here is the online version
> if you want to have a look at it:
> http://docs.adacore.com/codepeer-docs/users_guide/_build/html/codepeer_by_example.html

Thank you for the pointer. I'm adding it to my to do list. ;-)

Best regards,
david