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; }
- Prev by Date: [Frama-c-discuss] problem with an example in acsl 1.4 doc
- Next by Date: [Frama-c-discuss] A bundle Frama-C-Beryllium-20090902 + Why-2.21 is available
- Previous by thread: [Frama-c-discuss] problem with an example in acsl 1.4 doc
- Next by thread: [Frama-c-discuss] A bundle Frama-C-Beryllium-20090902 + Why-2.21 is available
- Index(es):