Function read_pdf_file

src/file_pdf.c:439–463

@ @ requires \valid_read(buffer+(0..512-1)); @ assigns \nothing; @*/

  @ assigns  \nothing;
  @*/
static uint64_t read_pdf_file(const unsigned char *buffer)
{
  const unsigned char sig_linearized[10]={'L','i','n','e','a','r','i','z','e','d'};
  const char *src;
  unsigned int i;
  const char *sbuffer=(const char *)buffer;
  src=(const char *)td_memmem(sbuffer, 512, sig_linearized, sizeof(sig_linearized));
  if(src == NULL)
    return 0;
  i = src - sbuffer;
  i+=sizeof(sig_linearized);
  if( i >= 512 -1)
    return 0;
  /*@ assert i < 512-1; */
  /*@
    @ loop assigns i;
    @ loop variant 512 - 1 - i;
    @ */
  for(; i < 512-1 && buffer[i]!='>'; i++)
  {
    if(buffer[i]=='/' && buffer[i+1]=='L')
      return read_pdf_file_aux(buffer, i+2);
  }
  return 0;
}

/*@
  @ requires buffer_size >= 512;