Function file_check_zip

src/file_zip.c:1028–1129

@ @ requires fr->file_check==&file_check_zip; @ requires valid_file_check_param(fr); @ ensures valid_file_check_result(fr); @ assigns *fr->handle, fr->file_size; @ assigns fr->time, fr->offset_ok, fr->offset_error; @ assigns Frama_C_entropy_source, errno; @ assigns first_filename[0 .. 255]; @ assigns msoffice, sh3d, ext_msoffice, expected_compressed_size; @*/

  @ assigns msoffice, sh3d, ext_msoffice, expected_compressed_size;
  @*/
static void file_check_zip(file_recovery_t *fr)
{
  const char *ext=NULL;
  unsigned int file_nbr=0;
  fr->file_size = 0;
  fr->offset_error=0;
  fr->offset_ok=0;
  /* fr->time is already set to 0 but it helps frama-c */
  fr->time=0;
  first_filename[0]='\0';
  if(my_fseek(fr->handle, 0, SEEK_SET) < 0)
    return ;
  /*@
    @ loop assigns *fr->handle, fr->file_size, ext, file_nbr;
    @ loop assigns fr->time, fr->offset_ok, fr->offset_error;
    @ loop assigns Frama_C_entropy_source, errno;
    @ loop assigns first_filename[0 .. 255];
    @ loop assigns msoffice, sh3d, ext_msoffice, expected_compressed_size;
    @*/
  while (1)
  {
    uint64_t file_size_old;
    char buf_header[sizeof(uint32_t)];
    const uint32_t *header_ptr=(const uint32_t *)&buf_header;
    uint32_t header;
    int      status;
    if(file_nbr>=0xffffffff || fr->file_size >= 0x8000000000000000 - 4)
    {
      fr->offset_error = fr->file_size;
      fr->file_size = 0;
      return;
    }
    /*@ assert fr->file_size < 0x8000000000000000 - 4; */
    if (fread(&buf_header, 4, 1, fr->handle)!=1)
    {
#ifdef DEBUG_ZIP
      log_trace("Failed to read block header\n");
#endif
      fr->offset_error=fr->file_size;
      fr->file_size=0;
      return;
    }
#if defined(__FRAMAC__)
    Frama_C_make_unknown(&buf_header, 4);
#endif
    header = le32(*header_ptr);
#ifdef DEBUG_ZIP
    log_trace("Header 0x%08X at 0x%llx\n", header, (long long unsigned int)fr->file_size);
    log_flush();
#endif
    fr->file_size += 4;
    file_size_old=fr->file_size;
    /*@ assert fr->file_size < 0x8000000000000000; */

    switch (header)
    {
      case ZIP_CENTRAL_DIR: /* Central dir */
        status = zip_parse_central_dir(fr);