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] 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