Are access structure field using pointer arithmetic and cast supported in 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). Note that 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 heterogeneous pointer casts, such as casts from pointer to structure to pointer to basic type, and arbitrary pointer arithmetic.