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

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