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] Jessie + simplify broken?

  • Subject: [Frama-c-discuss] Jessie + simplify broken?
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Tue, 12 Oct 2010 07:23:51 +0200
  • In-reply-to: <4CB32B19.4080800@inria.fr>
  • References: <2130910004.130939.1286806628226.JavaMail.root@zmbs1.inria.fr> <4CB32B19.4080800@inria.fr>
On Mon, 2010-10-11 at 17:19 +0200, Claude Marche wrote:

> When the "tools" icon shows up for a prover, please select Proof/Debug 
> mode in the menu
> and replay the same proof by double-clicking on it. Debug info should 
> print on the standard error, so that you can figure out what is the problem.

That's what i get:

oblig : get2_safety_po_1
calling Simplify on /tmp/gwhyb915b2_why.sx
command line: simplify   /tmp/gwhyb915b2_why.sx
Calldp : Command output : why-cpulimit: simplify:command not found
Debug: not removing temporary file '/tmp/gwhyb915b2_why.sx'


CVC3 works. There's even a package for Ubuntu.

> Apart from that, I confirm that the time limit setting of Gwhy should be 
> stored permanently between sessions, so you have a specific problem with 

I can reproduce the following:
- if I quit gwhy with Ctrl-Q, the timeout is stored
- if I quit gwhy by clicking on the close-gadget in the window, the
timeout is not stored

-- 
Regards,
Boris