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: Timeout for Simplify broken?

  • Subject: [Frama-c-discuss] Jessie: Timeout for Simplify broken?
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
  • Date: Wed, 2 Mar 2011 18:54:49 +0100
  • References: <1299076237.31590.27.camel@iti27>
Hello Boris,

we haven't used why-2.29 yet but we know already for some time
that simplify has a problem with reporting overflow warning when the
only thing that is going on is a an initialization from int to int.
I found that sometimes instead of writing

  int a = b; // b is of type int as well

it helps to write

  int a = 0;
  a = b;

but it's hardly a beautiful solution.

I am not sure but we might have reported this to the current maintainers of
simplify last summer,
but no new version has been released since then. 

Jens


-----Original Message-----
From: frama-c-discuss-bounces at lists.gforge.inria.fr on behalf of Boris
Hollas
Sent: Wed 02.03.2011 15:30
To: Frama-C public discussion
Subject: [Frama-c-discuss] Jessie: Timeout for Simplify broken?
 
Hello,

I have the prover timeout set to 60s in gWhy. Still, Simplify 1.5.4.
spends only a few seconds on each VC and fails to prove some arithmetic
overflow VCs that can be proved with alt-ergo. Is there something wrong
with the timeout? I use why-2.29.
-- 
Regards,
Boris


_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/ms-tnef
Size: 3395 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110302/ac9f0bd5/attachment.bin>