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] 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