void
test( const unsigned char * const pattern, const unsigned int plen )
{
	long int bad_character[256];
	
	/*@
	  @ loop invariant 0 <= i <= plen;
	  @ loop variant plen - i;
      @ loop assigns *( bad_character + { pattern[k] | integer k ; 0 <= k < i } );
	  @*/
	for( unsigned int i = 0; i < plen; ++i ) {
		bad_character[pattern[i]] = i;
	}

}