--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on March 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie: Timeout for Simplify broken?



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>