--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on May 2014 ---
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>