Function set_part_name

src/common.c:189–204

#endif

void set_part_name(partition_t *partition, const char *src, const unsigned int max_size)
{
  unsigned int i;
  /*@
    @ loop invariant \separated(partition, src + (..));
    @ loop invariant 0 <= i < sizeof(partition->fsname);
    @ loop invariant 0 <= i <= max_size;
    @ loop invariant \initialized(partition->fsname+(0 .. i-1));
    @ loop assigns i, partition->fsname[0 .. i];
    @ loop variant sizeof(partition->fsname)-1 - i;
    @*/
  for(i=0; i<sizeof(partition->fsname)-1 && i<max_size && src[i]!='\0'; i++)
    partition->fsname[i]=src[i];
  partition->fsname[i]='\0';
  /*@ assert valid_string((char *)&partition->fsname); */
}

void set_part_name_chomp(partition_t *partition, const char *src, const unsigned int max_size)
{