--- layout: fc_discuss_archives title: Message 102 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,

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;
}