--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on May 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] rte: valid



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>