*** empty log message ***

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

diff --git a/src/Headers/stateInfo.h b/src/Headers/stateInfo.h
index a446b4b6ccbdb88336e6c225533cd4a4ac7bc3c3..a5d0fcbd880807091e19ffc8c80f798a6b60f38d 100644 (file)
--- a/src/Headers/stateInfo.h
+++ b/src/Headers/stateInfo.h
@@ -33,6 +33,7 @@ extern /*@only@*/ stateInfo
 
 extern /*@only@*/ stateInfo stateInfo_copy (stateInfo p_a); 
 
+extern /*@only@*/ /*@notnull@*/ stateInfo stateInfo_currentLoc (void) ;
 extern /*@only@*/ /*@notnull@*/ stateInfo stateInfo_makeLoc (fileloc p_loc) ;
 extern /*@only@*/ stateInfo stateInfo_makeRefLoc (/*@exposed@*/ sRef p_ref, fileloc p_loc) ;