Function file_add_data

src/psearch.h:28–52

@ @ requires \valid(data); @*/

  @ requires \valid(data);
  @*/
static inline alloc_data_t *file_add_data(alloc_data_t *data, const uint64_t offset, const unsigned int content)
{
  if(!(data->start <= offset && offset <= data->end))
  {
    log_critical("file_add_data: bug\n");
    return data;
  }
  if(data->start==offset)
  {
    data->data=content;
    return data;
  }
  if(data->data==content)
    return data;
  {
    alloc_data_t *datanext=(alloc_data_t*)MALLOC(sizeof(*datanext));
    memcpy(datanext, data, sizeof(*datanext));
    data->end=offset-1;
    datanext->start=offset;
    datanext->file_stat=NULL;
    datanext->data=content;
    td_list_add(&datanext->list, &data->list);
    return datanext;
  }
}

/*@
  @ requires \valid(dst);