#define __constraintExpr_h__
-typedef union constraintTermValue_
-{
- exprNode expr;
- sRef sref;
- int intlit;
-} constraintTermValue;
-
-typedef enum
-{
- EXPRNODE, SREF,
- INTLITERAL
-} constraintTermType;
-
-struct _constraintTerm {
- fileloc loc;
- constraintTermValue value;
- constraintTermType kind;
-};
-
-
-typedef enum
-{
- PLUS,
- MINUS
-}
-constraintExprBinaryOpKind;
-
-typedef enum
-{
- VALUE, CALLSAFE,
- MAXSET, MINSET, MAXREAD, MINREAD,
- NULLTERMINATED,
- UNDEFINED
-}
-constraintExprUnaryOpKind;
-
typedef enum
{
binaryexpr,
unaryExpr,
- term,
+ term
}
constraintExprKind;
-typedef struct constraintExprBinaryOp_
-{
- constraintExpr expr1;
- constraintExprBinaryOpKind binaryOp;
- constraintExpr expr2;
-} constraintExprBinaryOp;
-
-
-typedef struct constraintExprUnaryOp_
-{
- constraintExpr expr;
- constraintExprUnaryOpKind unaryOp;
-} constraintExprUnaryOp;
-
-
-typedef union constraintExprData_
-{
- constraintExprBinaryOp binaryOp;
- constraintExprUnaryOp unaryOp;
- constraintTerm term;
-} *constraintExprData;
-
-
-struct constraintExpr_ {
+struct _constraintExpr {
constraintExprKind kind;
constraintExprData data;
};
-# define constraintExpr_undefined ((constraintExpr)NULL)
-
-//constraintTerm constraintTerm_copy (constraintTerm term);
-int constraintExpr_getValue (constraintExpr expr);
-constraintExpr constraintExpr_setFileloc (constraintExpr expr, fileloc loc);
-
-constraintExpr constraintExpr_copy (constraintExpr expr);
+/*@constant null constraintExpr constraintExpr_undefined; @*/
+# define constraintExpr_undefined ((constraintExpr)NULL)
-cstring constraintExpr_unparse (constraintExpr ex);
-extern cstring constraintExpr_print (constraintExpr expr);
+extern /*@falsenull@*/ bool constraintExpr_isDefined (constraintExpr p_e) /*@*/ ;
+extern /*@unused@*/ /*@truenull@*/ bool constraintExpr_isUndefined (constraintExpr p_e) /*@*/ ;
+extern /*@unused@*/ /*@truenull@*/ bool constraintExpr_isError (constraintExpr p_e) /*@*/ ;
+# define constraintExpr_isDefined(e) ((e) != constraintExpr_undefined)
+# define constraintExpr_isUndefined(e) ((e) == constraintExpr_undefined)
+# define constraintExpr_isError(e) ((e) == constraintExpr_undefined)
-bool constraintExpr_similar (constraintExpr expr1, constraintExpr expr2);
-bool constraintExpr_same (constraintExpr expr1, constraintExpr expr2);
-constraintExpr constraintExpr_searchandreplace (constraintExpr c, constraintExpr old, constraintExpr new );
-bool constraintExpr_canGetValue (constraintExpr expr);
-int constraintExpr_compare (constraintExpr expr1, constraintExpr expr2);
+void constraintExpr_free ( /*@only@*/ constraintExpr expr);
-constraintExpr constraintExpr_makeValueInt (int i);
+int constraintExpr_getValue (constraintExpr expr) /*@*/;
-constraintExpr constraintExpr_makeIntLiteral (int i);
+constraintExpr constraintExpr_setFileloc (/*@returned@*/ constraintExpr c, fileloc loc) /*@modifies c@*/;
-constraintExpr constraintExpr_makeValueExpr (exprNode expr);
+constraintExpr constraintExpr_copy (constraintExpr expr) /*@*/;
-constraintExpr constraintExpr_makeMaxSetExpr (exprNode expr);
+/*@only@*/ cstring constraintExpr_unparse (/*@temp@*/ /*@observer@*/ constraintExpr ex) /*@*/;
+extern cstring constraintExpr_print (constraintExpr expr) /*@*/;
-constraintExpr constraintExpr_makeMaxReadExpr (exprNode expr);
-constraintExpr constraintExpr_makeMinSetExpr (exprNode expr);
+bool constraintExpr_similar (constraintExpr expr1, constraintExpr expr2) /*@*/;
+bool constraintExpr_same (constraintExpr expr1, constraintExpr expr2) /*@*/;
+/*@only@*/ constraintExpr constraintExpr_searchandreplace (/*@only@*/ /*@unique@*/ constraintExpr c, /*@observer@*/ constraintExpr old, /*@observer@*/ constraintExpr new ) /*@modifies c@*/;
+bool constraintExpr_canGetValue (constraintExpr expr) /*@*/;
-constraintExpr constraintExpr_makeMinReadExpr (exprNode expr);
+int constraintExpr_compare (constraintExpr expr1, constraintExpr expr2) /*@*/;
-constraintExpr constraintExpr_makeIncConstraintExpr (constraintExpr expr);
+//constraintExpr constraintExpr_makeValueInt (int i);
-constraintExpr constraintExpr_makeDecConstraintExpr (constraintExpr expr);
+/*@only@*/ constraintExpr constraintExpr_makeIntLiteral (int i);
-constraintExpr constraintExpr_simplify (constraintExpr c);
+/*@only@*/ constraintExpr constraintExpr_makeValueExpr (/*@exposed@*/ exprNode expr);
+/*@only@*/ constraintExpr constraintExpr_makeMaxSetExpr (/*@exposed@*/ exprNode expr);
-constraintExpr constraintExpr_solveBinaryExpr (constraintExpr lexpr, constraintExpr expr);
+/*@only@*/ constraintExpr constraintExpr_makeMaxReadExpr (/*@exposed@*/ exprNode expr);
-bool constraintExpr_search (constraintExpr c, constraintExpr old);
-/* jjjkkkk */
+/*@only@*/ constraintExpr constraintExpr_makeIncConstraintExpr (/*@only@*/ constraintExpr expr);
-constraintExprData constraintExprData_copy (constraintExprData data, constraintExprKind kind);
+/*@only@*/ constraintExpr constraintExpr_makeDecConstraintExpr (/*@only@*/ constraintExpr expr);
+/*@only@*/ constraintExpr constraintExpr_simplify (/*@only@*/ constraintExpr c);
-constraintExprData constraintExprData_termSetTerm (/*@out@*/ constraintExprData data, constraintTerm term);
+/*@only@*/ constraintExpr constraintExpr_solveBinaryExpr (constraintExpr lexpr, /*@only@*/ constraintExpr expr) /*@modifies lexpr, expr @*/;
-constraintTerm constraintExprData_termGetTerm (constraintExprData data) /*@*/;
+bool constraintExpr_search (/*@observer@*/ constraintExpr c, /*@observer@*/ constraintExpr old);
-constraintExprUnaryOpKind constraintExprData_unaryExprGetOp (constraintExprData data) /*@*/;
+/*@only@*/ fileloc constraintExpr_getFileloc (constraintExpr expr);
-constraintExpr constraintExprData_unaryExprGetExpr (constraintExprData data) /*@*/;
-constraintExprData constraintExprData_unaryExprSetOp (constraintExprData data, constraintExprUnaryOpKind op);
+/*@only@*/ constraintExpr constraintExpr_makeSRefMaxset ( /*@exposed@*/ sRef s);
+/*@only@*/ constraintExpr constraintExpr_makeTermsRef (/*@exposed@*/ sRef s);
-constraintExprData constraintExprData_unaryExprSetExpr (constraintExprData data, constraintExpr expr);
+constraintExpr constraintExpr_doSRefFixBaseParam ( /*@returned@*/ constraintExpr expr, exprNodeList arglist);
+/*@only@*/ constraintExpr constraintExpr_makeExprNode (/*@exposed@*/ exprNode e);
-constraintExprBinaryOpKind constraintExprData_binaryExprGetOp (constraintExprData data);
+/*@only@*/ constraintExpr constraintExpr_doFixResult (/*@only@*/ constraintExpr expr, /*@exposed@*/ exprNode fcnCall);
-constraintExpr constraintExprData_binaryExprGetExpr1 (constraintExprData data)/*@*/;
+bool constraintExpr_isLit (constraintExpr expr);
-constraintExpr constraintExprData_binaryExprGetExpr2 (constraintExprData data)/*@*/;
+/*@only@*/ constraintExpr constrainExpr_makeAddExpr (/*@only@*/constraintExpr expr, /*@only@*/ constraintExpr add);
-constraintExprData constraintExprData_binaryExprSetExpr1 (constraintExprData data, constraintExpr expr);
+/*@only@*/ constraintExpr constraintExpr_makeSubtractExpr (/*@only@*/ constraintExpr expr, /*@only@*/ constraintExpr addent);
-constraintExprData constraintExprData_binaryExprSetExpr2 (constraintExprData data, constraintExpr expr);
+/*@only@*/ constraintExpr constraintExpr_parseMakeUnaryOp (lltok op,/*@only@*/ constraintExpr cexpr);
-constraintExprData constraintExprData_binaryExprSetOp (constraintExprData data, constraintExprBinaryOpKind op);
-fileloc constraintExpr_getFileloc (constraintExpr expr);
+constraintExpr constraintExpr_parseMakeBinaryOp (/*@only@*/ constraintExpr expr1, lltok op, /*@only@*/ constraintExpr expr2);
-constraintExpr constraintExpr_makeBinaryOpConstraintExprIntLiteral (constraintExpr expr, int literal);
+bool constraintExpr_hasMaxSet (/*@observer@*/ constraintExpr expr);
-constraintExpr constraintExpr_makeSRefMaxset (sRef s);
-constraintExpr constraintExpr_makeTermsRef (sRef s);
-constraintExpr constraintExpr_doSRefFixBaseParam ( /*@returned@*/ constraintExpr expr, exprNodeList arglist);
-constraintExpr constraintExpr_makeExprNode (exprNode e);
-constraintExpr constraintExpr_doSRefFixConstraintParam (/*@returned@*/ constraintExpr expr, exprNodeList arglist);
+/*@only@*/ constraintExpr constraintExpr_makeSRefMaxRead(/*@exposed@*/ sRef s);
-constraintExpr constraintExpr_doFixResult (/*@returned@*/ constraintExpr expr, exprNode fcnCall);
-bool constraintExpr_isLit (constraintExpr expr);
-constraintExpr constraintExpr_makeAddConstraintExpr (constraintExpr expr, constraintExpr add);
+/*@only@*/ constraintExpr constraintExpr_doSRefFixConstraintParam (/*@returned@*/ /*@only@*/ constraintExpr expr, exprNodeList arglist) /*@modifies expr@*/;
-constraintExpr constraintExpr_parseMakeUnaryOp (lltok op, constraintExpr cexpr);
+/*@only@*/
+constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr expr,
+ /*@out@*/ bool * propagate,
+ /*@out@*/ int *literal);
-constraintExpr constraintExpr_parseMakeBinaryOp (constraintExpr expr1, lltok op, constraintExpr expr2);
+bool constraintExpr_isBinaryExpr (/*@observer@*/ constraintExpr c);
+#else
-bool constraintExpr_hasMaxSet (constraintExpr expr);
+# error "Multiple include"
#endif
andersk / splint.git / blobdiff