--- layout: fc_discuss_archives title: Message 102 from Frama-C-discuss on June 2009 ---
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; }