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] Jessie proof obligation not discharged?

  • Subject: [Frama-c-discuss] Jessie proof obligation not discharged?
  • From: MarkoSchuetz at web.de (Marko Schütz Schmuck)
  • Date: Wed, 22 Aug 2012 17:12:05 -0400
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>