/*
-** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
+** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
** See ../LICENSE for license information.
**
*/
** (tokens are defined in cgrammar.y)
*/
-typedef enum _quals {
- QU_UNKNOWN,
+typedef enum {
+ QU_UNKNOWN = 0,
QU_CONST, QU_VOLATILE, QU_INLINE,
QU_EXTERN, QU_STATIC, QU_AUTO, QU_REGISTER,
QU_SHORT, QU_LONG, QU_SIGNED, QU_UNSIGNED,
QU_OUT, QU_IN,
QU_ONLY, QU_IMPONLY,
QU_TEMP, QU_SHARED, QU_KEEP, QU_KEPT, QU_PARTIAL, QU_SPECIAL,
- QU_NULL, QU_RELNULL, QU_NULLTERMINATED,
+ QU_NULL, QU_RELNULL, QU_ISNULL,
+ QU_NULLTERMINATED,
QU_SETBUFFERSIZE,
QU_EXPOSED, QU_RETURNED, QU_OBSERVER, QU_UNIQUE,
QU_OWNED, QU_DEPENDENT, QU_RELDEF,
QU_CHECKED, QU_UNCHECKED, QU_CHECKEDSTRICT, QU_CHECKMOD,
QU_UNDEF, QU_KILLED,
QU_PRINTFLIKE, QU_SCANFLIKE, QU_MESSAGELIKE,
+ QU_USERANNOT,
QU_LAST
-} qual ;
+} quenum;
+
+immut_typedef struct {
+ quenum kind;
+ /*@observer@*/ /*@null@*/ annotationInfo info; /* for QU_USERANNOT only */
+} *qual;
+
+extern /*@only@*/ cstring qual_dump (qual) ;
+extern qual qual_undump (char **p_s) /*@modifies *p_s@*/ ;
+
/*
** qualifiers correspond to tokens in the grammar:
extern qual qual_fromInt (int p_q) /*@*/ ;
extern /*@observer@*/ cstring qual_unparse (qual p_q) /*@*/ ;
-extern bool qual_equal (qual p_q1, qual p_q2) /*@*/ ;
-# define qual_equal(q1,q2) ((q1) == (q2))
+extern bool qual_match (qual p_q1, qual p_q2) /*@*/ ;
extern bool qual_isUnknown (qual) /*@*/ ;
extern bool qual_isTrueNull (qual) /*@*/ ;
extern bool qual_isCheckedStrict (qual) /*@*/ ;
extern bool qual_isUnchecked (qual) /*@*/ ;
extern bool qual_isNull (qual) /*@*/ ;
+extern bool qual_isIsNull (qual) /*@*/ ;
extern bool qual_isRelNull (qual) /*@*/ ;
extern bool qual_isNotNull (qual) /*@*/ ;
extern bool qual_isReturned (qual) /*@*/ ;
extern bool qual_isImplied (/*@sef@*/ qual) /*@*/ ;
extern bool qual_isExQual (/*@sef@*/ qual) /*@*/ ;
extern bool qual_isAliasQual (/*@sef@*/ qual) /*@*/ ;
-/* start modifications */
-extern bool qual_isNullTerminated (qual) /*@*/ ;
-extern bool qual_isBufQualifier (qual) /*@*/ ;
-/* end modifications */
+extern bool qual_isPrintfLike (/*@sef@*/ qual) /*@*/ ;
+extern bool qual_isScanfLike (/*@sef@*/ qual) /*@*/ ;
+extern bool qual_isMessageLike (/*@sef@*/ qual) /*@*/ ;
+extern bool qual_isMetaState (/*@sef@*/ qual) /*@*/ ;
+extern bool qual_isNullTerminated( /*@sef@*/ qual ) /*@*/ ;
+
+extern bool qual_isMemoryAllocation (/*@sef@*/ qual) /*@*/ ;
+# define qual_isMemoryAllocation(q) \
+ (qual_isOnly (q) || qual_isShared (q) || \
+ qual_isDependent (q) || qual_isOwned (q))
-# define qual_isUnknown(q) ((q) == QU_UNKNOWN)
-# define qual_isTrueNull(q) ((q) == QU_TRUENULL)
-# define qual_isFalseNull(q) ((q) == QU_FALSENULL)
-# define qual_isOwned(q) ((q) == QU_OWNED)
-# define qual_isDependent(q) ((q) == QU_DEPENDENT)
-# define qual_isRefCounted(q) ((q) == QU_REFCOUNTED)
-# define qual_isRefs(q) ((q) == QU_REFS)
-# define qual_isNewRef(q) ((q) == QU_NEWREF)
-# define qual_isKillRef(q) ((q) == QU_KILLREF)
-# define qual_isTempRef(q) ((q) == QU_TEMPREF)
-# define qual_isLong(q) ((q) == QU_LONG)
-# define qual_isShort(q) ((q) == QU_SHORT)
-# define qual_isSigned(q) ((q) == QU_SIGNED)
-# define qual_isUnsigned(q) ((q) == QU_UNSIGNED)
-# define qual_isUnique(q) ((q) == QU_UNIQUE)
-# define qual_isExits(q) ((q) == QU_EXITS)
-# define qual_isMayExit(q) ((q) == QU_MAYEXIT)
-# define qual_isNeverExit(q) ((q) == QU_NEVEREXIT)
-# define qual_isTrueExit(q) ((q) == QU_TRUEEXIT)
-# define qual_isFalseExit(q) ((q) == QU_FALSEEXIT)
-# define qual_isConst(q) ((q) == QU_CONST)
-# define qual_isVolatile(q) ((q) == QU_VOLATILE)
-# define qual_isInline(q) ((q) == QU_INLINE)
-# define qual_isExtern(q) ((q) == QU_EXTERN)
-# define qual_isStatic(q) ((q) == QU_STATIC)
-# define qual_isAuto(q) ((q) == QU_AUTO)
-# define qual_isRegister(q) ((q) == QU_REGISTER)
-# define qual_isOut(q) ((q) == QU_OUT)
-# define qual_isIn(q) ((q) == QU_IN)
-# define qual_isYield(q) ((q) == QU_YIELD)
-# define qual_isOnly(q) ((q) == QU_ONLY)
-# define qual_isImpOnly(q) ((q) == QU_IMPONLY)
-# define qual_isPartial(q) ((q) == QU_PARTIAL)
-# define qual_isSpecial(q) ((q) == QU_SPECIAL)
-# define qual_isKeep(q) ((q) == QU_KEEP)
-# define qual_isKept(q) ((q) == QU_KEPT)
-# define qual_isTemp(q) ((q) == QU_TEMP)
-# define qual_isShared(q) ((q) == QU_SHARED)
-# define qual_isRelDef(q) ((q) == QU_RELDEF)
-# define qual_isNull(q) ((q) == QU_NULL)
-# define qual_isRelNull(q) ((q) == QU_RELNULL)
-# define qual_isNotNull(q) ((q) == QU_NOTNULL)
-# define qual_isReturned(q) ((q) == QU_RETURNED)
-# define qual_isExposed(q) ((q) == QU_EXPOSED)
-# define qual_isObserver(q) ((q) == QU_OBSERVER)
-# define qual_isUnused(q) ((q) == QU_UNUSED)
-# define qual_isExternal(q) ((q) == QU_EXTERNAL)
-# define qual_isSef(q) ((q) == QU_SEF)
-# define qual_isAbstract(q) ((q) == QU_ABSTRACT)
-# define qual_isConcrete(q) ((q) == QU_CONCRETE)
-# define qual_isMutable(q) ((q) == QU_MUTABLE)
-# define qual_isImmutable(q) ((q) == QU_IMMUTABLE)
-# define qual_isChecked(q) ((q) == QU_CHECKED)
-# define qual_isCheckMod(q) ((q) == QU_CHECKMOD)
-# define qual_isCheckedStrict(q) ((q) == QU_CHECKEDSTRICT)
-# define qual_isUnchecked(q) ((q) == QU_UNCHECKED)
-# define qual_isUndef(q) ((q) == QU_UNDEF)
-# define qual_isKilled(q) ((q) == QU_KILLED)
-# define qual_isNullTerminated(q) ((q) == QU_NULLTERMINATED)
+extern bool qual_isSharing (/*@sef@*/ qual) /*@*/ ;
+# define qual_isSharing(q) \
+ (qual_isObserver (q) || qual_isExposed (q))
+extern /*@observer@*/ annotationInfo qual_getAnnotationInfo (qual) /*@*/ ;
+
+# define qual_isUnknown(q) ((q)->kind == QU_UNKNOWN)
+# define qual_isTrueNull(q) ((q)->kind == QU_TRUENULL)
+# define qual_isFalseNull(q) ((q)->kind == QU_FALSENULL)
+# define qual_isOwned(q) ((q)->kind == QU_OWNED)
+# define qual_isDependent(q) ((q)->kind == QU_DEPENDENT)
+# define qual_isRefCounted(q) ((q)->kind == QU_REFCOUNTED)
+# define qual_isRefs(q) ((q)->kind == QU_REFS)
+# define qual_isNewRef(q) ((q)->kind == QU_NEWREF)
+# define qual_isKillRef(q) ((q)->kind == QU_KILLREF)
+# define qual_isTempRef(q) ((q)->kind == QU_TEMPREF)
+# define qual_isLong(q) ((q)->kind == QU_LONG)
+# define qual_isShort(q) ((q)->kind == QU_SHORT)
+# define qual_isSigned(q) ((q)->kind == QU_SIGNED)
+# define qual_isUnsigned(q) ((q)->kind == QU_UNSIGNED)
+# define qual_isUnique(q) ((q)->kind == QU_UNIQUE)
+# define qual_isExits(q) ((q)->kind == QU_EXITS)
+# define qual_isMayExit(q) ((q)->kind == QU_MAYEXIT)
+# define qual_isNeverExit(q) ((q)->kind == QU_NEVEREXIT)
+# define qual_isTrueExit(q) ((q)->kind == QU_TRUEEXIT)
+# define qual_isFalseExit(q) ((q)->kind == QU_FALSEEXIT)
+# define qual_isConst(q) ((q)->kind == QU_CONST)
+# define qual_isVolatile(q) ((q)->kind == QU_VOLATILE)
+# define qual_isInline(q) ((q)->kind == QU_INLINE)
+# define qual_isExtern(q) ((q)->kind == QU_EXTERN)
+# define qual_isStatic(q) ((q)->kind == QU_STATIC)
+# define qual_isAuto(q) ((q)->kind == QU_AUTO)
+# define qual_isRegister(q) ((q)->kind == QU_REGISTER)
+# define qual_isOut(q) ((q)->kind == QU_OUT)
+# define qual_isIn(q) ((q)->kind == QU_IN)
+# define qual_isYield(q) ((q)->kind == QU_YIELD)
+# define qual_isOnly(q) ((q)->kind == QU_ONLY)
+# define qual_isImpOnly(q) ((q)->kind == QU_IMPONLY)
+# define qual_isPartial(q) ((q)->kind == QU_PARTIAL)
+# define qual_isSpecial(q) ((q)->kind == QU_SPECIAL)
+# define qual_isKeep(q) ((q)->kind == QU_KEEP)
+# define qual_isKept(q) ((q)->kind == QU_KEPT)
+# define qual_isTemp(q) ((q)->kind == QU_TEMP)
+# define qual_isShared(q) ((q)->kind == QU_SHARED)
+# define qual_isRelDef(q) ((q)->kind == QU_RELDEF)
+# define qual_isNull(q) ((q)->kind == QU_NULL)
+# define qual_isIsNull(q) ((q)->kind == QU_ISNULL)
+# define qual_isRelNull(q) ((q)->kind == QU_RELNULL)
+# define qual_isNotNull(q) ((q)->kind == QU_NOTNULL)
+# define qual_isReturned(q) ((q)->kind == QU_RETURNED)
+# define qual_isExposed(q) ((q)->kind == QU_EXPOSED)
+# define qual_isObserver(q) ((q)->kind == QU_OBSERVER)
+# define qual_isUnused(q) ((q)->kind == QU_UNUSED)
+# define qual_isExternal(q) ((q)->kind == QU_EXTERNAL)
+# define qual_isSef(q) ((q)->kind == QU_SEF)
+# define qual_isAbstract(q) ((q)->kind == QU_ABSTRACT)
+# define qual_isConcrete(q) ((q)->kind == QU_CONCRETE)
+# define qual_isMutable(q) ((q)->kind == QU_MUTABLE)
+# define qual_isImmutable(q) ((q)->kind == QU_IMMUTABLE)
+# define qual_isChecked(q) ((q)->kind == QU_CHECKED)
+# define qual_isCheckMod(q) ((q)->kind == QU_CHECKMOD)
+# define qual_isCheckedStrict(q) ((q)->kind == QU_CHECKEDSTRICT)
+# define qual_isUnchecked(q) ((q)->kind == QU_UNCHECKED)
+# define qual_isUndef(q) ((q)->kind == QU_UNDEF)
+# define qual_isKilled(q) ((q)->kind == QU_KILLED)
+# define qual_isPrintfLike(q) ((q)->kind == QU_PRINTFLIKE)
+# define qual_isScanfLike(q) ((q)->kind == QU_SCANFLIKE)
+# define qual_isMessageLike(q) ((q)->kind == QU_MESSAGELIKE)
+# define qual_isMetaState(q) ((q)->kind == QU_USERANNOT)
+
+# define qual_isNullTerminated(q) ((q)->kind == QU_NULLTERMINATED)
+
+extern qual qual_createPlain (quenum) /*@*/ ;
+extern qual qual_createMetaState (annotationInfo) /*@*/ ;
extern qual qual_createTrueNull (void) /*@*/ ;
extern qual qual_createFalseNull (void) /*@*/ ;
extern qual qual_createRefCounted (void) /*@*/ ;
extern qual qual_createKept (void) /*@*/ ;
extern qual qual_createTemp (void) /*@*/ ;
extern qual qual_createShared (void) /*@*/ ;
-extern qual qual_createNull (void) /*@*/ ;
+extern qual qual_createNull (void) /*@*/ ;
+extern qual qual_createIsNull (void) /*@*/ ;
extern qual qual_createRelNull (void) /*@*/ ;
extern qual qual_createReturned (void) /*@*/ ;
extern qual qual_createExposed (void) /*@*/ ;
extern qual qual_createKilled (void) /*@*/ ;
extern qual qual_createNullTerminated (void) /*@*/ ;
-# ifndef NOLCL
extern qual qual_createUnknown (void) /*@*/ ;
-# define qual_createUnknown() (QU_UNKNOWN)
+# define qual_createUnknown() (qual_createPlain (QU_UNKNOWN))
extern qual qual_createPrintfLike (void) /*@*/ ;
extern qual qual_createScanfLike (void) /*@*/ ;
extern qual qual_createMessageLike (void) /*@*/ ;
-# define qual_createPrintfLike() (QU_PRINTFLIKE)
-# define qual_createScanfLike() (QU_SCANFLIKE)
-# define qual_createMessageLike() (QU_MESSAGELIKE)
-# endif
+# define qual_createPrintfLike() (qual_createPlain (QU_PRINTFLIKE))
+# define qual_createScanfLike() (qual_createPlain (QU_SCANFLIKE))
+# define qual_createMessageLike() (qual_createPlain (QU_MESSAGELIKE))
+
+# define qual_createTrueNull() qual_createPlain (QU_TRUENULL)
+# define qual_createFalseNull() qual_createPlain (QU_FALSENULL)
+# define qual_createRefCounted() qual_createPlain (QU_REFCOUNTED)
+# define qual_createRefs() qual_createPlain (QU_REFS)
+# define qual_createNewRef() qual_createPlain (QU_NEWREF)
+# define qual_createKillRef() qual_createPlain (QU_KILLREF)
+# define qual_createTempRef() qual_createPlain (QU_TEMPREF)
+# define qual_createNotNull() qual_createPlain (QU_NOTNULL)
+# define qual_createAbstract() qual_createPlain (QU_ABSTRACT)
+# define qual_createConcrete() qual_createPlain (QU_CONCRETE)
+# define qual_createMutable() qual_createPlain (QU_MUTABLE)
+# define qual_createImmutable() qual_createPlain (QU_IMMUTABLE)
+# define qual_createShort() qual_createPlain (QU_SHORT)
+# define qual_createLong() qual_createPlain (QU_LONG)
+# define qual_createSigned() qual_createPlain (QU_SIGNED)
+# define qual_createUnsigned() qual_createPlain (QU_UNSIGNED)
+# define qual_createUnique() qual_createPlain (QU_UNIQUE)
+# define qual_createMayExit() qual_createPlain (QU_MAYEXIT)
+# define qual_createExits() qual_createPlain (QU_EXITS)
+# define qual_createNeverExit() qual_createPlain (QU_NEVEREXIT)
+# define qual_createTrueExit() qual_createPlain (QU_TRUEEXIT)
+# define qual_createFalseExit() qual_createPlain (QU_FALSEEXIT)
+# define qual_createConst() qual_createPlain (QU_CONST)
+# define qual_createVolatile() qual_createPlain (QU_VOLATILE)
+# define qual_createInline() qual_createPlain (QU_INLINE)
+# define qual_createExtern() qual_createPlain (QU_EXTERN)
+# define qual_createStatic() qual_createPlain (QU_STATIC)
+# define qual_createAuto() qual_createPlain (QU_AUTO)
+# define qual_createRegister() qual_createPlain (QU_REGISTER)
+# define qual_createOut() qual_createPlain (QU_OUT)
+# define qual_createIn() qual_createPlain (QU_IN)
+# define qual_createYield() qual_createPlain (QU_YIELD)
+# define qual_createOnly() qual_createPlain (QU_ONLY)
+# define qual_createOwned() qual_createPlain (QU_OWNED)
+# define qual_createDependent() qual_createPlain (QU_DEPENDENT)
+# define qual_createRelDef() qual_createPlain (QU_RELDEF)
+# define qual_createImpOnly() qual_createPlain (QU_IMPONLY)
+# define qual_createPartial() qual_createPlain (QU_PARTIAL)
+# define qual_createSpecial() qual_createPlain (QU_SPECIAL)
+# define qual_createKeep() qual_createPlain (QU_KEEP)
+# define qual_createKept() qual_createPlain (QU_KEPT)
+# define qual_createTemp() qual_createPlain (QU_TEMP)
+# define qual_createShared() qual_createPlain (QU_SHARED)
+# define qual_createNull() qual_createPlain (QU_NULL)
+# define qual_createIsNull() qual_createPlain (QU_ISNULL)
+# define qual_createRelNull() qual_createPlain (QU_RELNULL)
+# define qual_createReturned() qual_createPlain (QU_RETURNED)
+# define qual_createExposed() qual_createPlain (QU_EXPOSED)
+# define qual_createObserver() qual_createPlain (QU_OBSERVER)
+# define qual_createUnused() qual_createPlain (QU_UNUSED)
+# define qual_createExternal() qual_createPlain (QU_EXTERNAL)
+# define qual_createSef() qual_createPlain (QU_SEF)
+# define qual_createChecked() qual_createPlain (QU_CHECKED)
+# define qual_createCheckMod() qual_createPlain (QU_CHECKMOD)
+# define qual_createCheckedStrict() qual_createPlain (QU_CHECKEDSTRICT)
+# define qual_createUnchecked() qual_createPlain (QU_UNCHECKED)
+# define qual_createUndef() qual_createPlain (QU_UNDEF)
+# define qual_createKilled() qual_createPlain (QU_KILLED)
-# define qual_createTrueNull() (QU_TRUENULL)
-# define qual_createFalseNull() (QU_FALSENULL)
-# define qual_createRefCounted() (QU_REFCOUNTED)
-# define qual_createRefs() (QU_REFS)
-# define qual_createNewRef() (QU_NEWREF)
-# define qual_createKillRef() (QU_KILLREF)
-# define qual_createTempRef() (QU_TEMPREF)
-# define qual_createNotNull() (QU_NOTNULL)
-# define qual_createAbstract() (QU_ABSTRACT)
-# define qual_createConcrete() (QU_CONCRETE)
-# define qual_createMutable() (QU_MUTABLE)
-# define qual_createImmutable() (QU_IMMUTABLE)
-# define qual_createShort() (QU_SHORT)
-# define qual_createLong() (QU_LONG)
-# define qual_createSigned() (QU_SIGNED)
-# define qual_createUnsigned() (QU_UNSIGNED)
-# define qual_createUnique() (QU_UNIQUE)
-# define qual_createMayExit() (QU_MAYEXIT)
-# define qual_createExits() (QU_EXITS)
-# define qual_createNeverExit() (QU_NEVEREXIT)
-# define qual_createTrueExit() (QU_TRUEEXIT)
-# define qual_createFalseExit() (QU_FALSEEXIT)
-# define qual_createConst() (QU_CONST)
-# define qual_createVolatile() (QU_VOLATILE)
-# define qual_createInline() (QU_INLINE)
-# define qual_createExtern() (QU_EXTERN)
-# define qual_createStatic() (QU_STATIC)
-# define qual_createAuto() (QU_AUTO)
-# define qual_createRegister() (QU_REGISTER)
-# define qual_createOut() (QU_OUT)
-# define qual_createIn() (QU_IN)
-# define qual_createYield() (QU_YIELD)
-# define qual_createOnly() (QU_ONLY)
-# define qual_createOwned() (QU_OWNED)
-# define qual_createDependent() (QU_DEPENDENT)
-# define qual_createRelDef() (QU_RELDEF)
-# define qual_createImpOnly() (QU_IMPONLY)
-# define qual_createPartial() (QU_PARTIAL)
-# define qual_createSpecial() (QU_SPECIAL)
-# define qual_createKeep() (QU_KEEP)
-# define qual_createKept() (QU_KEPT)
-# define qual_createTemp() (QU_TEMP)
-# define qual_createShared() (QU_SHARED)
-# define qual_createNull() (QU_NULL)
-# define qual_createRelNull() (QU_RELNULL)
-# define qual_createReturned() (QU_RETURNED)
-# define qual_createExposed() (QU_EXPOSED)
-# define qual_createObserver() (QU_OBSERVER)
-# define qual_createUnused() (QU_UNUSED)
-# define qual_createExternal() (QU_EXTERNAL)
-# define qual_createSef() (QU_SEF)
-# define qual_createChecked() (QU_CHECKED)
-# define qual_createCheckMod() (QU_CHECKMOD)
-# define qual_createCheckedStrict() (QU_CHECKEDSTRICT)
-# define qual_createUnchecked() (QU_UNCHECKED)
-# define qual_createUndef() (QU_UNDEF)
-# define qual_createKilled() (QU_KILLED)
-# define qual_createNullTerminated() (QU_NULLTERMINATED)
-# define qual_createSetBufferSize() (QU_SETBUFFERSIZE)
+
+# define qual_createNullTerminated() qual_createPlain (QU_NULLTERMINATED)
+//# define qual_createSetBufferSize() qual_createPlain (QU_SETBUFFERSIZE)
+
+
+
+/* start modifications */
+//extern bool qual_isNullTerminated (qual p_q) ;
+//extern bool qual_isBufQualifier (qual p_q) ;
+/* end modifications */
+
+/* start modifications */
+/* This is used to check if we the qualifier matches any of the
+len/size/nullterminated types */
+
+extern bool qual_isBufQualifier(/*@sef@*/ qual) /*@*/;
+
+# define qual_isBufQualifier(q) \
+ (qual_isNullTerminated(q))
+
+/* end of modification/s */
extern bool qual_isGlobCheck (/*@sef@*/ qual p_q) /*@*/ ;
# define qual_isGlobCheck(q) \
(qual_isRefCounted(q) || qual_isRefs(q) || qual_isNewRef (q) || \
qual_isKillRef (q) || qual_isTempRef (q))
+extern bool qual_isNullStateQual (/*@sef@*/ qual) /*@*/ ;
+# define qual_isNullStateQual(q) \
+ (qual_isNull (q) || qual_isIsNull (q) || qual_isRelNull (q) \
+ || qual_isNotNull (q))
+
# define qual_isTypeQual(q) \
(qual_isAbstract(q) || qual_isMutable(q) || qual_isImmutable(q))
(qual_isOut (q) || qual_isIn (q) || qual_isSpecial (q) \
|| qual_isPartial (q) || qual_isRelDef (q))
-/* start modifications */
-/* This is used to check if we the qualifier matches any of the
-len/size/nullterminated types */
-
-# define qual_isBufQualifier(q) \
- (qual_isNullTerminated(q))
-
-/* end of modification/s */
-
# define qual_isGlobalQual(q) \
(qual_isUndef(q) || qual_isKilled (q))
# define qual_isImplied(q) (qual_isImpOnly(q))
-
# define qual_isExQual(q) (qual_isExposed (q) || qual_isObserver (q))
# define qual_isAliasQual(q) \
# endif
+
+
+