--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on May 2014 ---
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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140523/09af2297/attachment.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: valid.c Type: text/x-csrc Size: 299 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140523/09af2297/attachment.c>