--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on August 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie proof obligation not discharged?



Dear All,

I have the C code in stringExtra.c

#include <stddef.h>
#include "stringExtra.h"
/*@
  @ predicate AbsentTail{L1,L2}(int e1, int e2, char c, char *array) =
  @    \forall int i;
  @       e2+1 <= i && i <= e1
  @         ==> \at(array[i],L1) != c;
  @*/

/*@ requires endi >= 0 && \valid_range(array, 0, endi);
  @ assigns \nothing;
  @ behavior absent:
  @   assumes \forall int i; 0 <= i <= endi ==> array[i] != c;
  @   ensures \result == -1;
  @ behavior present:
  @   assumes \exists int i; 0 <= i <= endi ==> array[i] == c;
  @   ensures 0 <= \result <= \at(endi, Pre);
  @*/
int strprevchr(int endi, char c, const char array[]) {
  /*@
    @ loop invariant \at(endi,Pre) >= endi >= -1 && AbsentTail{Pre,Here}(\at(endi,Pre), \at(endi,Here), c, array);
    @ loop variant endi;
    @*/
  while (endi >= 0 && array[endi] != c)
    endi--;
  return endi;
}

and in GWhy (using why 2) I see

strprevchr_ensures_present_po_3

endi: int32
c_0: int8
array_1: char_P pointer
char_P_array_2_alloc_table: char_P alloc_table
char_P_char_M_array_2: (char_P, int8) memory
H1: (exists i_1:int32,
     0 <= integer_of_int32(i_1) and
     integer_of_int32(i_1) <= integer_of_int32(endi) ->
     integer_of_int8(select(char_P_char_M_array_2,
                     shift(array_1, integer_of_int32(i_1)))) = integer_of_int8(c_0)) and
    (integer_of_int32(endi) >= 0 and
     offset_min(char_P_array_2_alloc_table, array_1) <= 0 and
     offset_max(char_P_array_2_alloc_table, array_1) >= integer_of_int32(endi))
mutable_endi: int32
H3: true
H4: (integer_of_int32(endi) >= integer_of_int32(mutable_endi) and
     integer_of_int32(mutable_endi) >= -1 and
     AbsentTail(endi, mutable_endi, c_0, array_1, char_P_char_M_array_2))
H14: integer_of_int32(mutable_endi) < 0
return: int32
H15: return = mutable_endi
______________

0 <= integer_of_int32(return)

and the ATPs do not discharge this PO.

H14 && H4 ==> mutable_endi == -1 and AbsentTail{..}(..) should become
\forall int i; 0 <= i && i <= endi ==> \at(array[i],L1) != c and,
together with H1, the PO should be discharged.

Am I misunderstanding/not seeing something here?

Thanks in advance and best regards,

Marko
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120822/d24b4f36/attachment.pgp>