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] Application to list_head_prev_0_new_0_4 creates an alias

  • Subject: [Frama-c-discuss] Application to list_head_prev_0_new_0_4 creates an alias
  • From: khoroshilov at ispras.ru (Alexey Khoroshilov)
  • Date: Fri, 26 Nov 2010 18:11:24 +0300
  • In-reply-to: <AANLkTinjCxX0VgLdLJDPRbTXc4os3F8+4=Pxg1Tg8OAy@mail.gmail.com>
  • References: <4CEFC2CE.5000709@ispras.ru> <AANLkTinjCxX0VgLdLJDPRbTXc4os3F8+4=Pxg1Tg8OAy@mail.gmail.com>
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