Function file_rename_doc

src/file_doc.c:1555–1798

@ @ requires file_recovery->file_rename==&file_rename_doc; @ requires valid_file_rename_param(file_recovery); @ ensures valid_file_rename_result(file_recovery); @*/

  @ ensures  valid_file_rename_result(file_recovery);
  @*/
static void file_rename_doc(file_recovery_t *file_recovery)
{
  const char *ext=NULL;
  char title[1024];
  FILE *file;
  unsigned char buffer_header[512];
  uint32_t *fat;
  const struct OLE_HDR *header=(const struct OLE_HDR*)&buffer_header;
  /*@ assert \valid_read(header); */
  time_t file_time=0;
  unsigned int fat_entries;
  unsigned int uSectorShift;
  unsigned int num_FAT_blocks;
  title[0]='\0';
  /*@ assert valid_string(&title[0]); */
  if(strstr(file_recovery->filename, ".sdd")!=NULL)
    ext=extension_sdd;
  if((file=fopen(file_recovery->filename, "rb"))==NULL)
    return;
#ifdef DEBUG_OLE
  log_info("file_rename_doc(%s)\n", file_recovery->filename);
#endif
  /*reads first sector including OLE header */
  if(my_fseek(file, 0, SEEK_SET) < 0 ||
      fread(&buffer_header, sizeof(buffer_header), 1, file) != 1)
  {
    fclose(file);
    return ;
  }
#if defined(__FRAMAC__)
  Frama_C_make_unknown((char *)&buffer_header, sizeof(buffer_header));
#endif
  uSectorShift=le16(header->uSectorShift);
  num_FAT_blocks=le32(header->num_FAT_blocks);
  /* Sanity check */
  if( uSectorShift != 9 && uSectorShift != 12)
  {
    fclose(file);
    return ;
  }
  /*@ assert 9 == uSectorShift || 12 == uSectorShift; */
  if(le16(header->uMiniSectorShift) != 6)
  {
    fclose(file);
    return ;
  }
  /* Sanity check */
  if(num_FAT_blocks==0 ||
      le32(header->num_extra_FAT_blocks)>50)
  {
    fclose(file);
    return ;
  }
  /*@ assert num_FAT_blocks > 0; */
  /*@ assert 0 <= le32(header->num_extra_FAT_blocks) <= 50; */
  if(num_FAT_blocks > 109+le32(header->num_extra_FAT_blocks)*((1<<uSectorShift)/4-1))
  {
    fclose(file);