/*@dependent@*/ uentryList defparams;
bool hasGlobs BOOLBITS;
bool hasMods BOOLBITS;
+
+ constraintList preconditions;
+ constraintList postconditions;
+
} *ufinfo ;
typedef struct _uiinfo
//extern void uentry_setBufferSize (uentry p_e, exprNode cconstant);
/* functions for making modification to null-term info */
-extern void uentry_setNullTerminatedState (uentry p_e);
-extern void uentry_setPossiblyNullTerminatedState (uentry p_e);
-extern void uentry_setNotNullTerminated (uentry p_e);
-extern void uentry_setSize(uentry p_e, int p_size);
-extern void uentry_setLen(uentry p_e, int p_len);
+ void uentry_setNullTerminatedState (uentry p_e);
+ void uentry_setPossiblyNullTerminatedState (uentry p_e);
+//extern void uentry_setNotNullTerminated (uentry p_e);
+void uentry_setSize(uentry p_e, int p_size);
+ void uentry_setLen(uentry p_e, int p_len);
/*@i66*/
/*@-nullderef@*/
# define uentry_hasBufStateInfo(p_ue) \
(((p_ue)->info->var->bufinfo != NULL) ? TRUE : FALSE)
-extern bool uentry_isNullTerminated(/*@sef@*/uentry p_ue);
+/*@unused@*/ extern bool uentry_isNullTerminated(/*@sef@*/uentry p_ue);
# define uentry_isNullTerminated(p_ue) \
( uentry_hasBufStateInfo( (p_ue ) ) ? ( (p_ue)->info->var->bufinfo->bufstate \
== BB_NULLTERMINATED) : FALSE)
-extern bool uentry_isPossiblyNullTerminated( /*@sef@*/ uentry p_ue);
+/*@unused@*/ extern bool uentry_isPossiblyNullTerminated( /*@sef@*/ uentry p_ue);
# define uentry_isPossiblyNullTerminated(p_ue) \
( uentry_hasBufStateInfo((p_ue)) ? ( (p_ue)->info->var->bufinfo->bufstate \
== BB_POSSIBLYNULLTERMINATED) : FALSE)
-extern bool uentry_isNotNullTerminated( /*@sef@*/ uentry p_ue);
+/*@unused@*/ extern bool uentry_isNotNullTerminated( /*@sef@*/ uentry p_ue);
# define uentry_isNotNullTerminated(p_ue) \
( uentry_hasBufStateInfo( (p_ue) ) ? ( (p_ue)->info->var->bufinfo->bufstate \
== BB_NOTNULLTERMINATED) : FALSE)
# endif /* DOANNOTS */
/* start modifications */
-extern void uentry_setBufferSize (uentry p_e, exprNode p_cconstant);
+//extern void uentry_setBufferSize (uentry p_e, exprNode p_cconstant);
+/*drl7x*/
+extern constraintList uentry_getFcnPreconditions (uentry ue);
+extern constraintList uentry_getFcnPostconditions (uentry ue);
+extern void
+uentry_setPostconditions (uentry ue, /*@only@*/ constraintList postconditions);
+
+extern void
+uentry_setPreconditions (uentry ue, /*@only@*/ constraintList preconditions);
+
+ /*end mods*/
# else
# error "Multiple include"