--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on May 2012 ---
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