--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on April 2009 ---
Hello, Le lun 20 avr 2009 11:13:27 CEST, "Christoph Weber" <Christoph.Weber at first.fraunhofer.de> a ?crit : > > requires a + length < b || b + length < a; > > > When calling this example with jessie gui, I get the message: > > File "why/swap_ranges_array.why", line 1152, characters 106-122: > Application to int_P_int_M_a_24 creates an alias > make[1]: *** [swap_ranges_array.stat] Error 1. > I'm not completely sure of what is going on (a real jessie specialist is needed here), but my guess would be that your requires clause tells the jessie plugin that arrays a and b might lie in the same allocated block (even though they do not overlap), which is not consistent with the hypothesis implicitly made for function swap, for which the two pointers must reside in two different regions. Giving the option -jessie-no-regions might help, but you might end up with proof obligations that cannot be discharged (in particular, if I remember correctly, the assigns clauses are not completely reflected yet in the corresponding why program, so that provers might not be able to infer that only a[i] and b[i] are touched in a loop step, and thus that everything they know about a[k] and b[k] for k < i is still valid. But again, this needs to be confirmed by a jessie developer). Best regards, -- Virgile Prevosto Ing?nieur-Chercheur, CEA, LIST Laboratoire de S?ret? des Logiciels +33/0 1 69 08 71 83