X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/4cccc6ad3936684419c0c7613b6d5aa443e5e9ce..920a3797c23377bfb7332b0c11bda1d708cabb72:/src/Headers/uentry.h

diff --git a/src/Headers/uentry.h b/src/Headers/uentry.h
index fcb6788..caaa6c3 100644
--- a/src/Headers/uentry.h
+++ b/src/Headers/uentry.h
@@ -103,6 +103,10 @@ typedef struct _ufinfo
   /*@dependent@*/ uentryList defparams; 
   bool hasGlobs BOOLBITS;
   bool hasMods  BOOLBITS;
+
+  constraintList preconditions;
+  constraintList postconditions;
+  
 } *ufinfo ;
 
 typedef struct _uiinfo
@@ -586,11 +590,11 @@ extern /*@exposed@*/ uentry uentry_makeUnrecognized (cstring p_c, /*@keep@*/ fil
 //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@*/
@@ -598,17 +602,17 @@ extern bool uentry_hasBufStateInfo (uentry p_ue);
 # 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)
@@ -627,7 +631,17 @@ extern void uentry_tallyAnnots (uentry u, ancontext kind);
 # 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"