--- layout: fc_discuss_archives title: Message 107 from Frama-C-discuss on June 2009 ---
Hello, thanx for your answer. I guess the redirection with "<" is not the problem, because even if the why-cpulimit command does not work, running for example yices -pc 0 smt < /cygdrive/c/Doc.../...../.....en/Temp/gwhy70ef43_why.smt in commandline does work and returns "unsat" which means valid . (just with old or new why-cpulimit it doesnt work and returns an error, so I guess why-cpulimit is the source of the problem) My question regarding the differing output of results in the Jessie-GUI was meant independently from the why-cpulimit-problem, because I took the results from a working Windows system, where why-cpulimit didn't cause the problems I have on my secondary Windows workstation. Here (in Windows) the non-valid PO's are not distinguished between timeout(scissors)/unknown(question mark)/failure(crossed tools) as they are in MacOS. The differing number of PO's (18 instead of 16 ) is due to the different integer models. I used "exact" which returns 16 PO's. Regards, Kerstin > AFAIK, Windows CreateProcess does not allow redirection characters (like "<") in the command-line parameter. > However, why/tools/dpConfig.ml contains "<" in command_switches component (in lines 116 and 129). > Removing these "<" and recompiling Why should solve the problem! (Yices and CVC3 do accept files as parameters, with no need for redirection under Windows). > On your code below, with the aforementioned changes, Yices discharged all the POs under Cygwin/XP (14/14 default behavior POs and 4/4 safety POs ... humm, not the same # of POs ...?). > > I've got a general question regarding the output of results in the Jessie-GUI. > > I realized some inconsistence between the output of some provers in MacOS and Windows. > > While with MacOS non-valid PO's are distinguished between timeout(scissors)/unknown(question mark)/failure(crossed tools) > > Windows usually just outputs every non-valid PO being a failure. > > For example: > > The code attached below outputs a result with yices: > > with MacOS: 13 valid + 2 timeout + 1 unknown > > with Windows : 13 valid + 3 failure > > As I saw several examples with the same inconsistent non-valid PO's I wanna ask if anyone knows why it is like that. > > Is there a reason for it or a fix or is it just normal? Its not about finding the error in the specification. > > Other provers than yices can prove this code-example. It's just an example to maybe understand why there are differences > > in the iconization of results. -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/ms-tnef Size: 4045 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090630/f27130d3/attachment.bin