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: alessio.bortolotti at studenti.unipr.it (ALESSIO BORTOLOTTI)
  • Date: Fri, 23 May 2014 13:37:33 +0200
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>