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] Problem with Why and Pointers

  • Subject: [Frama-c-discuss] Problem with Why and Pointers
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
  • Date: Mon, 20 Apr 2009 14:21:11 +0200
  • In-reply-to: <6B6DFDD8383348B7A88B1AA0DF84FE75@AHARDPLACE>
  • References: <6B6DFDD8383348B7A88B1AA0DF84FE75@AHARDPLACE>
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