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