typedef /*@abstract@*/ char *mstring;

int faucet (void)
{
  int *x = (int *) malloc (sizeof (int) * 24);

  /*
  ** silly program ...
  */

  return 3;
}