[splint.git] / src / cstring.c

/*
** Splint - annotation-assisted static program checker
** Copyright (C) 1994-2002 University of Virginia,
**         Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
** under the terms of the GNU General Public License as published by the
** Free Software Foundation; either version 2 of the License, or (at your
** option) any later version.
** 
** This program is distributed in the hope that it will be useful, but
** WITHOUT ANY WARRANTY; without even the implied warranty of
** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
** General Public License for more details.
** 
** The GNU General Public License is available from http://www.gnu.org/ or
** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
** MA 02111-1307, USA.
**
** For information on splint: info@splint.org
** To report a bug: splint-bug@splint.org
** For more information: http://www.splint.org
*/
/*
** cstring.c
*/

/*
 * Herbert 06/12/2000
 * - use drive spec specials with OS2 like with WIN32
 * - cstring_replaceAll () needed in cpplib.c
 */

# include "splintMacros.nf"
# include "basic.h"
# include "osd.h"
# include "portab.h"

/*@only@*/ /*@notnull@*/ 
cstring cstring_newEmpty (void)
{
  return (cstring_create (0));
}

char cstring_firstChar (cstring s) 
{
  llassert (cstring_isDefined (s));
  llassert (cstring_length (s) > 0);

  return (s[0]);
}

char cstring_getChar (cstring s, int n) 
{
  int length = cstring_length (s);

  llassert (cstring_isDefined (s));
  llassert (n >= 1 && n <= length);

  return (s[n - 1]);
}

cstring cstring_suffix (cstring s, int n) 
{
  llassert (cstring_isDefined (s));
  llassert (n <= cstring_length (s));

  return (s + n);
}

cstring cstring_prefix (cstring s, int n) /*@requires maxRead(s) >= n /\ maxSet(s) >= n @*/ /*@ensures maxRead(result) == n /\ maxSet(result) == n @*/
{
  cstring t;
  char c;
  llassert (cstring_isDefined (s));
  llassert (n <= cstring_length (s));

  c = *(s + n);
  /*@-mods@*/  /* The modifications cancel out. */
  *(s + n) = '\0';
  t = cstring_copy (s);
  *(s + n) = c;
  /*@=mods@*/

  return t;
}

/* effects If s = [0-9]*, returns s as an int.
**         else returns -1.
*/

int cstring_toPosInt (cstring s)
{
  int val = 0;

  cstring_chars (s, c)
    {
      if (isdigit ((unsigned char) c))
	{
	  val = (val * 10) + (int)(c - '0');
	}
      else
	{
	  return -1;
	}
    } end_cstring_chars ; 

  return val;
}

cstring cstring_afterChar (cstring s, char c) 
{
  llassert (cstring_isDefined (s));
  return strchr (s, c);
}

cstring cstring_beforeChar (cstring s, char c)
{
  if (cstring_isDefined (s))
    {
      char *cp = strchr (s, c);

      if (cp != NULL)
	{
	  cstring ret;

	  /*@-mods@*/
	  *cp = '\0';
	  ret = cstring_copy (s);
	  *cp = c;
	  /*@=mods@*/ /* modification is undone */
	  
	  return ret;
	}
    }

  return cstring_undefined;
}

void cstring_setChar (cstring s, int n, char c) /*@requires maxRead(s) >= (n - 1) /\ maxSet(s) >= (n - 1) @*/
{
  llassert (cstring_isDefined (s));
  llassert (n > 0 && n <= cstring_length (s));

  s[n - 1] = c;
}

char cstring_lastChar (cstring s) 
{
  int length;

  llassert (cstring_isDefined (s));

  length = cstring_length (s);
  llassert (length > 0);

  return (s[length - 1]);
}

/*@only@*/ cstring cstring_copy (cstring s) /*@ensures maxSet(result) == maxRead(s) /\ maxRead(result) == maxRead(s) @*/
{
  if (cstring_isDefined (s))
    {
      return (mstring_copy (s));
    }
  else
    {
      return cstring_undefined;
    }
}

/*@only@*/ cstring cstring_copyLength (char *s, int len) /*@requires maxSet(s) >= (len - 1) @*/
{
  char *res = mstring_create (len + 1);

  strncpy (res, s, size_fromInt (len));
  res[len] = '\0';
  return res;
}

bool cstring_containsChar (cstring c, char ch)
{
  if (cstring_isDefined (c))
    {
      return (strchr (c, ch) != NULL);
    }
  else
    {
      return FALSE;
    }
}

/*
** Replaces all occurances of old in s with new.
*/

void cstring_replaceAll (cstring s, char old, char snew)
{
  
  llassert (old != snew);

  if (cstring_isDefined (s))
    {
      char *sp = strchr (s, old);

      while (sp != NULL)
	{
	  *sp = snew;
	  sp = strchr (sp, old);
	}

          }
}

void cstring_replaceLit (/*@unique@*/ cstring s, char *old, char *snew) 
   /*@requires maxRead(snew) >= 0 /\ maxRead(old) >= 0 /\ maxRead(old) >= maxRead(snew) @*/
{
  llassert (strlen (old) >= strlen (snew));
  
  if (cstring_isDefined (s))
    {
      char *sp = strstr (s, old);

      while (sp != NULL)
	{
	  int lendiff = size_toInt (strlen (old) - strlen (snew));
	  char *tsnew = snew;

	  llassert (lendiff >= 0);

	  while (*tsnew != '\0')
	    {
	      llassert (*sp != '\0');
	      *sp++ = *tsnew++;
	    }
	  
	  if (lendiff > 0)
	    {
	      while (*(sp + lendiff) != '\0')
		{
		  *sp = *(sp + lendiff);
		  sp++;
		}
	      
	      *sp = '\0';
	    }

	  sp = strstr (s, old);
	}
    }
}

/*
** removes all chars in clist from s
*/

void cstring_stripChars (cstring s, const char *clist)
{
  if (cstring_isDefined (s))
    {
      int i;
      int size = cstring_length (s);

      for (i = 0; i < size; i++)
	{
/*drl bee: is*/ 	  char c = s[i];
	  
	  if (strchr (clist, c) != NULL)
	    {
	      /* strip this char */
	      int j;
	      
	      size--;

	      for (j = i; j < size; j++)
		{
	/*drl bee: is*/ 	/*drl bee: is*/   s[j] = s[j+1];
		}

	  /*drl bee: is*/     s[size] = '\0'; 
	      i--;
	    }
	}
    }
}

bool cstring_contains (/*@unique@*/ cstring c, cstring sub)
{
  if (cstring_isDefined (c))
    {
      llassert (cstring_isDefined (sub));
      
      return (strstr (c, sub) != NULL);
    }
  else
    {
      return FALSE;
    }
}

static char lookLike (char c) /*@*/
{
  if (c == 'I' || c == 'l')
    {
      return '1';
    }
  else if (c == 'O' || c == 'o')
    {
      return '0';
    }
  else if (c == 'Z')
    {
      return '2';
    }
  else if (c == 'S')
    {
      return '5';
    }
  else
    {
      return c;
    }
}

cmpcode cstring_genericEqual (cstring s, cstring t,
			      int nchars,
			      bool caseinsensitive,
			      bool lookalike)  /*@requires maxRead(s) >= nchars /\ maxRead(t) >= nchars @*/
{
  if (s == t) return CGE_SAME;
  else if (cstring_isUndefined (s))
    {
      return cstring_isEmpty (t) ? CGE_SAME : CGE_DISTINCT;
    }
  else if (cstring_isUndefined (t))
    {
      return cstring_isEmpty (s) ? CGE_SAME : CGE_DISTINCT;
    }
  else
    {
      int i = 0;
      bool diffcase = FALSE;
      bool difflookalike = FALSE;

      while (*s != '\0')
	{
	  if (nchars > 0 && i >= nchars)
	    {
	      break;
	    }

	  if (*t == *s)
	    {
	      ; /* no difference */
	    }
	  else if (caseinsensitive 
		   && (toupper ((int) *t) == toupper ((int) *s)))
	    {
	      diffcase = TRUE;
	    }
	  else if (lookalike && (lookLike (*t) == lookLike (*s)))
	    {
	      difflookalike = TRUE;
	    }
	  else 
	    {
	      return CGE_DISTINCT;
	    }
	  i++;
	  s++;
	  t++;
	}

  /*drl bee: ib*/
      /*drl bee: ib*/ 
      if (*s == '\0' && *t != '\0')
	{
	  return CGE_DISTINCT;
	}

      if (diffcase)
	{
	  return CGE_CASE;
	}
      else if (difflookalike)
	{
	  return CGE_LOOKALIKE;
	}
      else
	{
	  return CGE_SAME;
	}
    }
}


bool cstring_equalFree (/*@only@*/ cstring c1, /*@only@*/ cstring c2)
{
  bool res = cstring_equal (c1, c2);
  cstring_free (c1);
  cstring_free (c2);
  return res;
}

bool cstring_equal (cstring c1, cstring c2)
{
  if (c1 == c2) return TRUE;
  else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
  else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
  else return (strcmp (c1, c2) == 0);
}

bool cstring_equalLen (cstring c1, cstring c2, int len)
{
  if (c1 == c2) return TRUE;
  else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
  else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
  else return (strncmp (c1, c2, size_fromInt (len)) == 0);
}

bool cstring_equalCaseInsensitive (cstring c1, cstring c2)
{
  if (c1 == c2) return TRUE;
  else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
  else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
  else return (cstring_genericEqual (c1, c2, 0, TRUE, FALSE) != CGE_DISTINCT);
}

bool cstring_equalLenCaseInsensitive (cstring c1, cstring c2, int len)
{
  llassert (len >= 0);

  if (c1 == c2) return TRUE;
  else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
  else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
  else return (cstring_genericEqual (c1, c2, len, TRUE, FALSE) != CGE_DISTINCT);
}

bool cstring_equalPrefix (cstring c1, cstring c2)
{
  llassert (c2 != NULL);

  if (cstring_isUndefined (c1)) 
    {
      return (strlen (c2) == 0);
    }

  return (strncmp (c1, c2, strlen (c2)) == 0);
}

bool cstring_equalPrefixLit (cstring c1, const char *c2)
{
  llassert (c2 != NULL);

  if (cstring_isUndefined (c1)) 
    {
      return (strlen (c2) == 0);
    }

  return (strncmp (c1, c2, strlen (c2)) == 0);
}

int cstring_xcompare (cstring *c1, cstring *c2)
{
  return (cstring_compare (*c1, *c2));
}

int cstring_compare (cstring c1, cstring c2)
{
  int res;

  if (c1 == c2)
    {
      res = 0;
    }
  else if (cstring_isUndefined (c1))
    {
      if (cstring_isEmpty (c2))
	{
	  res = 0;
	}
      else
	{
	  res = 1;
	}
    }
  else if (cstring_isUndefined (c2))
    {
      if (cstring_isEmpty (c1))
	{
	  res = 0;
	}
      else
	{
	  res = -1;
	}
    }
  else
    {
      res = strcmp (c1, c2);
    }

    return (res);
}

void cstring_markOwned (/*@owned@*/ cstring s)
{
  sfreeEventually (s);
}

void cstring_free (/*@only@*/ cstring s)
{
  if (cstring_isDefined (s)) 
    {
      sfree (s);
    }
}

cstring cstring_fromChars (/*@exposed@*/ const char *cp)
{
  return (cstring) cp;
}

/*@exposed@*/ char *cstring_toCharsSafe (cstring s)
{
  static /*@only@*/ cstring emptystring = cstring_undefined;

  if (cstring_isDefined (s))
    {
      return (char *) s;
    }
  else
    {
      if (cstring_isUndefined (emptystring))
	{
	  emptystring = cstring_newEmpty ();
	}

      return emptystring;
    }
}

int cstring_length (cstring s)
{
  if (cstring_isDefined (s))
    {
      return size_toInt (strlen (s));
    }
  return 0;
}

cstring
cstring_capitalize (cstring s) /*@requires maxSet(s) >= 0 @*/
{
  if (!cstring_isEmpty (s))
    {
      cstring ret = cstring_copy (s);

      cstring_setChar (ret, 1, (char) toupper ((int) cstring_firstChar (ret)));
      return ret;
    }
  
  return cstring_undefined;
}

cstring
cstring_capitalizeFree (cstring s) /*@requires maxSet(s) >= 0 /\ maxRead(s) >= 0 @*/
{
  if (!cstring_isEmpty (s))
    {
      cstring_setChar (s, 1, (char) toupper ((int) cstring_firstChar (s)));
      return s;
    }
  
  return s;
}

cstring
cstring_clip (cstring s, int len)
{
  if (cstring_isUndefined (s) || cstring_length (s) <= len)
    {
      ;
    }
  else
    {
      llassert (s != NULL);
    /*drl bee: mrms*/   *(s + len) = '\0';
    }

  return s;
}

/*@only@*/ cstring
cstring_elide (cstring s, int len)
{
  if (cstring_isUndefined (s) || cstring_length (s) <= len)
    {
      return cstring_copy (s);
    }
  else
    {
      cstring sc = cstring_create (len);
     
      strncpy (sc, s, size_fromInt (len));
     /*drl bee: mrms*/  *(sc + len - 1) = '\0';
      *(sc + len - 2) = '.';      
      *(sc + len - 3) = '.';      
      *(sc + len - 4) = '.';      
      return sc;
    }
}

/*@only@*/ cstring
cstring_fill (cstring s, int n) /*@requires n >= 0 @*/
{
  cstring t = cstring_create (n + 1);
  cstring ot = t;
  int len = cstring_length (s);
  int i;
  
  if (len > n)
    {
      for (i = 0; i < n; i++)
	{
	/*drl bee: is*/
	  /*drl bee: is*/ 
	  *t++ = *s++;
	}
      *t = '\0';
    }
  else
    {
      for (i = 0; i < len; i++)
	{
	/*drl bee: is*/
/*drl bee: is*/ 
	  *t++ = *s++;
	}
      for (i = 0; i < n - len; i++)
	{
/*drl bee: is*/ 
	  *t++ = ' ';
	}
      *t = '\0';
    }

  return ot;
}

cstring
cstring_downcase (cstring s)
{
  if (cstring_isDefined (s))
    {
      cstring t = cstring_create (strlen (s) + 1);
      cstring ot = t;
      char c;
      
 /*drl bee: lhnt*/      while ((c = *s) != '\0')
	{
	  if (c >= 'A' && c <= 'Z')
	    {
	      c = c - 'A' + 'a';
	    }
	  *t++ = c;
	  s++;
	}
     /*drl bee: is*/  *t = '\0';
      
      return ot;
    }
  else
    {
      return cstring_undefined;
    }
}

/*@notnull@*/ cstring 
cstring_appendChar (/*@only@*/ cstring s1, char c)
{
  int l = cstring_length (s1);
  char *s;

  s = (char *) dmalloc (sizeof (*s) * (l + 2));

  if (cstring_isDefined (s1))
    {  
      strcpy (s, s1);
      *(s + l) = c;
      /*drl bee: dm*/ *(s + l + 1) = '\0';
      sfree (s1); 
    }
  else
    {
      *(s) = c;
      /*drl bee: dm*/  *(s + 1) = '\0';
    } 

  return s;
}

/*@only@*/ cstring 
cstring_concatFree (cstring s, cstring t)
{
  cstring res = cstring_concat (s, t);
  cstring_free (s);
  cstring_free (t);
  return res;
}

/*@only@*/ cstring 
cstring_concatFree1 (cstring s, cstring t)
{
  cstring res = cstring_concat (s, t);
  cstring_free (s);
  return res;
}

# ifndef NOLCL
/*@only@*/ cstring 
cstring_concatChars (cstring s, char *t)
{
  cstring res = cstring_concat (s, cstring_fromChars (t));
  cstring_free (s);
  return res;
}
# endif

/*@only@*/ cstring 
cstring_concatLength (cstring s1, char *s2, int len) /*@requires maxSet(s2) >= (len - 1) @*/
{
  cstring tmp = cstring_copyLength (s2, len);
  cstring res = cstring_concat (s1, tmp);
  cstring_free (tmp);
  cstring_free (s1);

  return res;
}

/*@only@*/ cstring 
cstring_concat (cstring s, cstring t) /*@requires maxSet(s) >= 0 @*/
{
  char *ret = mstring_create (cstring_length (s) + cstring_length (t));

  if (cstring_isDefined (s))
    {
    /*drl bee: sl*/   strcpy (ret, s);
    }
  if (cstring_isDefined (t))
    {
      strcat (ret, t);
    }

  return ret;
}

/*@notnull@*/ /*@only@*/ cstring 
cstring_prependCharO (char c, /*@only@*/ cstring s1)
{
  cstring res = cstring_prependChar (c, s1);

  cstring_free (s1);
  return (res);
}

/*@notnull@*/ /*@only@*/ cstring 
cstring_prependChar (char c, /*@temp@*/ cstring s1)
{
  int l = cstring_length (s1);
  char *s = (char *) dmalloc (sizeof (*s) * (l + 2));
  
/*drl bee: dm*/   *(s) = c;

  if (cstring_isDefined (s1)) 
    {
      /*@-mayaliasunique@*/ 
      strcpy (s + 1, s1);
      /*@=mayaliasunique@*/ 
    }

 /*drl bee: dm*/ *(s + l + 1) = '\0';
  return s;
}

# ifndef NOLCL
bool
cstring_hasNonAlphaNumBar (cstring s)
{
  int c;

  if (cstring_isUndefined (s)) return FALSE;

/*drl bee: lhnt*/  while ((c = (int) *s) != (int) '\0')
    {
      if ((isalnum (c) == 0) && (c != (int) '_')
	  && (c != (int) '.') && (c != (int) CONNECTCHAR))
	{
	  return TRUE;
	}

      s++;
    }
  return FALSE;
}
# endif

/*@only@*/ /*@notnull@*/ cstring 
cstring_create (int n)
{
  char *s = dmalloc (sizeof (*s) * (n + 1));

 /*drl bee: dm*/ *s = '\0';
  return s;
}

/*@only@*/ /*@notnull@*/ cstring
cstring_copySegment (cstring s, int findex, int tindex)
{
  cstring res = cstring_create (tindex - findex + 1);

  llassert (cstring_isDefined (s));
  llassert (cstring_length (s) > tindex);

  strncpy (res, (s + findex), size_fromInt ((tindex - findex + 1)));
  return res;
}

# ifndef NOLCL
lsymbol cstring_toSymbol (cstring s)
{
  lsymbol res = lsymbol_fromString (s);

  cstring_free (s);
  return res;
}
# endif

cstring cstring_bsearch (cstring key, char **table, int nentries)
{
  if (cstring_isDefined (key))
    {
      int low = 0;
      int high = nentries;
      int mid = (high + low + 1) / 2;
      int last = -1;
      cstring res = cstring_undefined;

      while (low <= high && mid < nentries)
	{
	  int cmp;

	  llassert (mid != last);
	  llassert (mid >= 0 && mid < nentries);

	  cmp = cstring_compare (key, table[mid]);
	  
	  if (cmp == 0)
	    {
	      res = table[mid];
	      break;
	    }
	  else if (cmp < 0) /* key is before table[mid] */
	    {
	      high = mid - 1;
	    }
	  else /* key of after table[mid] */
	    {
	      low = mid + 1;
	    }

	  last = mid;
	  mid = (high + low + 1) / 2;
	}

      if (mid != 0 && mid < nentries - 1)
	{
	  llassert (cstring_compare (key, table[mid - 1]) > 0);
	/*drl bee: ndv*/  llassert (cstring_compare (key, table[mid + 1]) < 0);
	}

      return res;
    }
  
  return cstring_undefined;
}

extern /*@observer@*/ cstring cstring_advanceWhiteSpace (cstring s)
{
  if (cstring_isDefined (s)) {
    char *t = s;

 /*drl bee: lhnt*/   while (*t != '\0' && isspace ((int) *t)) {
      t++;
    }

    return t;
  }
  
  return cstring_undefined;
}
Commit	Line	Data
616915dd	1	/*
11db3170	2	** Splint - annotation-assisted static program checker
77d37419	3	** Copyright (C) 1994-2002 University of Virginia,
616915dd	4	** Massachusetts Institute of Technology
	5	**
	6	** This program is free software; you can redistribute it and/or modify it
	7	** under the terms of the GNU General Public License as published by the
	8	** Free Software Foundation; either version 2 of the License, or (at your
	9	** option) any later version.
	10	**
	11	** This program is distributed in the hope that it will be useful, but
	12	** WITHOUT ANY WARRANTY; without even the implied warranty of
	13	** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
	14	** General Public License for more details.
	15	**
	16	** The GNU General Public License is available from http://www.gnu.org/ or
	17	** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
	18	** MA 02111-1307, USA.
	19	**
155af98d	20	** For information on splint: info@splint.org
155af98d	21	** To report a bug: splint-bug@splint.org
11db3170	22	** For more information: http://www.splint.org
616915dd	23	*/
	24	/*
	25	** cstring.c
	26	*/
	27
	28	/*
	29	* Herbert 06/12/2000
	30	* - use drive spec specials with OS2 like with WIN32
	31	* - cstring_replaceAll () needed in cpplib.c
	32	*/
	33
1b8ae690	34	# include "splintMacros.nf"
616915dd	35	# include "basic.h"
	36	# include "osd.h"
	37	# include "portab.h"
	38
2934b455	39	/@only@/ /@notnull@/
616915dd	40	cstring cstring_newEmpty (void)
	41	{
	42	return (cstring_create (0));
	43	}
	44
	45	char cstring_firstChar (cstring s)
	46	{
	47	llassert (cstring_isDefined (s));
	48	llassert (cstring_length (s) > 0);
	49
	50	return (s[0]);
	51	}
	52
	53	char cstring_getChar (cstring s, int n)
	54	{
	55	int length = cstring_length (s);
	56
	57	llassert (cstring_isDefined (s));
	58	llassert (n >= 1 && n <= length);
	59
	60	return (s[n - 1]);
	61	}
	62
	63	cstring cstring_suffix (cstring s, int n)
	64	{
	65	llassert (cstring_isDefined (s));
	66	llassert (n <= cstring_length (s));
	67
	68	return (s + n);
	69	}
	70
86d93ed3	71	cstring cstring_prefix (cstring s, int n) /@requires maxRead(s) >= n /\ maxSet(s) >= n @/ /@ensures maxRead(result) == n /\ maxSet(result) == n @/
616915dd	72	{
	73	cstring t;
	74	char c;
	75	llassert (cstring_isDefined (s));
	76	llassert (n <= cstring_length (s));
	77
	78	c = *(s + n);
	79	/@-mods@/ /* The modifications cancel out. */
	80	*(s + n) = '\0';
	81	t = cstring_copy (s);
	82	*(s + n) = c;
	83	/@=mods@/
	84
	85	return t;
	86	}
	87
	88	/* effects If s = [0-9]*, returns s as an int.
	89	** else returns -1.
	90	*/
	91
	92	int cstring_toPosInt (cstring s)
	93	{
	94	int val = 0;
	95
	96	cstring_chars (s, c)
	97	{
	98	if (isdigit ((unsigned char) c))
	99	{
	100	val = (val * 10) + (int)(c - '0');
	101	}
	102	else
	103	{
	104	return -1;
	105	}
	106	} end_cstring_chars ;
	107
	108	return val;
	109	}
	110
68de3f33	111	cstring cstring_afterChar (cstring s, char c)
	112	{
	113	llassert (cstring_isDefined (s));
	114	return strchr (s, c);
	115	}
	116
616915dd	117	cstring cstring_beforeChar (cstring s, char c)
	118	{
	119	if (cstring_isDefined (s))
	120	{
	121	char *cp = strchr (s, c);
	122
	123	if (cp != NULL)
	124	{
	125	cstring ret;
	126
	127	/@-mods@/
	128	*cp = '\0';
	129	ret = cstring_copy (s);
	130	*cp = c;
	131	/@=mods@/ /* modification is undone */
	132
	133	return ret;
	134	}
	135	}
	136
	137	return cstring_undefined;
	138	}
	139
86d93ed3	140	void cstring_setChar (cstring s, int n, char c) /@requires maxRead(s) >= (n - 1) /\ maxSet(s) >= (n - 1) @/
616915dd	141	{
	142	llassert (cstring_isDefined (s));
	143	llassert (n > 0 && n <= cstring_length (s));
	144
	145	s[n - 1] = c;
	146	}
	147
	148	char cstring_lastChar (cstring s)
	149	{
	150	int length;
	151
	152	llassert (cstring_isDefined (s));
	153
	154	length = cstring_length (s);
	155	llassert (length > 0);
	156
	157	return (s[length - 1]);
	158	}
	159
86d93ed3	160	/@only@/ cstring cstring_copy (cstring s) /@ensures maxSet(result) == maxRead(s) /\ maxRead(result) == maxRead(s) @/
616915dd	161	{
	162	if (cstring_isDefined (s))
	163	{
	164	return (mstring_copy (s));
	165	}
	166	else
	167	{
	168	return cstring_undefined;
	169	}
	170	}
	171
86d93ed3	172	/@only@/ cstring cstring_copyLength (char s, int len) /@requires maxSet(s) >= (len - 1) @*/
616915dd	173	{
	174	char *res = mstring_create (len + 1);
	175
	176	strncpy (res, s, size_fromInt (len));
	177	res[len] = '\0';
	178	return res;
	179	}
	180
	181	bool cstring_containsChar (cstring c, char ch)
	182	{
	183	if (cstring_isDefined (c))
	184	{
	185	return (strchr (c, ch) != NULL);
	186	}
	187	else
	188	{
	189	return FALSE;
	190	}
	191	}
	192
	193	/*
	194	** Replaces all occurances of old in s with new.
	195	*/
	196
616915dd	197	void cstring_replaceAll (cstring s, char old, char snew)
	198	{
	199
	200	llassert (old != snew);
	201
	202	if (cstring_isDefined (s))
	203	{
	204	char *sp = strchr (s, old);
	205
	206	while (sp != NULL)
	207	{
	208	*sp = snew;
	209	sp = strchr (sp, old);
	210	}
	211
	212	}
	213	}
616915dd	214
92b2ba2c	215	void cstring_replaceLit (/@unique@/ cstring s, char old, char snew)
92b2ba2c	216	/@requires maxRead(snew) >= 0 /\ maxRead(old) >= 0 /\ maxRead(old) >= maxRead(snew) @/
616915dd	217	{
616915dd	218	llassert (strlen (old) >= strlen (snew));
92b2ba2c	219
616915dd	220	if (cstring_isDefined (s))
	221	{
	222	char *sp = strstr (s, old);
	223
	224	while (sp != NULL)
	225	{
	226	int lendiff = size_toInt (strlen (old) - strlen (snew));
	227	char *tsnew = snew;
92b2ba2c	228
	229	llassert (lendiff >= 0);
	230
616915dd	231	while (*tsnew != '\0')
616915dd	232	{
92b2ba2c	233	llassert (*sp != '\0');
616915dd	234	sp++ = tsnew++;
616915dd	235	}
92b2ba2c	236
616915dd	237	if (lendiff > 0)
	238	{
	239	while (*(sp + lendiff) != '\0')
	240	{
	241	sp = (sp + lendiff);
	242	sp++;
	243	}
dcdc46c8	244
616915dd	245	*sp = '\0';
	246	}
	247
	248	sp = strstr (s, old);
	249	}
dcdc46c8	250	}
616915dd	251	}
	252
	253	/*
	254	** removes all chars in clist from s
	255	*/
	256
	257	void cstring_stripChars (cstring s, const char *clist)
	258	{
	259	if (cstring_isDefined (s))
	260	{
	261	int i;
	262	int size = cstring_length (s);
	263
	264	for (i = 0; i < size; i++)
	265	{
86d93ed3	266	/drl bee: is/ char c = s[i];
616915dd	267
	268	if (strchr (clist, c) != NULL)
	269	{
	270	/* strip this char */
	271	int j;
	272
	273	size--;
	274
	275	for (j = i; j < size; j++)
	276	{
86d93ed3	277	/drl bee: is/ /drl bee: is/ s[j] = s[j+1];
616915dd	278	}
616915dd	279
86d93ed3	280	/drl bee: is/ s[size] = '\0';
616915dd	281	i--;
	282	}
	283	}
	284	}
	285	}
	286
	287	bool cstring_contains (/@unique@/ cstring c, cstring sub)
	288	{
	289	if (cstring_isDefined (c))
	290	{
	291	llassert (cstring_isDefined (sub));
	292
	293	return (strstr (c, sub) != NULL);
	294	}
	295	else
	296	{
	297	return FALSE;
	298	}
	299	}
	300
	301	static char lookLike (char c) /@/
	302	{
	303	if (c == 'I' \|\| c == 'l')
	304	{
	305	return '1';
	306	}
	307	else if (c == 'O' \|\| c == 'o')
	308	{
	309	return '0';
	310	}
	311	else if (c == 'Z')
	312	{
	313	return '2';
	314	}
	315	else if (c == 'S')
	316	{
	317	return '5';
	318	}
	319	else
	320	{
	321	return c;
	322	}
	323	}
	324
	325	cmpcode cstring_genericEqual (cstring s, cstring t,
	326	int nchars,
	327	bool caseinsensitive,
86d93ed3	328	bool lookalike) /@requires maxRead(s) >= nchars /\ maxRead(t) >= nchars @/
616915dd	329	{
	330	if (s == t) return CGE_SAME;
	331	else if (cstring_isUndefined (s))
	332	{
	333	return cstring_isEmpty (t) ? CGE_SAME : CGE_DISTINCT;
	334	}
	335	else if (cstring_isUndefined (t))
	336	{
	337	return cstring_isEmpty (s) ? CGE_SAME : CGE_DISTINCT;
	338	}
	339	else
	340	{
	341	int i = 0;
	342	bool diffcase = FALSE;
	343	bool difflookalike = FALSE;
	344
	345	while (*s != '\0')
	346	{
	347	if (nchars > 0 && i >= nchars)
	348	{
	349	break;
	350	}
	351
	352	if (t == s)
	353	{
	354	; /* no difference */
	355	}
	356	else if (caseinsensitive
	357	&& (toupper ((int) t) == toupper ((int) s)))
	358	{
	359	diffcase = TRUE;
	360	}
	361	else if (lookalike && (lookLike (t) == lookLike (s)))
	362	{
	363	difflookalike = TRUE;
	364	}
	365	else
	366	{
	367	return CGE_DISTINCT;
	368	}
	369	i++;
	370	s++;
	371	t++;
	372	}
	373
86d93ed3	374	/drl bee: ib/
86d93ed3	375	/drl bee: ib/
616915dd	376	if (s == '\0' && t != '\0')
	377	{
	378	return CGE_DISTINCT;
	379	}
	380
	381	if (diffcase)
	382	{
	383	return CGE_CASE;
	384	}
	385	else if (difflookalike)
	386	{
	387	return CGE_LOOKALIKE;
	388	}
	389	else
	390	{
	391	return CGE_SAME;
	392	}
	393	}
	394	}
	395
	396
	397
	398	bool cstring_equalFree (/@only@/ cstring c1, /@only@/ cstring c2)
	399	{
	400	bool res = cstring_equal (c1, c2);
	401	cstring_free (c1);
	402	cstring_free (c2);
	403	return res;
	404	}
	405
	406	bool cstring_equal (cstring c1, cstring c2)
	407	{
	408	if (c1 == c2) return TRUE;
	409	else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
	410	else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
	411	else return (strcmp (c1, c2) == 0);
	412	}
	413
	414	bool cstring_equalLen (cstring c1, cstring c2, int len)
	415	{
	416	if (c1 == c2) return TRUE;
	417	else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
	418	else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
	419	else return (strncmp (c1, c2, size_fromInt (len)) == 0);
	420	}
	421
	422	bool cstring_equalCaseInsensitive (cstring c1, cstring c2)
	423	{
	424	if (c1 == c2) return TRUE;
	425	else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
	426	else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
	427	else return (cstring_genericEqual (c1, c2, 0, TRUE, FALSE) != CGE_DISTINCT);
	428	}
	429
	430	bool cstring_equalLenCaseInsensitive (cstring c1, cstring c2, int len)
	431	{
	432	llassert (len >= 0);
	433
	434	if (c1 == c2) return TRUE;
	435	else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
	436	else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
	437	else return (cstring_genericEqual (c1, c2, len, TRUE, FALSE) != CGE_DISTINCT);
	438	}
	439
68de3f33	440	bool cstring_equalPrefix (cstring c1, cstring c2)
616915dd	441	{
	442	llassert (c2 != NULL);
	443
	444	if (cstring_isUndefined (c1))
	445	{
	446	return (strlen (c2) == 0);
	447	}
	448
	449	return (strncmp (c1, c2, strlen (c2)) == 0);
	450	}
	451
68de3f33	452	bool cstring_equalPrefixLit (cstring c1, const char *c2)
616915dd	453	{
	454	llassert (c2 != NULL);
	455
	456	if (cstring_isUndefined (c1))
	457	{
	458	return (strlen (c2) == 0);
	459	}
	460
616915dd	461	return (strncmp (c1, c2, strlen (c2)) == 0);
616915dd	462	}
	463
	464	int cstring_xcompare (cstring c1, cstring c2)
	465	{
	466	return (cstring_compare (c1, c2));
	467	}
	468
	469	int cstring_compare (cstring c1, cstring c2)
	470	{
	471	int res;
	472
	473	if (c1 == c2)
	474	{
	475	res = 0;
	476	}
	477	else if (cstring_isUndefined (c1))
	478	{
	479	if (cstring_isEmpty (c2))
	480	{
	481	res = 0;
	482	}
	483	else
	484	{
	485	res = 1;
	486	}
	487	}
	488	else if (cstring_isUndefined (c2))
	489	{
	490	if (cstring_isEmpty (c1))
	491	{
	492	res = 0;
	493	}
	494	else
	495	{
	496	res = -1;
	497	}
	498	}
	499	else
	500	{
	501	res = strcmp (c1, c2);
	502	}
	503
	504	return (res);
	505	}
	506
	507	void cstring_markOwned (/@owned@/ cstring s)
	508	{
	509	sfreeEventually (s);
	510	}
	511
	512	void cstring_free (/@only@/ cstring s)
	513	{
	514	if (cstring_isDefined (s))
	515	{
	516	sfree (s);
	517	}
	518	}
	519
	520	cstring cstring_fromChars (/@exposed@/ const char *cp)
	521	{
	522	return (cstring) cp;
	523	}
	524
	525	/@exposed@/ char *cstring_toCharsSafe (cstring s)
526	{
527	static /@only@/ cstring emptystring = cstring_undefined;
528
529	if (cstring_isDefined (s))
530	{
531	return (char *) s;
532	}
533	else
534	{
535	if (cstring_isUndefined (emptystring))
536	{
537	emptystring = cstring_newEmpty ();
538	}
539
540	return emptystring;
541	}
542	}
543
544	int cstring_length (cstring s)
545	{
546	if (cstring_isDefined (s))
547	{
548	return size_toInt (strlen (s));
549	}
550	return 0;
551	}
552
553	cstring
86d93ed3	554	cstring_capitalize (cstring s) /@requires maxSet(s) >= 0 @/
616915dd	555	{
	556	if (!cstring_isEmpty (s))
	557	{
	558	cstring ret = cstring_copy (s);
	559
	560	cstring_setChar (ret, 1, (char) toupper ((int) cstring_firstChar (ret)));
	561	return ret;
	562	}
	563
	564	return cstring_undefined;
	565	}
	566
	567	cstring
86d93ed3	568	cstring_capitalizeFree (cstring s) /@requires maxSet(s) >= 0 /\ maxRead(s) >= 0 @/
616915dd	569	{
	570	if (!cstring_isEmpty (s))
	571	{
	572	cstring_setChar (s, 1, (char) toupper ((int) cstring_firstChar (s)));
	573	return s;
	574	}
	575
	576	return s;
	577	}
	578
	579	cstring
	580	cstring_clip (cstring s, int len)
	581	{
	582	if (cstring_isUndefined (s) \|\| cstring_length (s) <= len)
	583	{
	584	;
	585	}
	586	else
	587	{
	588	llassert (s != NULL);
86d93ed3	589	/drl bee: mrms/ *(s + len) = '\0';
616915dd	590	}
	591
	592	return s;
	593	}
	594
	595	/@only@/ cstring
	596	cstring_elide (cstring s, int len)
	597	{
	598	if (cstring_isUndefined (s) \|\| cstring_length (s) <= len)
	599	{
	600	return cstring_copy (s);
	601	}
	602	else
	603	{
	604	cstring sc = cstring_create (len);
	605
	606	strncpy (sc, s, size_fromInt (len));
86d93ed3	607	/drl bee: mrms/ *(sc + len - 1) = '\0';
616915dd	608	*(sc + len - 2) = '.';
	609	*(sc + len - 3) = '.';
	610	*(sc + len - 4) = '.';
	611	return sc;
	612	}
	613	}
	614
	615	/@only@/ cstring
86d93ed3	616	cstring_fill (cstring s, int n) /@requires n >= 0 @/
616915dd	617	{
	618	cstring t = cstring_create (n + 1);
	619	cstring ot = t;
	620	int len = cstring_length (s);
	621	int i;
	622
	623	if (len > n)
	624	{
	625	for (i = 0; i < n; i++)
	626	{
86d93ed3	627	/drl bee: is/
86d93ed3	628	/drl bee: is/
616915dd	629	t++ = s++;
	630	}
	631	*t = '\0';
	632	}
	633	else
	634	{
	635	for (i = 0; i < len; i++)
	636	{
86d93ed3	637	/drl bee: is/
86d93ed3	638	/drl bee: is/
616915dd	639	t++ = s++;
	640	}
	641	for (i = 0; i < n - len; i++)
	642	{
86d93ed3	643	/drl bee: is/
616915dd	644	*t++ = ' ';
	645	}
	646	*t = '\0';
	647	}
	648
	649	return ot;
	650	}
	651
	652	cstring
	653	cstring_downcase (cstring s)
	654	{
	655	if (cstring_isDefined (s))
	656	{
	657	cstring t = cstring_create (strlen (s) + 1);
	658	cstring ot = t;
	659	char c;
	660
86d93ed3	661	/drl bee: lhnt/ while ((c = *s) != '\0')
616915dd	662	{
	663	if (c >= 'A' && c <= 'Z')
	664	{
	665	c = c - 'A' + 'a';
	666	}
	667	*t++ = c;
	668	s++;
	669	}
86d93ed3	670	/drl bee: is/ *t = '\0';
616915dd	671
	672	return ot;
	673	}
	674	else
	675	{
	676	return cstring_undefined;
	677	}
	678	}
	679
	680	/@notnull@/ cstring
	681	cstring_appendChar (/@only@/ cstring s1, char c)
	682	{
	683	int l = cstring_length (s1);
	684	char *s;
	685
	686	s = (char ) dmalloc (sizeof (s) * (l + 2));
	687
	688	if (cstring_isDefined (s1))
	689	{
	690	strcpy (s, s1);
	691	*(s + l) = c;
86d93ed3	692	/drl bee: dm/ *(s + l + 1) = '\0';
616915dd	693	sfree (s1);
	694	}
	695	else
	696	{
	697	*(s) = c;
4dd72714	698	/drl bee: dm/ *(s + 1) = '\0';
616915dd	699	}
	700
	701	return s;
	702	}
	703
	704	/@only@/ cstring
	705	cstring_concatFree (cstring s, cstring t)
	706	{
	707	cstring res = cstring_concat (s, t);
	708	cstring_free (s);
	709	cstring_free (t);
	710	return res;
	711	}
	712
	713	/@only@/ cstring
	714	cstring_concatFree1 (cstring s, cstring t)
	715	{
	716	cstring res = cstring_concat (s, t);
	717	cstring_free (s);
	718	return res;
	719	}
	720
	721	# ifndef NOLCL
	722	/@only@/ cstring
	723	cstring_concatChars (cstring s, char *t)
	724	{
	725	cstring res = cstring_concat (s, cstring_fromChars (t));
	726	cstring_free (s);
	727	return res;
	728	}
	729	# endif
	730
	731	/@only@/ cstring
86d93ed3	732	cstring_concatLength (cstring s1, char s2, int len) /@requires maxSet(s2) >= (len - 1) @*/
616915dd	733	{
	734	cstring tmp = cstring_copyLength (s2, len);
	735	cstring res = cstring_concat (s1, tmp);
	736	cstring_free (tmp);
	737	cstring_free (s1);
	738
	739	return res;
	740	}
	741
	742	/@only@/ cstring
86d93ed3	743	cstring_concat (cstring s, cstring t) /@requires maxSet(s) >= 0 @/
616915dd	744	{
	745	char *ret = mstring_create (cstring_length (s) + cstring_length (t));
	746
	747	if (cstring_isDefined (s))
	748	{
86d93ed3	749	/drl bee: sl/ strcpy (ret, s);
616915dd	750	}
	751	if (cstring_isDefined (t))
	752	{
	753	strcat (ret, t);
	754	}
	755
	756	return ret;
	757	}
	758
	759	/@notnull@/ /@only@/ cstring
	760	cstring_prependCharO (char c, /@only@/ cstring s1)
	761	{
	762	cstring res = cstring_prependChar (c, s1);
	763
	764	cstring_free (s1);
	765	return (res);
	766	}
	767
	768	/@notnull@/ /@only@/ cstring
	769	cstring_prependChar (char c, /@temp@/ cstring s1)
	770	{
	771	int l = cstring_length (s1);
	772	char s = (char ) dmalloc (sizeof (s) (l + 2));
	773
86d93ed3	774	/drl bee: dm/ *(s) = c;
616915dd	775
	776	if (cstring_isDefined (s1))
	777	{
	778	/@-mayaliasunique@/
	779	strcpy (s + 1, s1);
	780	/@=mayaliasunique@/
	781	}
	782
86d93ed3	783	/drl bee: dm/ *(s + l + 1) = '\0';
616915dd	784	return s;
	785	}
	786
	787	# ifndef NOLCL
	788	bool
	789	cstring_hasNonAlphaNumBar (cstring s)
	790	{
	791	int c;
	792
	793	if (cstring_isUndefined (s)) return FALSE;
	794
86d93ed3	795	/drl bee: lhnt/ while ((c = (int) *s) != (int) '\0')
616915dd	796	{
	797	if ((isalnum (c) == 0) && (c != (int) '_')
	798	&& (c != (int) '.') && (c != (int) CONNECTCHAR))
	799	{
	800	return TRUE;
	801	}
	802
	803	s++;
	804	}
	805	return FALSE;
	806	}
	807	# endif
	808
	809	/@only@/ /@notnull@/ cstring
	810	cstring_create (int n)
	811	{
	812	char s = dmalloc (sizeof (s) * (n + 1));
	813
86d93ed3	814	/drl bee: dm/ *s = '\0';
616915dd	815	return s;
	816	}
	817
2934b455	818	/@only@/ /@notnull@/ cstring
	819	cstring_copySegment (cstring s, int findex, int tindex)
	820	{
	821	cstring res = cstring_create (tindex - findex + 1);
	822
	823	llassert (cstring_isDefined (s));
	824	llassert (cstring_length (s) > tindex);
	825
	826	strncpy (res, (s + findex), size_fromInt ((tindex - findex + 1)));
	827	return res;
	828	}
	829
616915dd	830	# ifndef NOLCL
	831	lsymbol cstring_toSymbol (cstring s)
	832	{
2934b455	833	lsymbol res = lsymbol_fromString (s);
616915dd	834
	835	cstring_free (s);
	836	return res;
	837	}
	838	# endif
	839
	840	cstring cstring_bsearch (cstring key, char **table, int nentries)
	841	{
	842	if (cstring_isDefined (key))
	843	{
	844	int low = 0;
	845	int high = nentries;
	846	int mid = (high + low + 1) / 2;
	847	int last = -1;
	848	cstring res = cstring_undefined;
	849
	850	while (low <= high && mid < nentries)
	851	{
	852	int cmp;
	853
	854	llassert (mid != last);
	855	llassert (mid >= 0 && mid < nentries);
	856
	857	cmp = cstring_compare (key, table[mid]);
	858
	859	if (cmp == 0)
	860	{
	861	res = table[mid];
	862	break;
	863	}
	864	else if (cmp < 0) /* key is before table[mid] */
	865	{
	866	high = mid - 1;
	867	}
	868	else /* key of after table[mid] */
	869	{
	870	low = mid + 1;
	871	}
	872
	873	last = mid;
	874	mid = (high + low + 1) / 2;
	875	}
	876
	877	if (mid != 0 && mid < nentries - 1)
	878	{
	879	llassert (cstring_compare (key, table[mid - 1]) > 0);
86d93ed3	880	/drl bee: ndv/ llassert (cstring_compare (key, table[mid + 1]) < 0);
616915dd	881	}
	882
	883	return res;
	884	}
	885
	886	return cstring_undefined;
	887	}
	888
	889	extern /@observer@/ cstring cstring_advanceWhiteSpace (cstring s)
	890	{
	891	if (cstring_isDefined (s)) {
	892	char *t = s;
	893
86d93ed3	894	/drl bee: lhnt/ while (t != '\0' && isspace ((int) t)) {
616915dd	895	t++;
	896	}
	897
	898	return t;
	899	}
	900
	901	return cstring_undefined;
	902	}
	903
	904
	905