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