void fprint_sb(FILE *fp, String_buf sb);This routine prints String_buf sb to FILE *fp.
void fprint_strbuf_mem(FILE *fp, BOOL heading);This routine prints (to FILE *fp) memory usage statistics for data types associated with the strbuf package. The Boolean argument heading tells whether to print a heading on the table.
String_buf get_string_buf(void);
String_buf init_string_buf(char *s);This routine allocates and returns a String_buf, initialized to string s. Don't forget to call zap_string_buf(sb) when finished with it. Also see get_string_buf().
void p_sb(String_buf sb);This routine prints String_buf sb, followed by '\n' and fflush, to stdout. If you don't want the newline, use fprint_sb() instead.
void p_strbuf_mem();This routine prints (to stdout) memory usage statistics for data types associated with the strbuf package.
void sb_append(String_buf sb, char *s);This routine appends string s to String_buf sb. The NULL character that marks the end of s does not go into the String_buf.
void sb_append_char(String_buf sb, char c);This routine appends character c to String_buf sb.
void sb_append_int(String_buf sb, int i);Convert an integer to a string and append the string to a String_buf.
void sb_cat(String_buf sb1, String_buf sb2);This routine appends a copy of sb2 to sb1, then deallocates sb2. Do not refer to sb2 after calling this rouine because it won't exist. You can use sb_cat_copy() instead if you need to save sb2.
void sb_cat_copy(String_buf sb1, String_buf sb2);This routine appends a copy of sb2 to sb1. String_buf sb2 is not changed. You can use sb_cat() instead if you won't be needing sb2.
char sb_char(String_buf sb, int n);This routine returns the n-th character (counting from 0) of String_buf sb. If index n is out of range, the NULL character '\0' is returned.
void sb_replace_char(String_buf sb, int i, char c);This routine replaces a character in a String_buf. If the index i is out of range, nothing happens.
int sb_size(String_buf sb);
char *sb_to_malloc_char_array(String_buf sb);This routine is similar to sb_to_malloc_string(), except that null characters are copied to the new string.
char *sb_to_malloc_string(String_buf sb);This routine returns a new, ordinary C string corresponding to the String_buf argument sb. WARNING: the new string, say s, is dynamically allocated (malloced), so don't forget to call free(s) when you are finished with the string. (This routine is not intended for printing String_bufs; use fprint_sb() instead.)
String_bufs do not have a NULL character marking the end; instead, they keep a count of the number of characters.
If the String_buf contains NULL characters, they do NOT mark the end of the string. Instead, they are simply ignored when constructing the ordinary string.
void zap_string_buf(String_buf sb);This routine deallocates a String_buf and frees all memory associated with it.
typedef struct string_buf * String_buf;
This is similar to the StringBuffer class in Java, and the cstrings of our old theorem prover LMA/ITP. We didn't have anything like this in Otter, but there were times when I wish we had, so here it is.