2 ** LCLint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2001 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 lclint: lclint-request@cs.virginia.edu
21 ** To report a bug: lclint-bug@cs.virginia.edu
22 ** For more information: http://lclint.cs.virginia.edu
29 /* #define DEBUGPRINT 1 */
31 # include <ctype.h> /* for isdigit */
32 # include "lclintMacros.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) )
738 voptgenerror (FLG_ARRAYBOUNDS, string, errorLoc);
740 voptgenerror (FLG_ARRAYBOUNDSREAD, string, errorLoc);
743 fileloc_free(errorLoc);
748 static cstring constraint_printDeep (constraint c)
751 cstring st = cstring_undefined;
753 st = constraint_print(c);
756 if (c->orig != constraint_undefined)
758 st = cstring_appendChar(st, '\n');
759 genExpr = exprNode_unparse(c->orig->generatingExpr);
763 st = cstring_concatFree(st, (message(" derived from %s precondition: %q", genExpr, constraint_printDeep(c->orig) )
766 st = cstring_concatFree(st,(message(" needed to satisfy precondition:\n%q",
767 constraint_printDeep(c->orig) )
773 st = cstring_concatFree(st,(message("derived from: %q",
774 constraint_printDeep(c->orig) )
784 static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
786 cstring st = cstring_undefined;
789 st = message ("Unsatisfied ensures constraint condition:\nLCLint is unable to verify the constraint %q", constraint_printDeep (c) );
791 genExpr = exprNode_unparse (c->generatingExpr);
793 if (context_getFlag (FLG_CONSTRAINTLOCATION) )
797 temp = message ("\nOriginal Generating expression %q: %s\n",
798 fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
800 st = cstring_concatFree (st, temp);
802 if (constraint_hasMaxSet(c) )
804 temp = message ("Has MaxSet\n");
805 st = cstring_concatFree (st, temp);
811 cstring constraint_printDetailed (constraint c)
813 cstring st = cstring_undefined;
814 cstring temp = cstring_undefined;
819 st = message ("Unable to resolve constraint:\n%q", constraint_printDeep (c) );
823 st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c) );
826 if (constraint_hasMaxSet(c) )
828 temp = cstring_makeLiteral("Possible out-of-bounds store:\n");
832 temp = cstring_makeLiteral("Possible out-of-bounds read:\n");
835 genExpr = exprNode_unparse (c->generatingExpr);
837 if (context_getFlag (FLG_CONSTRAINTLOCATION) )
840 temp2 = message ("%s\n", genExpr );
841 temp = cstring_concatFree (temp, temp2);
844 st = cstring_concatFree(temp,st);
849 /*@only@*/ cstring constraint_print (constraint c) /*@*/
851 cstring st = cstring_undefined;
852 cstring type = cstring_undefined;
856 if (context_getFlag (FLG_PARENCONSTRAINT) )
858 type = cstring_makeLiteral ("ensures: ");
862 type = cstring_makeLiteral ("ensures");
867 if (context_getFlag (FLG_PARENCONSTRAINT) )
869 type = cstring_makeLiteral ("requires: ");
873 type = cstring_makeLiteral ("requires");
877 if (context_getFlag (FLG_PARENCONSTRAINT) )
879 st = message ("%q: %q %q %q",
881 constraintExpr_print (c->lexpr),
882 arithType_print(c->ar),
883 constraintExpr_print(c->expr)
888 st = message ("%q %q %q %q",
890 constraintExpr_print (c->lexpr),
891 arithType_print(c->ar),
892 constraintExpr_print(c->expr)
898 cstring constraint_printOr (constraint c) /*@*/
903 ret = cstring_undefined;
906 ret = cstring_concatFree (ret, constraint_print(temp) );
910 while ( constraint_isDefined(temp) )
912 ret = cstring_concatFree (ret, cstring_makeLiteral (" OR ") );
913 ret = cstring_concatFree (ret, constraint_print(temp) );
921 /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
922 exprNodeList arglist)
924 precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
926 precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
933 constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exprNode fcnCall)
935 postcondition = constraint_copy (postcondition);
936 postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
937 postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
939 return postcondition;
942 /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
943 exprNodeList arglist)
946 precondition = constraint_copy (precondition);
947 precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
948 precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
950 precondition->fcnPre = FALSE;
954 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
957 DPRINTF( (message("Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
959 if (c->orig == constraint_undefined)
960 c->orig = constraint_copy (c);
962 else if (c->orig->fcnPre)
968 /* avoid infinite loop */
970 c->orig = constraint_copy (c);
971 if (c->orig->orig == NULL)
973 c->orig->orig = temp;
978 llcontbug((message("Expected c->orig->orig to be null" ) ));
979 constraint_free(c->orig->orig);
980 c->orig->orig = temp;
986 DPRINTF( (message("Not changing constraint") ));
989 DPRINTF( (message("After Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
998 constraint constraint_togglePost (/*@returned@*/ constraint c)
1004 constraint constraint_togglePostOrig (/*@returned@*/ constraint c)
1006 if (c->orig != NULL)
1007 c->orig = constraint_togglePost(c->orig);
1011 bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint c)
1013 if (c->orig == NULL)
1020 constraint constraint_undump (FILE *f)
1027 constraintExpr lexpr;
1028 constraintExpr expr;
1035 s = mstring_create (MAX_DUMP_LINE_LENGTH);
1039 s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1041 /*@i33*/ /*this should probably be wrappered...*/
1043 fcnPre = (bool) reader_getInt (&s);
1045 post = (bool) reader_getInt (&s);
1047 ar = (arithType) reader_getInt (&s);
1049 s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1051 reader_checkChar (&s, 'l');
1053 lexpr = constraintExpr_undump (f);
1055 s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1057 reader_checkChar (&s, 'r');
1058 expr = constraintExpr_undump (f);
1060 c = constraint_makeNew();
1070 c = constraint_preserveOrig(c);
1075 void constraint_dump (/*@observer@*/ constraint c, FILE *f)
1081 constraintExpr lexpr;
1082 constraintExpr expr;
1091 fprintf(f, "%d@%d@%d\n", (int) fcnPre, (int) post, (int) ar);
1093 constraintExpr_dump (lexpr, f);
1095 constraintExpr_dump (expr, f);
1099 int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * c1, /*@observer@*/ /*@temp@*/ const constraint * c2) /*@*/
1105 llassert(constraint_isDefined(*c1) );
1106 llassert(constraint_isDefined(*c2) );
1108 if (constraint_isUndefined(*c1) )
1110 if (constraint_isUndefined(*c2) )
1116 if (constraint_isUndefined(*c2) )
1121 loc1 = constraint_getFileloc(*c1);
1122 loc2 = constraint_getFileloc(*c2);
1124 ret = fileloc_compare(loc1, loc2);
1133 bool constraint_isPost (/*@observer@*/ /*@temp@*/ constraint c)
1135 llassert(constraint_isDefined(c) );
1137 if (constraint_isUndefined(c) )
1144 static int constraint_getDepth(/*@observer@*/ /*@temp@*/ constraint c)
1148 l = constraintExpr_getDepth(c->lexpr);
1149 r = constraintExpr_getDepth(c->expr);
1153 DPRINTF(( message("constraint depth returning %d for %s", l, constraint_print(c) ) ));
1158 DPRINTF(( message("constraint depth returning %d for %s", r, constraint_print(c) ) ));
1164 bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint c)
1168 temp = constraint_getDepth(c);