Function file_rename

src/filegen.c:821–837

The original filename begins at offset in buffer and is null terminated */

/* The original filename begins at offset in buffer and is null terminated */
int file_rename(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int append_original_ext)
{
  /*@ assert valid_file_recovery(file_recovery); */
  if(file_recovery->filename[0] == 0)
    return 0;
  /*@ assert strlen((char *)&file_recovery->filename) > 0; */
  /*@ assert new_ext==\null || valid_read_string(new_ext); */
  if(buffer!=NULL && 0 <= offset && offset < buffer_size &&
      _file_rename(file_recovery->filename, buffer, buffer_size, offset, new_ext, append_original_ext)==0)
    return 0;
  /*@ assert valid_string((char *)(&file_recovery->filename)); */
  /*@ assert new_ext==\null || valid_read_string(new_ext); */
  if(new_ext==NULL)
    return 0;
  /* Try without the original filename */
  return file_rename_aux(file_recovery, new_ext);
}

/* The original filename begins at offset in buffer and is null terminated */
/*@