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

  • Subject: [Frama-c-discuss] Result icons in Jessie-GUI
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
  • Date: Tue, 30 Jun 2009 11:34:42 +0200
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;
}