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