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] lots of unproved goals for simple example

On 07/11/2013 18:49, John Regehr wrote:

> I am simply trying to verify the insertion sort code from here:
>
>    http://proval.lri.fr/gallery/InsertionSortACSL.en.html
>
> Using Frama-C Nitrogen-20111001 from an Ubuntu package, all goals can be
> proved.  However, I am left with many unproved goals using these tools:
>
>    frama-c-Fluorine-20130601
>    why-2.33
>    why3-0.81
>
> Specifically, CVC4 1.1, Z3 4.3.1, and Yices 1.0.39 are all timing out
> for most (but not all) goals.  I've put a screenshot here if that is
> helpful:
>
>    http://www.cs.utah.edu/~regehr/frama-c.png

I have tried it and it works fine for me. (Except for one proof 
obligation not proved by Z3, but proved by CVC4 and Alt-Ergo.)

In fact, your screenshot does not even make sense to me. Your obligation 
for invariant decrease is "0 <= 0 /\ 0 < 0" (obviously impossible to 
prove), while mine is "0 <= (n_1 - i1) /\ (n_1 - i2) < (n_1 - i1)" 
(trivially true). So something must have gone horribly wrong. No idea 
what it is, though.

Or maybe I do, assuming you did not make any mistake when copy-pasting 
the example of your other email. Indeed, that other example is not 
syntactically correct (missing semi-colon in the specification), so my 
guess is that the specification did not make it through the toolchain, 
otherwise you would have gotten an error message. Did you forget to pass 
the "-C" option to the preprocessor?

Best regards,

Guillaume