--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on July 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] access structure field using pointer arithmeticand cast



>    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