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] gWhy timeout


  • Subject: [Frama-c-discuss] gWhy timeout
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Mon, 11 Oct 2010 16:19:54 +0200
  • In-reply-to: <1286806062.2466.24.camel@iti27>
  • References: <1286806062.2466.24.camel@iti27>

> the prover timeout for gWhy doesn't work on my system. I set it to 1 s
> in the GUI, yet it still takes 10 s for alt-ergo to timeout. Is there a
> fix for that?
>
> Also, is it possible to set the timeout permanently? gWhy forgets the
> setting upon the next start.

For me (Max OS X distribution from http://frama-c.com/ with alt-ergo 0.92.1
installed by hand) the timeout setting works and is remembered across
executions of gWhy.

> BTW, have you considered using iterative deepening instead? This way,
> the user could very quickly see which VCs may not verify and start

I believe that under some (almost true) assumptions on the hardware you
are doing proofs on, this "iterative deepening" is subsumed by the parallel
execution of proofs that will be available with the next version of Why.
Simply trick Why into launching more of them than you have execution
threads, and if your system is fair/robust enough, the result will be the same,
only more efficient.

Pascal