By pascal on Saturday, August 27 2011, 01:53 - Permalink
More often than is good for me, I find someone on the internet saying something to the effect that "Frama-C only does intervals". Sadly, I think I see what they mean.
- they may be of the school of thought that static analysis is abstract interpretation, so that although Frama-C is a static analysis framework with a large range of useful tricks it can do, they identify it with the one plug-in that does mostly abstract interpretation and nothing more than abstract interpretation. That much is ordinary: for every person who knows about it at all, there is a single plug-in that they think Frama-C is.
- For those making the "intervals" remark, programs are structurally simple sequences of computations involving simple variables, so that a non-relational analysis is naturally an interval analysis. What other kind of interesting information could a non-relational analysis compute ? It's not as if programs exhibited uninitialized variables, dangling pointers, pointer arithmetics, and dirty pointer manipulation tricks.
- And they are not interested in data flow properties either, so that they completely miss Frama-C's various plug-ins for computing data flow properties with abstract interpretation and dedicated abstract domains.
It's all fine, of course. May everyone find joy doing what they like most. I just wish Frama-C was dragged less often into these people's discussion. They don't need to hear about it, because they don't have a C program to verify, and it ruins my own fun when Google Alerts digs up this kind of comment. But I don't host a cat, and it must be a law of nature that everyone should find something foul on their doorstep once in a while.