*** empty log message ***

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

diff --git a/src/Headers/exprNode.h b/src/Headers/exprNode.h
index e9b8cda69562b45e1571477c467304e42cdab5a8..226cabb5bb024fe66a1edc1156c5161178eb1b1b 100644 (file)
--- a/src/Headers/exprNode.h
+++ b/src/Headers/exprNode.h
@@ -217,7 +217,11 @@ extern /*@exposed@*/ sRef exprNode_getSref (exprNode p_e) /*@*/ ;
 extern /*@observer@*/ uentry exprNode_getUentry (exprNode p_e) 
    /*@globals internalState@*/ ;
 extern void exprNode_produceGuards (exprNode p_pred) /*@modifies p_pred@*/ ;
+
 extern /*@observer@*/ fileloc exprNode_loc (exprNode p_e) /*@*/ ;
+extern /*@observer@*/ fileloc exprNode_getLoc (exprNode p_e) /*@*/ ;
+# define exprNode_getLoc exprNode_loc
+
 extern exprNode
   exprNode_charLiteral (char p_c, cstring p_text, /*@only@*/ fileloc p_loc) /*@*/ ;
 extern /*@observer@*/ exprNode exprNode_makeMustExit (void) /*@*/ ;