--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on November 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Application to list_head_prev_0_new_0_4 creates an alias



Thank you for the clarification.

Regards,
Alexey

On 11/26/2010 05:48 PM, Pascal Cuoq wrote:
> Hello,
>> Could you please clarify what does the following error message mean?
> This problem is related to the "separation analysis",
> a component of Jessie.
>> The error message disappears if someone reduces assigns clause of __list_add
>> or remove call of __list_add.
> You can also keep the assigns clauses and add the following line at the
> top of your file:
>
>   # pragma SeparationPolicy(none)
>
> This changes the hypotheses made on pointers passed to functions, and
> also has for effect to disable the separation analysis. For the kind of
> verification that you are conducting, it makes more sense: the separation
> hypotheses are not satisfied in list_add, and therefore should simply not
> be made. I *think* this is the meaning of the error message you get.
>
> For more about the difficulty of computing weakest preconditions in presence
> of aliases, which is the reason the separation exists in the first
> case (it provides
> arbitrary additional hypotheses, which are often true, and often useful):
>
> http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-January/000912.html
>
> See also "Chapter 5 Separation of Memory Regions" in:
>
> http://frama-c.com/jessie/jessie-tutorial.pdf
>
> Pascal