Fixed all /*@i...@*/ tags (except 1).

[splint.git] / src / Headers / misc.h

diff --git a/src/Headers/misc.h b/src/Headers/misc.h
index f31abd7297a0a48e2bc8e57d6de605b631c15e63..3afd2b4c319b03b3f99c4f1e304a86cd82c9672e 100644 (file)
--- a/src/Headers/misc.h
+++ b/src/Headers/misc.h
@@ -1,5 +1,5 @@
 /*
-** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
+** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
 ** See ../LICENSE for license information.
 **
 */
@@ -12,9 +12,7 @@
 # ifndef MISC_H
 # define MISC_H
 
-# ifndef NOLCL
 # include "lclMisc.h"
-# endif
 
 extern void assertSet (/*@special@*/ /*@sef@*/ /*@unused@*/ void *p_x) 
    /*@sets p_x, *p_x@*/ ;
@@ -25,52 +23,17 @@ extern void assertDefined (/*@sef@*/ /*@unused@*/ void *p_x) ;
 
 
 /*@-czechfcns@*/
-extern int size_toInt (size_t p_x) /*@*/ /*@ensures result==p_x@*/;
-extern long size_toLong (size_t p_x) /*@*/ /*@ensures result==p_x@*/ ;
-extern size_t size_fromInt (int p_x) /*@*/ /*@ensures result==p_x@*/ ;
-extern int longUnsigned_toInt (long unsigned int p_x) /*@*/ /*@ensures result==p_x@*/ ;
-extern int long_toInt (long p_x) /*@*/ /*@ensures result==p_x@*/;
-extern long unsigned longUnsigned_fromInt (int p_x) /*@*/  /*@ensures result==p_x@*/ ;
+extern int size_toInt (size_t p_x) /*@*/ /*@ensures result == p_x@*/;
+extern long size_toLong (size_t p_x) /*@*/ /*@ensures result == p_x@*/ ;
+extern size_t size_fromInt (int p_x) /*@*/ /*@ensures result == p_x@*/ ;
+extern size_t size_fromLong (long p_x) /*@*/ /*@ensures result == p_x@*/ ;
+extern size_t size_fromLongUnsigned (long unsigned p_x) /*@*/ /*@ensures result == p_x@*/ ;
+extern int longUnsigned_toInt (long unsigned int p_x) /*@*/ /*@ensures result == p_x@*/ ;
+extern int long_toInt (long p_x) /*@*/ /*@ensures result == p_x@*/;
+extern long unsigned longUnsigned_fromInt (int p_x) /*@*/  /*@ensures result == p_x@*/ ;
 /*@=czechfcns@*/
 
-/* string functions */
-
-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 int mstring_length (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ;
-# define mstring_length(s) \
-  (((s) != NULL) ? size_toInt (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 (int 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)
+# include "mstring.h"
 
 extern int int_compare (/*@sef@*/ int p_x, /*@sef@*/ int p_y) /*@*/ ;
 # define int_compare(x,y) (((x) > (y)) ? 1 : (((x) < (y)) ? -1 : 0))