const char* @symbol@(void)
{
  return "INFO:symbol[@symbol@]";
}