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

[Frama-c-discuss] rte: valid



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>