[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;
	  
	  while (*tsnew != '\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
86d93ed3	215	void cstring_replaceLit (/@unique@/ cstring s, char old, char snew) /@requires maxRead(snew) >= 0 /\ maxRead(old) >= 0 /\ maxRead(old) >= maxRead(snew) @/
616915dd	216	{
	217
	218	llassert (strlen (old) >= strlen (snew));
	219
	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;
	228
	229	while (*tsnew != '\0')
	230	{
	231	sp++ = tsnew++;
	232	}
	233
	234	if (lendiff > 0)
	235	{
	236	while (*(sp + lendiff) != '\0')
	237	{
	238	sp = (sp + lendiff);
	239	sp++;
	240	}
dcdc46c8	241
616915dd	242	*sp = '\0';
	243	}
	244
	245	sp = strstr (s, old);
	246	}
dcdc46c8	247	}
616915dd	248	}
	249
	250	/*
	251	** removes all chars in clist from s
	252	*/
	253
	254	void cstring_stripChars (cstring s, const char *clist)
	255	{
	256	if (cstring_isDefined (s))
	257	{
	258	int i;
	259	int size = cstring_length (s);
	260
	261	for (i = 0; i < size; i++)
	262	{
86d93ed3	263	/drl bee: is/ char c = s[i];
616915dd	264
	265	if (strchr (clist, c) != NULL)
	266	{
	267	/* strip this char */
	268	int j;
	269
	270	size--;
	271
	272	for (j = i; j < size; j++)
	273	{
86d93ed3	274	/drl bee: is/ /drl bee: is/ s[j] = s[j+1];
616915dd	275	}
616915dd	276
86d93ed3	277	/drl bee: is/ s[size] = '\0';
616915dd	278	i--;
	279	}
	280	}
	281	}
	282	}
	283
	284	bool cstring_contains (/@unique@/ cstring c, cstring sub)
	285	{
	286	if (cstring_isDefined (c))
	287	{
	288	llassert (cstring_isDefined (sub));
	289
	290	return (strstr (c, sub) != NULL);
	291	}
	292	else
	293	{
	294	return FALSE;
	295	}
	296	}
	297
	298	static char lookLike (char c) /@/
	299	{
	300	if (c == 'I' \|\| c == 'l')
	301	{
	302	return '1';
	303	}
	304	else if (c == 'O' \|\| c == 'o')
	305	{
	306	return '0';
	307	}
	308	else if (c == 'Z')
	309	{
	310	return '2';
	311	}
	312	else if (c == 'S')
	313	{
	314	return '5';
	315	}
	316	else
	317	{
	318	return c;
	319	}
	320	}
	321
	322	cmpcode cstring_genericEqual (cstring s, cstring t,
	323	int nchars,
	324	bool caseinsensitive,
86d93ed3	325	bool lookalike) /@requires maxRead(s) >= nchars /\ maxRead(t) >= nchars @/
616915dd	326	{
	327	if (s == t) return CGE_SAME;
	328	else if (cstring_isUndefined (s))
	329	{
	330	return cstring_isEmpty (t) ? CGE_SAME : CGE_DISTINCT;
	331	}
	332	else if (cstring_isUndefined (t))
	333	{
	334	return cstring_isEmpty (s) ? CGE_SAME : CGE_DISTINCT;
	335	}
	336	else
	337	{
	338	int i = 0;
	339	bool diffcase = FALSE;
	340	bool difflookalike = FALSE;
	341
	342	while (*s != '\0')
	343	{
	344	if (nchars > 0 && i >= nchars)
	345	{
	346	break;
	347	}
	348
	349	if (t == s)
	350	{
	351	; /* no difference */
	352	}
	353	else if (caseinsensitive
	354	&& (toupper ((int) t) == toupper ((int) s)))
	355	{
	356	diffcase = TRUE;
	357	}
	358	else if (lookalike && (lookLike (t) == lookLike (s)))
	359	{
	360	difflookalike = TRUE;
	361	}
	362	else
	363	{
	364	return CGE_DISTINCT;
	365	}
	366	i++;
	367	s++;
	368	t++;
	369	}
	370
86d93ed3	371	/drl bee: ib/
86d93ed3	372	/drl bee: ib/
616915dd	373	if (s == '\0' && t != '\0')
	374	{
	375	return CGE_DISTINCT;
	376	}
	377
	378	if (diffcase)
	379	{
	380	return CGE_CASE;
	381	}
	382	else if (difflookalike)
	383	{
	384	return CGE_LOOKALIKE;
	385	}
	386	else
	387	{
	388	return CGE_SAME;
	389	}
	390	}
	391	}
	392
	393
	394
	395	bool cstring_equalFree (/@only@/ cstring c1, /@only@/ cstring c2)
	396	{
	397	bool res = cstring_equal (c1, c2);
	398	cstring_free (c1);
	399	cstring_free (c2);
	400	return res;
	401	}
	402
	403	bool cstring_equal (cstring c1, cstring c2)
	404	{
	405	if (c1 == c2) return TRUE;
	406	else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
	407	else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
	408	else return (strcmp (c1, c2) == 0);
	409	}
	410
	411	bool cstring_equalLen (cstring c1, cstring c2, int len)
	412	{
	413	if (c1 == c2) return TRUE;
	414	else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
	415	else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
	416	else return (strncmp (c1, c2, size_fromInt (len)) == 0);
	417	}
	418
	419	bool cstring_equalCaseInsensitive (cstring c1, cstring c2)
	420	{
	421	if (c1 == c2) return TRUE;
	422	else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
	423	else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
	424	else return (cstring_genericEqual (c1, c2, 0, TRUE, FALSE) != CGE_DISTINCT);
	425	}
	426
	427	bool cstring_equalLenCaseInsensitive (cstring c1, cstring c2, int len)
	428	{
	429	llassert (len >= 0);
	430
	431	if (c1 == c2) return TRUE;
	432	else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
	433	else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
	434	else return (cstring_genericEqual (c1, c2, len, TRUE, FALSE) != CGE_DISTINCT);
	435	}
	436
68de3f33	437	bool cstring_equalPrefix (cstring c1, cstring c2)
616915dd	438	{
	439	llassert (c2 != NULL);
	440
	441	if (cstring_isUndefined (c1))
	442	{
	443	return (strlen (c2) == 0);
	444	}
	445
	446	return (strncmp (c1, c2, strlen (c2)) == 0);
	447	}
	448
68de3f33	449	bool cstring_equalPrefixLit (cstring c1, const char *c2)
616915dd	450	{
	451	llassert (c2 != NULL);
	452
	453	if (cstring_isUndefined (c1))
	454	{
	455	return (strlen (c2) == 0);
	456	}
	457
616915dd	458	return (strncmp (c1, c2, strlen (c2)) == 0);
616915dd	459	}
	460
	461	int cstring_xcompare (cstring c1, cstring c2)
	462	{
	463	return (cstring_compare (c1, c2));
	464	}
	465
	466	int cstring_compare (cstring c1, cstring c2)
	467	{
	468	int res;
	469
	470	if (c1 == c2)
	471	{
	472	res = 0;
	473	}
	474	else if (cstring_isUndefined (c1))
	475	{
	476	if (cstring_isEmpty (c2))
	477	{
	478	res = 0;
	479	}
	480	else
	481	{
	482	res = 1;
	483	}
	484	}
	485	else if (cstring_isUndefined (c2))
	486	{
	487	if (cstring_isEmpty (c1))
	488	{
	489	res = 0;
	490	}
	491	else
	492	{
	493	res = -1;
	494	}
	495	}
	496	else
	497	{
	498	res = strcmp (c1, c2);
	499	}
	500
	501	return (res);
	502	}
	503
	504	void cstring_markOwned (/@owned@/ cstring s)
	505	{
	506	sfreeEventually (s);
	507	}
	508
	509	void cstring_free (/@only@/ cstring s)
	510	{
	511	if (cstring_isDefined (s))
	512	{
	513	sfree (s);
	514	}
	515	}
	516
	517	cstring cstring_fromChars (/@exposed@/ const char *cp)
	518	{
	519	return (cstring) cp;
	520	}
	521
	522	/@exposed@/ char *cstring_toCharsSafe (cstring s)
523	{
524	static /@only@/ cstring emptystring = cstring_undefined;
525
526	if (cstring_isDefined (s))
527	{
528	return (char *) s;
529	}
530	else
531	{
532	if (cstring_isUndefined (emptystring))
533	{
534	emptystring = cstring_newEmpty ();
535	}
536
537	return emptystring;
538	}
539	}
540
541	int cstring_length (cstring s)
542	{
543	if (cstring_isDefined (s))
544	{
545	return size_toInt (strlen (s));
546	}
547	return 0;
548	}
549
550	cstring
86d93ed3	551	cstring_capitalize (cstring s) /@requires maxSet(s) >= 0 @/
616915dd	552	{
	553	if (!cstring_isEmpty (s))
	554	{
	555	cstring ret = cstring_copy (s);
	556
	557	cstring_setChar (ret, 1, (char) toupper ((int) cstring_firstChar (ret)));
	558	return ret;
	559	}
	560
	561	return cstring_undefined;
	562	}
	563
	564	cstring
86d93ed3	565	cstring_capitalizeFree (cstring s) /@requires maxSet(s) >= 0 /\ maxRead(s) >= 0 @/
616915dd	566	{
	567	if (!cstring_isEmpty (s))
	568	{
	569	cstring_setChar (s, 1, (char) toupper ((int) cstring_firstChar (s)));
	570	return s;
	571	}
	572
	573	return s;
	574	}
	575
	576	cstring
	577	cstring_clip (cstring s, int len)
	578	{
	579	if (cstring_isUndefined (s) \|\| cstring_length (s) <= len)
	580	{
	581	;
	582	}
	583	else
	584	{
	585	llassert (s != NULL);
86d93ed3	586	/drl bee: mrms/ *(s + len) = '\0';
616915dd	587	}
	588
	589	return s;
	590	}
	591
	592	/@only@/ cstring
	593	cstring_elide (cstring s, int len)
	594	{
	595	if (cstring_isUndefined (s) \|\| cstring_length (s) <= len)
	596	{
	597	return cstring_copy (s);
	598	}
	599	else
	600	{
	601	cstring sc = cstring_create (len);
	602
	603	strncpy (sc, s, size_fromInt (len));
86d93ed3	604	/drl bee: mrms/ *(sc + len - 1) = '\0';
616915dd	605	*(sc + len - 2) = '.';
	606	*(sc + len - 3) = '.';
	607	*(sc + len - 4) = '.';
	608	return sc;
	609	}
	610	}
	611
	612	/@only@/ cstring
86d93ed3	613	cstring_fill (cstring s, int n) /@requires n >= 0 @/
616915dd	614	{
	615	cstring t = cstring_create (n + 1);
	616	cstring ot = t;
	617	int len = cstring_length (s);
	618	int i;
	619
	620	if (len > n)
	621	{
	622	for (i = 0; i < n; i++)
	623	{
86d93ed3	624	/drl bee: is/
86d93ed3	625	/drl bee: is/
616915dd	626	t++ = s++;
	627	}
	628	*t = '\0';
	629	}
	630	else
	631	{
	632	for (i = 0; i < len; i++)
	633	{
86d93ed3	634	/drl bee: is/
86d93ed3	635	/drl bee: is/
616915dd	636	t++ = s++;
	637	}
	638	for (i = 0; i < n - len; i++)
	639	{
86d93ed3	640	/drl bee: is/
616915dd	641	*t++ = ' ';
	642	}
	643	*t = '\0';
	644	}
	645
	646	return ot;
	647	}
	648
	649	cstring
	650	cstring_downcase (cstring s)
	651	{
	652	if (cstring_isDefined (s))
	653	{
	654	cstring t = cstring_create (strlen (s) + 1);
	655	cstring ot = t;
	656	char c;
	657
86d93ed3	658	/drl bee: lhnt/ while ((c = *s) != '\0')
616915dd	659	{
	660	if (c >= 'A' && c <= 'Z')
	661	{
	662	c = c - 'A' + 'a';
	663	}
	664	*t++ = c;
	665	s++;
	666	}
86d93ed3	667	/drl bee: is/ *t = '\0';
616915dd	668
	669	return ot;
	670	}
	671	else
	672	{
	673	return cstring_undefined;
	674	}
	675	}
	676
	677	/@notnull@/ cstring
	678	cstring_appendChar (/@only@/ cstring s1, char c)
	679	{
	680	int l = cstring_length (s1);
	681	char *s;
	682
	683	s = (char ) dmalloc (sizeof (s) * (l + 2));
	684
	685	if (cstring_isDefined (s1))
	686	{
	687	strcpy (s, s1);
	688	*(s + l) = c;
86d93ed3	689	/drl bee: dm/ *(s + l + 1) = '\0';
616915dd	690	sfree (s1);
	691	}
	692	else
	693	{
	694	*(s) = c;
4dd72714	695	/drl bee: dm/ *(s + 1) = '\0';
616915dd	696	}
	697
	698	return s;
	699	}
	700
	701	/@only@/ cstring
	702	cstring_concatFree (cstring s, cstring t)
	703	{
	704	cstring res = cstring_concat (s, t);
	705	cstring_free (s);
	706	cstring_free (t);
	707	return res;
	708	}
	709
	710	/@only@/ cstring
	711	cstring_concatFree1 (cstring s, cstring t)
	712	{
	713	cstring res = cstring_concat (s, t);
	714	cstring_free (s);
	715	return res;
	716	}
	717
	718	# ifndef NOLCL
	719	/@only@/ cstring
	720	cstring_concatChars (cstring s, char *t)
	721	{
	722	cstring res = cstring_concat (s, cstring_fromChars (t));
	723	cstring_free (s);
	724	return res;
	725	}
	726	# endif
	727
	728	/@only@/ cstring
86d93ed3	729	cstring_concatLength (cstring s1, char s2, int len) /@requires maxSet(s2) >= (len - 1) @*/
616915dd	730	{
	731	cstring tmp = cstring_copyLength (s2, len);
	732	cstring res = cstring_concat (s1, tmp);
	733	cstring_free (tmp);
	734	cstring_free (s1);
	735
	736	return res;
	737	}
	738
	739	/@only@/ cstring
86d93ed3	740	cstring_concat (cstring s, cstring t) /@requires maxSet(s) >= 0 @/
616915dd	741	{
	742	char *ret = mstring_create (cstring_length (s) + cstring_length (t));
	743
	744	if (cstring_isDefined (s))
	745	{
86d93ed3	746	/drl bee: sl/ strcpy (ret, s);
616915dd	747	}
	748	if (cstring_isDefined (t))
	749	{
	750	strcat (ret, t);
	751	}
	752
	753	return ret;
	754	}
	755
	756	/@notnull@/ /@only@/ cstring
	757	cstring_prependCharO (char c, /@only@/ cstring s1)
	758	{
	759	cstring res = cstring_prependChar (c, s1);
	760
	761	cstring_free (s1);
	762	return (res);
	763	}
	764
	765	/@notnull@/ /@only@/ cstring
	766	cstring_prependChar (char c, /@temp@/ cstring s1)
	767	{
	768	int l = cstring_length (s1);
	769	char s = (char ) dmalloc (sizeof (s) (l + 2));
	770
86d93ed3	771	/drl bee: dm/ *(s) = c;
616915dd	772
	773	if (cstring_isDefined (s1))
	774	{
	775	/@-mayaliasunique@/
	776	strcpy (s + 1, s1);
	777	/@=mayaliasunique@/
	778	}
	779
86d93ed3	780	/drl bee: dm/ *(s + l + 1) = '\0';
616915dd	781	return s;
	782	}
	783
	784	# ifndef NOLCL
	785	bool
	786	cstring_hasNonAlphaNumBar (cstring s)
	787	{
	788	int c;
	789
	790	if (cstring_isUndefined (s)) return FALSE;
	791
86d93ed3	792	/drl bee: lhnt/ while ((c = (int) *s) != (int) '\0')
616915dd	793	{
	794	if ((isalnum (c) == 0) && (c != (int) '_')
	795	&& (c != (int) '.') && (c != (int) CONNECTCHAR))
	796	{
	797	return TRUE;
	798	}
	799
	800	s++;
	801	}
	802	return FALSE;
	803	}
	804	# endif
	805
	806	/@only@/ /@notnull@/ cstring
	807	cstring_create (int n)
	808	{
	809	char s = dmalloc (sizeof (s) * (n + 1));
	810
86d93ed3	811	/drl bee: dm/ *s = '\0';
616915dd	812	return s;
	813	}
	814
2934b455	815	/@only@/ /@notnull@/ cstring
	816	cstring_copySegment (cstring s, int findex, int tindex)
	817	{
	818	cstring res = cstring_create (tindex - findex + 1);
	819
	820	llassert (cstring_isDefined (s));
	821	llassert (cstring_length (s) > tindex);
	822
	823	strncpy (res, (s + findex), size_fromInt ((tindex - findex + 1)));
	824	return res;
	825	}
	826
616915dd	827	# ifndef NOLCL
	828	lsymbol cstring_toSymbol (cstring s)
	829	{
2934b455	830	lsymbol res = lsymbol_fromString (s);
616915dd	831
	832	cstring_free (s);
	833	return res;
	834	}
	835	# endif
	836
	837	cstring cstring_bsearch (cstring key, char **table, int nentries)
	838	{
	839	if (cstring_isDefined (key))
	840	{
	841	int low = 0;
	842	int high = nentries;
	843	int mid = (high + low + 1) / 2;
	844	int last = -1;
	845	cstring res = cstring_undefined;
	846
	847	while (low <= high && mid < nentries)
	848	{
	849	int cmp;
	850
	851	llassert (mid != last);
	852	llassert (mid >= 0 && mid < nentries);
	853
	854	cmp = cstring_compare (key, table[mid]);
	855
	856	if (cmp == 0)
	857	{
	858	res = table[mid];
	859	break;
	860	}
	861	else if (cmp < 0) /* key is before table[mid] */
	862	{
	863	high = mid - 1;
	864	}
	865	else /* key of after table[mid] */
	866	{
	867	low = mid + 1;
	868	}
	869
	870	last = mid;
	871	mid = (high + low + 1) / 2;
	872	}
	873
	874	if (mid != 0 && mid < nentries - 1)
	875	{
	876	llassert (cstring_compare (key, table[mid - 1]) > 0);
86d93ed3	877	/drl bee: ndv/ llassert (cstring_compare (key, table[mid + 1]) < 0);
616915dd	878	}
	879
	880	return res;
	881	}
	882
	883	return cstring_undefined;
	884	}
	885
	886	extern /@observer@/ cstring cstring_advanceWhiteSpace (cstring s)
	887	{
	888	if (cstring_isDefined (s)) {
	889	char *t = s;
	890
86d93ed3	891	/drl bee: lhnt/ while (t != '\0' && isspace ((int) t)) {
616915dd	892	t++;
	893	}
	894
	895	return t;
	896	}
	897
	898	return cstring_undefined;
	899	}
	900
	901
	902