--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on August 2012 ---
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>