--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on November 2013 ---
[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