*** empty log message ***

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

diff --git a/src/Headers/annotationInfo.h b/src/Headers/annotationInfo.h
index 08d762152a521a8aaac0a4f80c9b4185801dc363..0ce3da9b17260c3964c110c48ce9d778f93ed700 100644 (file)
--- a/src/Headers/annotationInfo.h
+++ b/src/Headers/annotationInfo.h
@@ -56,6 +56,8 @@ extern void annotationInfo_free (/*@only@*/ annotationInfo) ;
 extern /*@observer@*/ cstring annotationInfo_dump (annotationInfo) ;
 extern /*@observer@*/ annotationInfo annotationInfo_undump (char **p_s) /*@modifies *p_s@*/ ;
 
+extern void annotationInfo_showContextRefError (annotationInfo, sRef) /*@*/ ;
+
 # else
 # error "Multiple include"
 # endif