*** empty log message ***

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

diff --git a/src/Headers/context.h b/src/Headers/context.h
index 29e4cf7ac34d5793ccce21152da1713499a167b5..1f64901092dc4d149ceda15ad6633e13b8e74c0a 100644 (file)
--- a/src/Headers/context.h
+++ b/src/Headers/context.h
@@ -325,10 +325,10 @@ extern void context_addAnnotation (/*@only@*/ annotationInfo)
 extern void context_addMetaState (/*@only@*/ cstring, /*@only@*/ metaStateInfo)
      /*@modifies internalState@*/ ;
 
-extern valueTable context_createValueTable (sRef p_s)
+extern valueTable context_createValueTable (sRef p_s, /*@only@*/ stateInfo p_sinfo)
      /*@globals internalState@*/ ;
 
-extern valueTable context_createGlobalMarkerValueTable (void)
+extern valueTable context_createGlobalMarkerValueTable (/*@only@*/ stateInfo p_sinfo)
      /*@globals internalState@*/ ;
 
 extern int context_getBugsLimit (void) /*@*/ ;