--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on March 2011 ---
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>