Function file_get_pos

src/file_zip.c:202–262

@ @ requires \valid(f); @ requires 0 < size <= 4096; @ requires \valid_read((const char *)needle + (0 .. size-1)); @ requires \separated(f, (const char *)needle+(..), &errno, &Frama_C_entropy_source); @ assigns *f,errno; @ assigns Frama_C_entropy_source; @*/

  @ assigns Frama_C_entropy_source;
  @*/
static int64_t file_get_pos(FILE *f, const void* needle, const unsigned int size)
{
  char     buffer[4096];
  int64_t  total   = 0;
#ifdef DEBUG_ZIP
  log_trace("zip: file_get_pos(f, needle, %u)\n", size);
#endif

  /*@
    @ loop assigns total, *f, errno, buffer[0..4096-1];
    @ loop assigns Frama_C_entropy_source;
    @*/
  while (!feof(f))
  {
    const size_t read_size=fread(&buffer, 1, 4096, f);
    if(read_size <= 0 || total > (0x7fffffffffffffff - 4096))
    {
      return -1;
    }
    /*@ assert 0 < read_size <= 4096; */
    /*@ assert total <= 0x8000000000000000 - 4096; */
#if defined(__FRAMAC__)
    Frama_C_make_unknown(&buffer, 4096);
#endif
    if(read_size >= size)
    {
      /*@ assert read_size >= size; */
      const unsigned int count_max=read_size - size;
      unsigned int count = 0;
      // TODO loop invariant 0 <= count <= count_max + 1;
      /*@
	@ loop assigns count, *f, errno;
	@ loop variant count_max - count;
	@*/
      for(count=0; count <= count_max; count++)
      {
	/*@ assert count <= count_max; */
	if (buffer[count]==*(const char *)needle && memcmp(buffer+count, needle, size)==0)
	{
	  if(my_fseek(f, (off_t)count-(off_t)read_size, SEEK_CUR)<0)
	  {
#if !defined(DISABLED_FOR_FRAMAC)
	    log_trace("zip: file_get_pos count-read failed\n");
#endif
	    return -1;
	  }
	  return total+count;
	}
      }
      total+=count_max+1;
    }
    if(feof(f) || my_fseek(f, (off_t)1-size, SEEK_CUR)<0)
    {
#if !defined(DISABLED_FOR_FRAMAC)
      log_trace("zip: file_get_pos 1-size failed\n");
#endif
      return -1;
    }