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

  • Subject: [Frama-c-discuss] lots of unproved goals for simple example
  • From: regehr at cs.utah.edu (John Regehr)
  • Date: Thu, 07 Nov 2013 10:49:37 -0700
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