--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on November 2010 ---
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