--- layout: fc_discuss_archives title: Message 41 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



Hi folks,

Thanks for helping with the preprocessor problems!  I am now running 
into a different strange issue and I hope there might again be an easy fix.

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'm running on a fast machine (Intel i7 4770) with plenty of RAM.

Of course I could back off and use the older version, but that isn't any 
fun.

Thanks,

John