pre addition of functino level annotations.

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

diff --git a/src/Headers/exprNode.h b/src/Headers/exprNode.h
index 322def8063179f9d1b7ee29a7410192e576f9a34..c4ca2c2a5ff8ad008bc6c2b998525cbb022fe6c4 100644 (file)
--- a/src/Headers/exprNode.h
+++ b/src/Headers/exprNode.h
@@ -162,6 +162,10 @@ struct _exprNode
   environmentTable environment;
   constraintList requiresConstraints;
   constraintList ensuresConstraints;
+  //these two are used only for boolean expressions
+  //they store the ensures constraints for the true and false cases
+  constraintList trueEnsuresConstraints;
+  constraintList falseEnsuresConstraints;
 } ;
 
 /*@constant null exprNode exprNode_undefined; @*/