Function get_int_from_command

src/common.c:475–500

}

uint64_t get_int_from_command(char **current_cmd)
{
  uint64_t tmp=0;
  /*@
    @ loop invariant valid_read_string(*current_cmd);
    @ loop assigns *current_cmd, tmp;
    @ loop variant strlen(*current_cmd);
    @*/
  while(*current_cmd[0] >='0' && *current_cmd[0] <= '9')
  {
#ifdef __FRAMAC__
    const unsigned int v=*current_cmd[0] - '0';
    /*@ assert 0 <= v <= 9; */
    if(tmp >= UINT64_MAX / 10)
      return tmp;
    /** assert tmp < UINT64_MAX / 10; */
    tmp *= 10;
    /** assert tmp <= UINT64_MAX - 10; */
    tmp += v;
#else
    tmp = tmp * 10 + (*current_cmd[0] - '0');
#endif
    (*current_cmd)++;
  }
  return tmp;
}