--- layout: fc_discuss_archives title: Message 107 from Frama-C-discuss on June 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Result icons in Jessie-GUI



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