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] rte: valid

  • Subject: [Frama-c-discuss] rte: valid
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
  • Date: Fri, 23 May 2014 13:48:03 +0200
  • In-reply-to: <CAAEWojU8Wr_YUdyN12D5CF8ctZsVb69Ubzw=J0e2E4AwpZbbcQ@mail.gmail.com>
  • References: <CAAEWojU8Wr_YUdyN12D5CF8ctZsVb69Ubzw=J0e2E4AwpZbbcQ@mail.gmail.com>
Hello,
Just add a clause about location assigned by the loop:
...
/*@ loop invariant i ? n;
    @ loop assigns i, *(a+(0 .. n-1)); */
   while (i < n) {
...

Kind regards,
Patrick.

Le 23/05/2014 13:37, ALESSIO BORTOLOTTI a ?crit :
> Good morning.
>
> While trying to proof properties of programs using arrays, we found a strange behavior of the theorem proover.
> The property of  \valid for the array could be proved outside of a loop, but the same identical property could not be proved inside of it.
> I am wondering what may I have done wrong.
>
> The code is attached.
> I am using Frama-C Neon on a 64-bit Ubuntu 14.04.
> I used Alt-Ergo (Native) as theorem proover, having enabled both RTE and Invariants.
> "\valid(a)" is proven to be true outside the loop, but not inside of it.
>
> While I am writing, I'd also like to ask if there was a way to get a counterexample when the proover is not able to proof a property.
>
> Kind regards,
> Alessio Bortolotti
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss


-- 
Patrick Baudin, DILS/LSL, B?t. 862,
Point Courrier n? 174
Institut CARNOT CEA LIST,
CEA Saclay Nano-INNOV,
91191 Gif-sur-Yvette cedex, France.
tel: +33 (0)1 6908 2072

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140523/366feef7/attachment.html>