--- layout: fc_discuss_archives title: Message 3 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 arithmetic and cast



Hi,

>    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. >From the Caduceus
> paper, it seems to be not supported.

Regarding Caduceus and Frama-C/Jessie, pointer arithmetic is supported
but pointer casts are not (casts between primitive types such as int,
long, float, etc. are supported, though).

-- 
Jean-Christophe Filli?tre
http://www.lri.fr/~filliatr/