--- layout: fc_discuss_archives title: Message 120 from Frama-C-discuss on December 2009 ---
Damien, I won't state about \separated keyword which is experimental, but locations are clearly defined into ACL 1.4. > Thank you for the reply but I am not sure what you meant.p and *p are > different types and \separated takes only memory locations. Is there a > way to cast between them? > Yes, because a location is a set of l-values. All l-values can be written as follow: *((T*)(addr)). In that case, the memory location related to that l-value starts at the addresse addr, and its size in bytes is sizeof(*((T*)(addr)))=sizeof(T). Mainly, tools which do not support cast in C code don't support cast into specifications too (it is the same kind of difficulty). I guess the \separated key word will be introduced into ACSL in order to express a contraint on pointers without using pointer comparisons nor casts: - it gives more readable specification - tools may take benefits of it Patrick.