2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2002 University of Virginia,
4 ** Massachusetts Institute of Technology
6 ** This program is free software; you can redistribute it and/or modify it
7 ** under the terms of the GNU General Public License as published by the
8 ** Free Software Foundation; either version 2 of the License, or (at your
9 ** option) any later version.
11 ** This program is distributed in the hope that it will be useful, but
12 ** WITHOUT ANY WARRANTY; without even the implied warranty of
13 ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
14 ** General Public License for more details.
16 ** The GNU General Public License is available from http://www.gnu.org/ or
17 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
18 ** MA 02111-1307, USA.
20 ** For information on splint: splint@cs.virginia.edu
21 ** To report a bug: splint-bug@cs.virginia.edu
22 ** For more information: http://www.splint.org
29 /* #define DEBUGPRINT 1 */
31 # include <ctype.h> /* for isdigit */
32 # include "splintMacros.nf"
34 # include "cgrammar.h"
35 # include "cgrammar_tokens.h"
37 # include "exprChecks.h"
38 # include "exprNodeSList.h"
42 /*@access exprNode @*/
45 static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
48 static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
49 /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/
50 /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
53 advanceField (char **s)
55 reader_checkChar (s, '@');
59 static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
64 ret = constraint_makeNew ();
65 llassert (constraintExpr_isDefined (l));
67 ret->lexpr = constraintExpr_copy (l);
70 if (relOp.tok == GE_OP)
72 else if (relOp.tok == LE_OP)
74 else if (relOp.tok == EQ_OP)
77 llfatalbug (message ("Unsupported relational operator"));
80 t = cstring_toCharsSafe (exprNode_unparse (cconstant));
82 ret->expr = constraintExpr_makeIntLiteral (c);
85 DPRINTF (("GENERATED CONSTRAINT:"));
86 DPRINTF ((message ("%s", constraint_print (ret))));
91 bool constraint_same (constraint c1, constraint c2)
93 llassert (c1 != NULL);
94 llassert (c2 != NULL);
101 if (!constraintExpr_similar (c1->lexpr, c2->lexpr))
106 if (!constraintExpr_similar (c1->expr, c2->expr))
114 constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
117 ret = constraint_makeNew ();
118 llassert (constraintExpr_isDefined (l));
120 ret->lexpr = constraintExpr_copy (l);
122 if (relOp.tok == GE_OP)
124 else if (relOp.tok == LE_OP)
126 else if (relOp.tok == EQ_OP)
129 llfatalbug ( message ("Unsupported relational operator"));
131 ret->expr = constraintExpr_copy (r);
135 ret->orig = constraint_copy (ret);
137 ret = constraint_simplify (ret);
138 /* ret->orig = ret; */
140 DPRINTF (("GENERATED CONSTRAINT:"));
141 DPRINTF ((message ("%s", constraint_print (ret))));
145 constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
149 llassert (constraint_isDefined (c));
151 ret = constraint_makeNew ();
152 ret->lexpr = constraintExpr_copy (c->lexpr);
154 ret->expr = constraintExpr_copy (c->expr);
157 ret->generatingExpr = c->generatingExpr;
162 ret->orig = constraint_copy (c->orig);
167 ret->or = constraint_copy (c->or);
171 ret->fcnPre = c->fcnPre;
176 /*like copy expect it doesn't allocate memory for the constraint*/
178 void constraint_overWrite (constraint c1, constraint c2)
180 llassert (constraint_isDefined (c1));
184 DPRINTF ((message ("OverWriteing constraint %q with %q", constraint_print (c1),
185 constraint_print (c2))));
187 constraintExpr_free (c1->lexpr);
188 constraintExpr_free (c1->expr);
190 c1->lexpr = constraintExpr_copy (c2->lexpr);
192 c1->expr = constraintExpr_copy (c2->expr);
195 if (c1->orig != NULL)
196 constraint_free (c1->orig);
198 if (c2->orig != NULL)
199 c1->orig = constraint_copy (c2->orig);
203 /*@i33 make sure that the or is freed correctly*/
205 constraint_free (c1->or);
208 c1->or = constraint_copy (c2->or);
212 c1->fcnPre = c2->fcnPre;
215 c1->generatingExpr = c2->generatingExpr;
221 static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
222 /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/
223 /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
226 ret = dmalloc (sizeof (*ret));
233 ret->generatingExpr = NULL;
238 constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e)
241 if (c->generatingExpr == NULL)
243 c->generatingExpr = e;
244 DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print (c), exprNode_unparse (e)) ));
248 DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print (c), exprNode_unparse (e)) ));
253 constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
256 if (c->orig != constraint_undefined)
258 c->orig = constraint_addGeneratingExpr (c->orig, e);
262 DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_print (c), exprNode_unparse (e)) ));
267 constraint constraint_setFcnPre (/*@returned@*/ constraint c)
270 if (c->orig != constraint_undefined)
272 c->orig->fcnPre = TRUE;
277 DPRINTF (( message ("Warning Setting fcnPre directly")));
285 fileloc constraint_getFileloc (constraint c)
287 if (exprNode_isDefined (c->generatingExpr))
288 return (fileloc_copy (exprNode_getfileloc (c->generatingExpr)));
290 return (constraintExpr_getFileloc (c->lexpr));
295 static bool checkForMaxSet (constraint c)
297 if (constraintExpr_hasMaxSet (c->lexpr) || constraintExpr_hasMaxSet (c->expr))
303 bool constraint_hasMaxSet (constraint c)
305 if (checkForMaxSet (c))
310 if (checkForMaxSet (c->orig))
317 constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
319 constraint ret = constraint_makeNew ();
323 ret->lexpr = constraintExpr_makeMaxReadExpr (po);
325 ret->expr = constraintExpr_makeValueExpr (ind);
330 constraint constraint_makeWriteSafeInt ( exprNode po, int ind)
332 constraint ret = constraint_makeNew ();
335 ret->lexpr =constraintExpr_makeMaxSetExpr (po);
337 ret->expr = constraintExpr_makeIntLiteral (ind);
341 constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
343 constraint ret = constraint_makeNew ();
344 ret->lexpr = constraintExpr_makeSRefMaxset (s);
346 ret->expr = constraintExpr_makeIntLiteral ((int)size);
351 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
353 constraint ret = constraint_makeNew ();
356 ret->lexpr = constraintExpr_makeSRefMaxset ( s);
358 ret->expr = constraintExpr_makeIntLiteral (ind);
363 /* drl added 01/12/2000
365 makes the constraint: Ensures index <= MaxRead (buffer) */
367 constraint constraint_makeEnsureLteMaxRead (exprNode index, exprNode buffer)
369 constraint ret = constraint_makeNew ();
371 ret->lexpr = constraintExpr_makeValueExpr (index);
373 ret->expr = constraintExpr_makeMaxReadExpr (buffer);
378 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
380 constraint ret = constraint_makeNew ();
383 ret->lexpr =constraintExpr_makeMaxSetExpr (po);
385 ret->expr = constraintExpr_makeValueExpr (ind);
390 constraint constraint_makeReadSafeInt ( exprNode t1, int index)
392 constraint ret = constraint_makeNew ();
394 ret->lexpr = constraintExpr_makeMaxReadExpr (t1);
396 ret->expr = constraintExpr_makeIntLiteral (index);
401 constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
403 constraint ret = constraint_makeNew ();
406 ret->lexpr = constraintExpr_makeSRefMaxRead (s);
408 ret->expr = constraintExpr_makeIntLiteral (ind);
413 constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
417 ret = constraint_makeReadSafeExprNode (t1, t2);
418 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
424 static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2, fileloc sequencePoint, arithType ar)
429 llassert (constraintExpr_isDefined (c1) && constraintExpr_isDefined (c2));
431 ret = constraint_makeNew ();
437 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
441 static constraint constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode e2, fileloc sequencePoint, arithType ar)
443 constraintExpr c1, c2;
447 if (! (exprNode_isDefined (e1) && exprNode_isDefined (e2)))
449 llcontbug ((message ("null exprNode, Exprnodes are %s and %s",
450 exprNode_unparse (e1), exprNode_unparse (e2))
455 c1 = constraintExpr_makeValueExpr (e);
458 c2 = constraintExpr_makeValueExpr (e);
460 ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
466 /* make constraint ensures e1 == e2 */
468 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
470 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ));
473 /*make constraint ensures e1 < e2 */
474 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
476 constraintExpr t1, t2;
478 t1 = constraintExpr_makeValueExpr (e1);
479 t2 = constraintExpr_makeValueExpr (e2);
481 /*change this to e1 <= (e2 -1) */
483 t2 = constraintExpr_makeDecConstraintExpr (t2);
485 return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE));
488 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
490 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE));
493 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
495 constraintExpr t1, t2;
497 t1 = constraintExpr_makeValueExpr (e1);
498 t2 = constraintExpr_makeValueExpr (e2);
501 /* change this to e1 >= (e2 + 1) */
502 t2 = constraintExpr_makeIncConstraintExpr (t2);
505 return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE));
508 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
510 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE));
514 exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
516 constraintList_free (dst->ensuresConstraints);
517 constraintList_free (dst->requiresConstraints);
518 constraintList_free (dst->trueEnsuresConstraints);
519 constraintList_free (dst->falseEnsuresConstraints);
521 dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints);
522 dst->requiresConstraints = constraintList_copy (src->requiresConstraints);
523 dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints);
524 dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints);
528 /* Makes the constraint e = e + f */
529 constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint)
531 constraintExpr x1, x2, y;
534 ret = constraint_makeNew ();
536 x1 = constraintExpr_makeValueExpr (e);
537 x2 = constraintExpr_copy (x1);
538 y = constraintExpr_makeValueExpr (f);
543 ret->expr = constraintExpr_makeAddExpr (x2, y);
545 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
551 /* Makes the constraint e = e - f */
552 constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint)
554 constraintExpr x1, x2, y;
557 ret = constraint_makeNew ();
559 x1 = constraintExpr_makeValueExpr (e);
560 x2 = constraintExpr_copy (x1);
561 y = constraintExpr_makeValueExpr (f);
566 ret->expr = constraintExpr_makeSubtractExpr (x2, y);
568 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
573 constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
575 constraint ret = constraint_makeNew ();
577 ret->lexpr = constraintExpr_makeValueExpr (e);
580 ret->expr = constraintExpr_makeValueExpr (e);
581 ret->expr = constraintExpr_makeDecConstraintExpr (ret->expr);
582 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
585 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
587 constraint ret = constraint_makeNew ();
589 ret->lexpr = constraintExpr_makeValueExpr (e);
592 ret->expr = constraintExpr_makeValueExpr (e);
593 ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr);
595 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
600 void constraint_free (/*@only@*/ constraint c)
602 llassert (constraint_isDefined (c));
605 if (constraint_isDefined (c->orig))
606 constraint_free (c->orig);
607 if ( constraint_isDefined (c->or))
608 constraint_free (c->or);
611 constraintExpr_free (c->lexpr);
612 constraintExpr_free (c->expr);
623 cstring arithType_print (arithType ar) /*@*/
625 cstring st = cstring_undefined;
629 st = cstring_makeLiteral ("<");
632 st = cstring_makeLiteral ("<=");
635 st = cstring_makeLiteral (">");
638 st = cstring_makeLiteral (">=");
641 st = cstring_makeLiteral ("==");
644 st = cstring_makeLiteral ("NONNEGATIVE");
647 st = cstring_makeLiteral ("POSITIVE");
656 void constraint_printErrorPostCondition (constraint c, fileloc loc)
659 fileloc errorLoc, temp;
661 string = constraint_printDetailedPostCondition (c);
667 temp = constraint_getFileloc (c);
669 if (fileloc_isDefined (temp))
672 voptgenerror ( FLG_CHECKPOST, string, errorLoc);
677 voptgenerror ( FLG_CHECKPOST, string, errorLoc);
681 /*drl added 8-11-001*/
682 cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint c) /*@*/
687 string = constraint_print (c);
689 errorLoc = constraint_getFileloc (c);
691 ret = message ("constraint: %q @ %q", string, fileloc_unparse (errorLoc));
693 fileloc_free (errorLoc);
700 void constraint_printError (constraint c, fileloc loc)
703 fileloc errorLoc, temp;
706 /*drl 11/26/2001 avoid printing tautological constraints */
707 if (constraint_isAlwaysTrue (c))
713 string = constraint_printDetailed (c);
717 temp = constraint_getFileloc (c);
719 if (fileloc_isDefined (temp))
726 DPRINTF (("constraint %s had undefined fileloc %s", constraint_print (c), fileloc_unparse (temp)));
728 errorLoc = fileloc_copy (errorLoc);
733 voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
737 if (constraint_hasMaxSet (c))
739 voptgenerror (FLG_BOUNDSWRITE, string, errorLoc);
743 voptgenerror (FLG_BOUNDSREAD, string, errorLoc);
747 fileloc_free(errorLoc);
750 static cstring constraint_printDeep (constraint c)
753 cstring st = cstring_undefined;
755 st = constraint_print(c);
757 if (c->orig != constraint_undefined)
759 st = cstring_appendChar (st, '\n');
760 genExpr = exprNode_unparse (c->orig->generatingExpr);
766 st = cstring_concatFree (st, message (" derived from %s precondition: %q",
767 genExpr, constraint_printDeep (c->orig)));
771 st = cstring_concatFree (st, message (" needed to satisfy precondition:\n%q",
772 constraint_printDeep (c->orig)));
777 st = cstring_concatFree (st, message ("derived from: %q",
778 constraint_printDeep (c->orig)));
786 static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
788 cstring st = cstring_undefined;
791 st = message ("Unsatisfied ensures constraint condition:\nSplint is unable to verify the constraint %q", constraint_printDeep (c));
793 genExpr = exprNode_unparse (c->generatingExpr);
795 if (context_getFlag (FLG_CONSTRAINTLOCATION))
799 temp = message ("\nOriginal Generating expression %q: %s\n",
800 fileloc_unparse ( exprNode_getfileloc (c->generatingExpr)),
802 st = cstring_concatFree (st, temp);
804 if (constraint_hasMaxSet (c))
806 temp = message ("Has MaxSet\n");
807 st = cstring_concatFree (st, temp);
813 cstring constraint_printDetailed (constraint c)
815 cstring st = cstring_undefined;
816 cstring temp = cstring_undefined;
821 st = message ("Unable to resolve constraint:\n%q", constraint_printDeep (c));
825 st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c));
828 if (constraint_hasMaxSet (c))
830 temp = cstring_makeLiteral ("Possible out-of-bounds store:\n");
834 temp = cstring_makeLiteral ("Possible out-of-bounds read:\n");
837 genExpr = exprNode_unparse (c->generatingExpr);
839 if (context_getFlag (FLG_CONSTRAINTLOCATION))
842 temp2 = message ("%s\n", genExpr);
843 temp = cstring_concatFree (temp, temp2);
846 st = cstring_concatFree (temp,st);
851 /*@only@*/ cstring constraint_print (constraint c) /*@*/
853 cstring st = cstring_undefined;
854 cstring type = cstring_undefined;
858 if (context_getFlag (FLG_PARENCONSTRAINT))
860 type = cstring_makeLiteral ("ensures: ");
864 type = cstring_makeLiteral ("ensures");
869 if (context_getFlag (FLG_PARENCONSTRAINT))
871 type = cstring_makeLiteral ("requires: ");
875 type = cstring_makeLiteral ("requires");
879 if (context_getFlag (FLG_PARENCONSTRAINT))
881 st = message ("%q: %q %q %q",
883 constraintExpr_print (c->lexpr),
884 arithType_print (c->ar),
885 constraintExpr_print (c->expr)
890 st = message ("%q %q %q %q",
892 constraintExpr_print (c->lexpr),
893 arithType_print (c->ar),
894 constraintExpr_print (c->expr)
900 cstring constraint_printOr (constraint c) /*@*/
905 ret = cstring_undefined;
908 ret = cstring_concatFree (ret, constraint_print (temp));
912 while ( constraint_isDefined (temp))
914 ret = cstring_concatFree (ret, cstring_makeLiteral (" OR "));
915 ret = cstring_concatFree (ret, constraint_print (temp));
923 /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
924 exprNodeList arglist)
926 precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
928 precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
935 constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exprNode fcnCall)
937 postcondition = constraint_copy (postcondition);
938 postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
939 postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
941 return postcondition;
943 /*Commenting out temporally
945 / *@only@* /constraint constraint_doSRefFixInvarConstraint(constraint invar, sRef s, ctype ct )
948 invar = constraint_copy (invar);
949 invar->lexpr = constraintExpr_doSRefFixInvarConstraint (invar->lexpr, s, ct);
950 invar->expr = constraintExpr_doSRefFixInvarConstraint (invar->expr, s, ct);
956 /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
957 exprNodeList arglist)
960 precondition = constraint_copy (precondition);
961 precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
962 precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
964 precondition->fcnPre = FALSE;
968 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
971 DPRINTF ((message ("Doing constraint_preserverOrig for %q ", constraint_printDetailed (c))));
973 if (c->orig == constraint_undefined)
974 c->orig = constraint_copy (c);
976 else if (c->orig->fcnPre)
982 /* avoid infinite loop */
984 c->orig = constraint_copy (c);
985 if (c->orig->orig == NULL)
987 c->orig->orig = temp;
992 llcontbug ((message ("Expected c->orig->orig to be null")));
993 constraint_free (c->orig->orig);
994 c->orig->orig = temp;
1000 DPRINTF ((message ("Not changing constraint")));
1003 DPRINTF ((message ("After Doing constraint_preserverOrig for %q ", constraint_printDetailed (c))));
1012 constraint constraint_togglePost (/*@returned@*/ constraint c)
1018 constraint constraint_togglePostOrig (/*@returned@*/ constraint c)
1020 if (c->orig != NULL)
1021 c->orig = constraint_togglePost (c->orig);
1025 bool constraint_hasOrig ( /*@observer@*/ /*@temp@*/ constraint c)
1027 if (c->orig == NULL)
1034 constraint constraint_undump (FILE *f)
1041 constraintExpr lexpr;
1042 constraintExpr expr;
1049 os = mstring_create (MAX_DUMP_LINE_LENGTH);
1051 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1053 /*@i33*/ /*this should probably be wrappered...*/
1055 fcnPre = (bool) reader_getInt (&s);
1057 post = (bool) reader_getInt (&s);
1059 ar = (arithType) reader_getInt (&s);
1061 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1063 reader_checkChar (&s, 'l');
1065 lexpr = constraintExpr_undump (f);
1067 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1069 reader_checkChar (&s, 'r');
1070 expr = constraintExpr_undump (f);
1072 c = constraint_makeNew ();
1082 c = constraint_preserveOrig (c);
1087 void constraint_dump (/*@observer@*/ constraint c, FILE *f)
1093 constraintExpr lexpr;
1094 constraintExpr expr;
1103 fprintf (f, "%d@%d@%d\n", (int) fcnPre, (int) post, (int) ar);
1105 constraintExpr_dump (lexpr, f);
1107 constraintExpr_dump (expr, f);
1111 int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * c1, /*@observer@*/ /*@temp@*/ const constraint * c2) /*@*/
1117 llassert (constraint_isDefined (*c1));
1118 llassert (constraint_isDefined (*c2));
1120 if (constraint_isUndefined (*c1))
1122 if (constraint_isUndefined (*c2))
1128 if (constraint_isUndefined (*c2))
1133 loc1 = constraint_getFileloc (*c1);
1134 loc2 = constraint_getFileloc (*c2);
1136 ret = fileloc_compare (loc1, loc2);
1138 fileloc_free (loc1);
1139 fileloc_free (loc2);
1145 bool constraint_isPost (/*@observer@*/ /*@temp@*/ constraint c)
1147 llassert (constraint_isDefined (c));
1149 if (constraint_isUndefined (c))
1156 static int constraint_getDepth (/*@observer@*/ /*@temp@*/ constraint c)
1160 l = constraintExpr_getDepth (c->lexpr);
1161 r = constraintExpr_getDepth (c->expr);
1165 DPRINTF (( message ("constraint depth returning %d for %s", l, constraint_print (c))));
1170 DPRINTF (( message ("constraint depth returning %d for %s", r, constraint_print (c))));
1176 bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint c)
1180 temp = constraint_getDepth (c);