Function pos_in_mem

src/file_zip.c:1396–1410

@ @ requires haystack_size > 0; @ requires needle_size > 0; @ requires \valid_read(haystack + (0 .. haystack_size-1)); @ requires \valid_read(needle + (0 .. needle_size-1)); @ assigns \nothing; @ ensures \result <= haystack_size; @*/

  @ ensures \result <= haystack_size;
  @*/
static unsigned int pos_in_mem(const unsigned char *haystack, const unsigned int haystack_size, const unsigned char *needle, const unsigned int needle_size)
{
  unsigned int i;
  if(haystack_size < needle_size)
    return 0;
  /*@
    @ loop invariant 0 <= i <= haystack_size - needle_size + 1;
    @ loop assigns i;
    @ loop variant haystack_size - needle_size - i;
    @*/
  for(i=0; i <= haystack_size - needle_size; i++)
    if(memcmp(&haystack[i],needle,needle_size)==0)
      return (i+needle_size);
  return 0;
}

/*@
  @ requires valid_register_header_check(file_stat);