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

Hi,

Indeed, I guess there is a problem within cpulimit-win.c that one can get around.
But not sure it fully explains iconization differences you mentioned. 

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 ...?).

Maybe our Why's specialists could kindly change dpConfig.ml in that way if it is still compliant with other OS?

HTH a bit,
Dillon
 

> -----Message d'origine-----
> De : frama-c-discuss-bounces at lists.gforge.inria.fr 
> [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la 
> part de Kerstin Hartig
> Envoy? : mardi 30 juin 2009 11:35
> ? : frama-c-discuss at lists.gforge.inria.fr
> Objet : [Frama-c-discuss] Result icons in Jessie-GUI
> 
> Hello,
> 
> First I wanna send some congrats for the new Release. But I 
> still have a question corresponding to the Lithium Release though.
> 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.
> 
> Thanks a lot,
> 
> Kerstin Hartig
>  
> 
> ---------------------
> /*@
>  requires 0 <= length;
>  requires \valid_range(a, 0, length-1);  assigns \nothing;  
> ensures 0 <= \result <= length;  ensures \forall integer k; 0 
> <= k < \result ==>  a[k] != value;  ensures \result < length 
> ==>  a[\result] == value;  */ int find_array (int* a, int 
> length, int value) {
>     int i = 0;
>     /*@
>       loop invariant 0 <= i <= length;
>       loop invariant \forall integer k; 0 <= k < i ==>  a[k] != value;
>     */
>     while (i != length && !(a[i] == value))
>         ++i;
>     return i;
> }