What is the difference between Frama-C and Caduceus?
Frama-C is a platform that allows many techniques to be applied to analyse a C program. We are increasingly combining analyses (plugins), so that in the end you should be able to prove many properties by abstract interpretation, slice the program for the remaining properties and prove them by deductive verification inside Why, all automatically. Frama-C aims at supporting all of C, which it does already, while plugins have their own limitations. The Jessie plugin is the one that translates C programs into an intermediate language inside the Why platform, so that Frama-C can be used to perform deductive verification in the same way as Caduceus. We just started to support casts and unions for experiments, but we have not released this part yet. It should be the case ultimately that constructs not supported in Caduceus are supported in this Jessie plugin.
