Function zip_parse_end_central_dir

src/file_zip.c:885–918

@ @ requires \valid(fr); @ requires \valid(fr->handle); @ requires fr->file_size < 0x8000000000000000; @ requires \separated(fr, fr->handle, &errno, &Frama_C_entropy_source); @ ensures \result == -1 || \result == 0; @ assigns *fr->handle, fr->file_size, errno, Frama_C_entropy_source; @*/

  @ assigns  *fr->handle, fr->file_size, errno, Frama_C_entropy_source;
  @*/
static int zip_parse_end_central_dir(file_recovery_t *fr)
{
  char buffer[sizeof(struct zip_end_central_dir)];
  const struct zip_end_central_dir *dir=(const struct zip_end_central_dir *)&buffer;

  if (fread(&buffer, sizeof(struct zip_end_central_dir), 1, fr->handle) != 1)
  {
#ifdef DEBUG_ZIP
    log_trace("zip: Unexpected EOF reading header of zip_parse_end_central_dir\n");
#endif
    return -1;
  }
#if defined(__FRAMAC__)
  Frama_C_make_unknown(buffer, sizeof(struct zip_end_central_dir));
#endif
  fr->file_size += sizeof(struct zip_end_central_dir);

  if (dir->comment_length)
  {
    const uint16_t len = le16(dir->comment_length);
    if (my_fseek(fr->handle, len, SEEK_CUR) == -1)
    {
#ifdef DEBUG_ZIP
      log_trace("zip: Unexpected EOF in end_central_dir: expected %u bytes\n", len);
#endif
      return -1;
    }
    fr->file_size += len;
#ifdef DEBUG_ZIP
    log_trace("zip: Comment of length %u\n", len);
#endif
  }
  return 0;
}

/*@
  @ requires \valid(fr);