Function zip_parse_data_desc

src/file_zip.c:928–953

@ @ 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_data_desc(file_recovery_t *fr)
{
  char buffer[sizeof(struct zip_desc)];
  const struct zip_desc *desc=(const struct zip_desc *)&buffer;
  if (fread(&buffer, sizeof(buffer), 1, fr->handle) != 1)
  {
#ifdef DEBUG_ZIP
    log_trace("zip: Unexpected EOF reading header of data_desc\n");
#endif
    return -1;
  }
#if defined(__FRAMAC__)
  Frama_C_make_unknown(buffer, sizeof(buffer));
#endif
  fr->file_size += sizeof(struct zip_desc);
#ifdef DEBUG_ZIP
  log_info("compressed_size=%u/%lu uncompressed_size=%u CRC32=0x%08X\n",
      le32(desc->compressed_size),
      expected_compressed_size,
      le32(desc->uncompressed_size),
      le32(desc->crc32));
#endif
  if(le32(desc->compressed_size)!=expected_compressed_size)
    return -1;
  return 0;
}

/*@
  @ requires \valid(fr);