Only intervals
Pascal Cuoq - 26th Aug 2011More 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.