Home My Page Projects The Why platform
Summary Activity Forums Tracker Lists Tasks Docs News SCM Files

[#11630] [jessie] incorrect translation

Date:
2010-12-25 14:53
Priority:
3
State:
Open
Submitted by:
Denis Yefremov (evdenis)
Assigned to:
Nobody (None)
Hardware:
none
Product:
none
Operating System:
Linux
Component:
none
Version:
none
Severity:
none
Resolution:
none
URL:
Summary:
[jessie] incorrect translation

Detailed description
[jessie] incorrect translation

In the body of the function memory is allocated (2), _malloc (1) is used.
In the snippet (3) - the essence of the problem.

Assert {3.1} is automatically proved. These conditions certainly hold:
offset_min(unsigned_int_P_good_suffix_41_alloc_table, good_suffix) <= 0
offset_max(unsigned_int_P_good_suffix_41_alloc_table, good_suffix) >= integer_of_uint32(plen_0_0) - 1

For {3.2,3.3}:
spos0: uint32
unsigned_int_P_good_suffix_41_alloc_table0: unsigned_int_P alloc_table
H122: (0 <= integer_of_uint32(spos0) and
integer_of_uint32(spos0) < integer_of_uint32(slen_1))

offset_min(unsigned_int_P_good_suffix_41_alloc_table0, good_suffix) <= 0
offset_max(unsigned_int_P_good_suffix_41_alloc_table0, good_suffix) >= integer_of_uint32(plen_0_0) - 1

No additional conditions on unsigned_int_P_good_suffix_41_alloc_table0 are imposed.

There is no modification of good_suffix in the third fragment.
I suppose, that generated conditions are incorrect.

3.1:
boyermoore_ensures_default_po_41
boyermoore_ensures_default_po_42
3.2:
boyermoore_ensures_default_po_45
boyermoore_ensures_default_po_46
3.3:
boyermoore_ensures_default_po_67
boyermoore_ensures_default_po_68

(1)
/*@
@ ensures \valid_range( \result, 0, size - 1 );
@ ensures \forall integer i; ( 0 <= i < size ) ==> ( \result[i] == 0 );
@*/
static size_t *
_malloc( const size_t size )
{
size_t *res = ( size_t * ) malloc( size * sizeof( size_t ) );

/*@ loop invariant 0 <= i <= size;
@ loop invariant \forall integer j; ( 0 <= j < i ) ==> ( res[j] == 0 );
@ loop variant size - i;
@*/
for( size_t i = 0; i < size; ++i ) res[i] = 0;

return res;
}

(2)
size_t *good_suffix = _malloc( plen );

(3)
// {3.1} This assert is automatically proved with alt-ergo
//@ assert \valid_range( good_suffix, 0, plen - 1 );

/*@
@ loop invariant 0 <= spos < slen;
@ loop variant slen - spos;
@*/
for ( unsigned long spos = 0; spos <= slen - plen; )
{
size_t ppos = plen - 1;

//@ ghost size_t ptmp = ppos;

// {3.2} It is impossible to prove this assert.
//@ assert \valid_range( good_suffix, 0, plen - 1 );

/*@
@ loop invariant 0 <= ppos <= ptmp;
@ loop invariant \forall integer i; ( ppos < i <= ptmp ) ==> ( pattern[i] == string[spos + i] );
@ loop variant ppos;
@*/
while ( ( pattern[ppos] == string[ppos + spos] ) && ( ppos > 0 ) ) --ppos;

if ( ppos == 0 ) {
_free( good_suffix );
return string + spos;
}

//@ assert pattern[ppos] != string[ppos + spos];
//@ assert ppos > 0;

//@ ghost size_t stmp = spos;
spos += max( good_suffix[ppos], ppos - bad_character[string[ppos + spos]] );
//@ assert spos > stmp;
}

// {3.3} It is impossible to prove this assert.
//@ assert \valid_range( good_suffix, 0, plen - 1 );

_free( good_suffix );

No Comments Have Been Posted

Attachments:
Size Name Date By Download
9 KiBtest.c2010-12-25 14:53evdenistest.c
Field Old Value Date By
File Added2061: test.c2010-12-25 14:53evdenis