/* ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003. ** See ../LICENSE for license information. ** */ /* ** mstring.h */ # ifndef MSTRING_H # define MSTRING_H /* mstring is a non-abstract string (char *) */ typedef /*@concrete@*/ char *mstring; typedef /*@observer@*/ char *ob_mstring; typedef /*@observer@*/ /*@null@*/ char *bn_mstring; extern /*@unused@*/ /*@notnull@*/ /*@observer@*/ char * mstring_safePrint (/*@returned@*/ /*@null@*/ mstring p_s) /*@*/ ; extern char *mstring_spaces (int p_n) /*@*/ ; extern char *mstring_concat (const char *p_s1, const char *p_s2) /*@*/ ; extern char *mstring_concatFree (/*@only@*/ char *p_s1, /*@only@*/ char *p_s2) /*@modifies *p_s1, *p_s2*/ ; extern char *mstring_concatFree1 (/*@only@*/ char *p_s1, const char *p_s2); extern char *mstring_append (/*@only@*/ char *p_s1, char p_c); extern char *mstring_copy (/*@null@*/ char *p_s1) /*@*/ /*@ensures maxRead(result) == maxRead(p_s1) /\ maxSet(result) == maxSet(p_s1) @*/ ; extern bool mstring_equalPrefix (const char *p_c1, const char *p_c2) /*@*/ ; extern bool mstring_equal (/*@null@*/ const char *p_s1, /*@null@*/ const char *p_s2) /*@*/ ; extern bool mstring_containsChar (/*@unique@*/ const char *p_s, char p_c) /*@*/ ; extern bool mstring_containsString (/*@unique@*/ const char *p_s, /*@unique@*/ const char *p_c) /*@*/ ; extern size_t mstring_length (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ; # define mstring_length(s) \ (((s) != NULL) ? strlen (s) : 0) extern /*@falsewhennull@*/ bool mstring_isDefined (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ; # define mstring_isDefined(s) ((s) != NULL) extern /*@nullwhentrue@*/ bool mstring_isEmpty (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ; # define mstring_isEmpty(s) (mstring_length(s) == 0) extern void mstring_markFree (/*@owned@*/ char *p_s) /*@modifies *p_s;@*/ ; extern /*@notnull@*/ /*@only@*/ char *mstring_create (size_t p_n) /*@*/ /*@ensures maxSet(result) == p_n /\ maxRead(result) == 0 @*/ ; extern /*@notnull@*/ /*@only@*/ char *mstring_createEmpty (void) /*@*/ ; extern void mstring_free (/*@out@*/ /*@only@*/ /*@null@*/ char *p_s); # define mstring_free(s) sfree(s) # define mstring_createEmpty() mstring_create(0) # else # error "Multiple include" # endif