*** empty log message ***

[splint.git] / src / annotationInfo.c

diff --git a/src/annotationInfo.c b/src/annotationInfo.c
index e270010849df405d582bd7bc4f7ad3fa6160b14b..8a1fe571e0019d9ecca6027385412b2eb3cba158 100644 (file)
--- a/src/annotationInfo.c
+++ b/src/annotationInfo.c
@@ -173,3 +173,30 @@ cstring annotationInfo_dump (annotationInfo ainfo)
 
   BADBRANCH;
 }
+
+void annotationInfo_showContextRefError (annotationInfo a, sRef sr)
+{
+  mtContextNode mcontext;
+  llassert (!annotationInfo_matchesContextRef (a, sr));
+  llassert (annotationInfo_isDefined (a));
+  mcontext = a->context;
+
+  if (mtContextNode_matchesRef (mcontext, sr))
+    {
+      /* Matches annotation context, must also match meta state context. */
+      metaStateInfo minfo = a->state;
+
+      if (mtContextNode_matchesRef (metaStateInfo_getContext (minfo), sr))
+       {
+         BADBRANCH;
+       }
+      else
+       {
+         mtContextNode_showRefError (metaStateInfo_getContext (minfo), sr);
+       }
+    }
+  else
+    {
+      mtContextNode_showRefError (mcontext, sr);
+    }
+}