--- layout: fc_discuss_archives title: Message 118 from Frama-C-discuss on December 2009 ---
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. >