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] Inconsistent results in batch- and GUI-mode

  • Subject: [Frama-c-discuss] Inconsistent results in batch- and GUI-mode
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
  • Date: Thu, 22 Oct 2009 13:35:50 +0200
Hello,

At the moment I am facing a problem with the batch-mode of Jessie.
We are using a script that runs Jessie with several provers on several
programs and outputs a table of results.
For that we read the output of Jessie batch-mode.
I have found out now that the results of batch- and GUI-mode are not
consistent.

For example:

frama-c -jessie -jessie-int-model exact find_array.c
results for cvc3: 16 valid + 0 timeout

frama-c -jessie-atp cvc3 -jessie -jessie-int-model exact find_array.c
results batch-mode: 15 valid + 1 timeout

It also works for other examples than this one, but results are only
differing with yices and cvc3.
Do you have an idea why the results are not consistent?
Is it maybe a bug?

Thanks in advance,

Kerstin


-----
/*@ 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;
}