Fixed library dump support so that buffer constraint annotations are read and written...

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

diff --git a/src/Headers/uentry.h b/src/Headers/uentry.h
index 18f84672e9be89a653038c95766f28b662e9d354..caaa6c364aa654e4bf977da528ec97a55fc70191 100644 (file)
--- a/src/Headers/uentry.h
+++ b/src/Headers/uentry.h
@@ -590,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);
+  void uentry_setNullTerminatedState (uentry p_e);
+ 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_setSize(uentry p_e, int p_size);
+ void uentry_setLen(uentry p_e, int p_len);
 
 /*@i66*/
 /*@-nullderef@*/
@@ -631,10 +631,16 @@ 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