--- layout: fc_discuss_archives title: Message 118 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



Hi Patrick

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?

Damien

Damien

BAUDIN Patrick wrote:
> Hello,
> Just from an ACSL point of view, the proof of the "assigns"
> and "ensures" clauses of your spec requires locations "p"
> and "*p" to be \separated.
> Patrick Baudin.
>