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

[Frama-c-discuss] Proof conditions with simple pointer assignment



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.