Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] access structure field using pointer arithmeticand cast
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Wed Jul 16 23:36:53 2008
  • References: <E58AAB7E41B746CFB21E33B5CC89D504@jamo>
>    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