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