--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on July 2008 ---
> I wonder whether access structure field using pointer arithmetic and cast > is supported in Frama-c/Jessie or Caduceus? I assume the memory model > of Frama-c/Jessie is the same as Caducecues. To complement Jean-Christophe's answer, it depends what you mean by "Frama-C/Jessie". Frama-C is an analysis framework where each plug-in (Jessie is one such plug-in) is free to define its own limitations on the subset of C that it handles. Frama-c itself has very few intrinsic limitations, and for instance, the value analysis that constitutes one of the many other plug-ins in Frama-C allows heterogenous pointer casts, such as casts from pointer to structure to pointer to basic type, and arbitrary pointer arithmetics. The theoretical bases for the sound collaboration of plug-ins with different limitations (for instance, different memory models) will be laid out in the future, but until this time, Frama-C can already be used to analyze programs that fit within the intersection of the subsets of C accepted by all the plug-ins used for the analysis. Pascal