--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on November 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Documentation of \valid



Hello Claude,

I understand that C treats arrays as pointers and that Jessie behaves the same way. From a user point of view, I find it inconsistent that

typedef int arr3[3];
typedef struct arr3a {int a0; int a1; int a2};

are treated differently - by C as well as by Jessie. I don't blame Jessie here as it, as you write, behaves just the way C does. Both arr3 and arr3a are types and they describe the same semantical concept. The only difference is in syntax and implementation in C. As inconsistencies may confuse users, I see use in telling it to users. That's why I suggested to add an example to the documentation. I believe that the documentation should also be useful to users who don't have a deep knowledge about pointer and data type handling in C.

Regards,
Boris