--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with Why and Pointers



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