Is pointer arithmetic supported? Are pointer casts supported?
First, answer to this question depends on what one means 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. The value analysis allows heterogeneous pointer casts, such as casts from pointer to structure to pointer to basic type, and arbitrary pointer arithmetic. Jessie supports pointer arithmetic, casts between primitive types such as int, long, float, etc., but not pointer casts.
