typedef union
{
- /*@dependent@*/ exprNode expr;
+ /*@exposed@*/ /*@dependent@*/ exprNode expr;
/*@only@*/ sRef sref;
int intlit;
} constraintTermValue;
+/*@-namechecks@*/
+
void constraintTermValue_copy (/*@out@*/ constraintTermValue src, constraintTermValue dst);
/*@-macroassign*/
} constraintTermType;
struct _constraintTerm {
- fileloc loc;
+ /*@only@*/ fileloc loc;
constraintTermValue value;
constraintTermType kind;
};
abst_typedef struct _constraintTerm * constraintTerm;
-
+extern constraintTermType constraintTerm_getKind (constraintTerm) ;
+extern /*@exposed@*/ sRef constraintTerm_getSRef (constraintTerm) ;
extern /*@falsenull@*/ bool constraintTerm_isDefined (constraintTerm p_e) /*@*/;
extern /*@unused@*/ /*@truenull@*/ bool constraintTerm_isUndefined (constraintTerm p_e) /*@*/ ;
constraintTerm constraintTerm_simplify (/*@returned@*/ constraintTerm term) /*@modifies term@*/ ;
-constraintTerm constraintTerm_makeExprNode (/*@only@*/ exprNode e) /*@*/;
+/*@only@*/ constraintTerm constraintTerm_makeExprNode (/*@dependent@*/ exprNode e) /*@*/;
constraintTerm constraintTerm_copy (constraintTerm term) /*@*/;
-//constraintTerm exprNode_makeConstraintTerm ( exprNode e) /*@*/;
-
-//bool constraintTerm_same (constraintTerm term1, constraintTerm term2) /*@*/;
-
bool constraintTerm_similar (constraintTerm term1, constraintTerm term2) /*@*/;
bool constraintTerm_canGetValue (constraintTerm term)/*@*/;
fileloc constraintTerm_getFileloc (constraintTerm t) /*@*/;
-//constraintTerm constraintTerm_makeMaxSetexpr (exprNode e) /*@*/;
-
-//constraintTerm constraintTerm_makeMinSetexpr (exprNode e) /*@*/;
-
-//constraintTerm constraintTerm_makeMaxReadexpr (exprNode e) /*@*/;
-
-//constraintTerm constraintTerm_makeMinReadexpr (exprNode e) /*@*/;
-
-//constraintTerm constraintTerm_makeValueexpr (exprNode e) /*@*/;
-
-//constraintTerm intLit_makeConstraintTerm (int i) /*@*/;
-
-//constraintTerm constraintTerm_makeIntLitValue (int i) /*@*/;
bool constraintTerm_isIntLiteral (constraintTerm term) /*@*/;
cstring constraintTerm_print (constraintTerm term) /*@*/;
-constraintTerm constraintTerm_makesRef (/*@only@*/ sRef s) /*@*/;
+constraintTerm constraintTerm_makesRef (/*@temp@*/ /*@observer@*/ sRef s) /*@*/;
/*@unused@*/ bool constraintTerm_probSame (constraintTerm term1, constraintTerm term2) /*@*/;
constraintTerm constraintTerm_doSRefFixBaseParam (/*@returned@*/ constraintTerm term, exprNodeList arglist) /*@modifies term@*/;
+void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f);
+
+/*@only@*/ constraintTerm constraintTerm_undump ( FILE *f);
+
+/*@=namechecks@*/
+
#else
#error Multiple Include