src/Headers/mstring.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
   3 ** See ../LICENSE for license information.
   4 **
   5 */
   6 /*
   7 ** mstring.h
   8 */
   9
  10 # ifndef MSTRING_H
  11 # define MSTRING_H
  12
  13 /* mstring is a non-abstract string (char *) */
  14
  15 typedef /*@concrete@*/ char *mstring;
  16 typedef /*@observer@*/ char *ob_mstring;
  17 typedef /*@observer@*/ /*@null@*/ char *bn_mstring;
  18
  19 extern /*@unused@*/ /*@notnull@*/ /*@observer@*/ char *
  20   mstring_safePrint (/*@returned@*/ /*@null@*/ mstring p_s) /*@*/ ;
  21 extern char *mstring_spaces (int p_n) /*@*/ ;
  22 extern char *mstring_concat  (const char *p_s1, const char *p_s2) /*@*/ ;
  23 extern char *mstring_concatFree (/*@only@*/ char *p_s1, /*@only@*/ char *p_s2) /*@modifies *p_s1, *p_s2*/ ;
  24 extern char *mstring_concatFree1 (/*@only@*/ char *p_s1, const char *p_s2);
  25 extern char *mstring_append (/*@only@*/ char *p_s1, char p_c);
  26 extern char *mstring_copy (/*@null@*/ char *p_s1) /*@*/  /*@ensures maxRead(result) == maxRead(p_s1) /\  maxSet(result) == maxSet(p_s1) @*/ ;
  27 extern bool mstring_equalPrefix (const char *p_c1, const char *p_c2) /*@*/ ;
  28 extern bool mstring_equal (/*@null@*/ const char *p_s1, /*@null@*/ const char *p_s2) /*@*/ ;
  29 extern bool mstring_containsChar (/*@unique@*/ const char *p_s, char p_c) /*@*/ ;
  30 extern bool mstring_containsString (/*@unique@*/ const char *p_s, /*@unique@*/ const char *p_c) /*@*/ ;
  31
  32 extern size_t mstring_length (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ;
  33 # define mstring_length(s) \
  34   (((s) != NULL) ? strlen (s) : 0)
  35
  36 extern /*@falsewhennull@*/ bool mstring_isDefined (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ;
  37 # define mstring_isDefined(s) ((s) != NULL)
  38
  39 extern /*@nullwhentrue@*/ bool mstring_isEmpty (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ;
  40 # define mstring_isEmpty(s) (mstring_length(s) == 0)
  41
  42 extern void mstring_markFree (/*@owned@*/ char *p_s) /*@modifies *p_s;@*/ ;
  43
  44 extern /*@notnull@*/ /*@only@*/ char *mstring_create (size_t p_n)
  45    /*@*/
  46    /*@ensures maxSet(result) == p_n /\ maxRead(result) == 0 @*/ ;
  47
  48 extern /*@notnull@*/ /*@only@*/ char *mstring_createEmpty (void) /*@*/ ;
  49
  50 extern void mstring_free (/*@out@*/ /*@only@*/ /*@null@*/ char *p_s);
  51 # define mstring_free(s) sfree(s)
  52
  53 # define mstring_createEmpty() mstring_create(0)
  54
  55 # else
  56 # error "Multiple include"
  57 # endif
  58
  59
  60
  61
  62