7 # include <ctype.h> /* for isdigit */
8 # include "lclintMacros.nf"
10 # include "cgrammar.h"
11 # include "cgrammar_tokens.h"
13 # include "exprChecks.h"
14 # include "exprNodeSList.h"
18 /*@access exprNode @*/
21 static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
24 static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
25 /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/
26 /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
28 /* constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant) */
34 /* ret = constraint_makeNew(); */
35 /* llassert (sRef_isValid(x) ); */
36 /* if (!sRef_isValid(x)) */
40 /* ret->lexpr = constraintExpr_makeTermsRef (x); */
41 /* #warning fix abstraction */
43 /* if (relOp.tok == GE_OP) */
45 /* else if (relOp.tok == LE_OP) */
47 /* else if (relOp.tok == EQ_OP) */
50 /* llfatalbug(message ("Unsupported relational operator") ); */
53 /* t = cstring_toCharsSafe (exprNode_unparse(cconstant)); */
55 /* ret->expr = constraintExpr_makeIntLiteral (c); */
57 /* ret->post = TRUE; */
58 /* // ret->orig = ret; */
59 /* DPRINTF(("GENERATED CONSTRAINT:")); */
60 /* DPRINTF( (message ("%s", constraint_print(ret) ) ) ); */
66 advanceField (char **s)
68 reader_checkChar (s, '@');
73 static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
78 ret = constraint_makeNew ();
79 llassert (constraintExpr_isDefined(l) );
81 ret->lexpr = constraintExpr_copy (l);
84 if (relOp.tok == GE_OP)
86 else if (relOp.tok == LE_OP)
88 else if (relOp.tok == EQ_OP)
91 llfatalbug(message("Unsupported relational operator") );
94 t = cstring_toCharsSafe (exprNode_unparse(cconstant));
96 ret->expr = constraintExpr_makeIntLiteral (c);
100 DPRINTF(("GENERATED CONSTRAINT:"));
101 DPRINTF( (message ("%s", constraint_print(ret) ) ) );
105 bool constraint_same (constraint c1, constraint c2)
108 if (c1->ar != c2->ar)
111 if (!constraintExpr_similar (c1->lexpr, c2->lexpr) )
114 if (!constraintExpr_similar (c1->expr, c2->expr) )
120 constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
123 ret = constraint_makeNew();
124 llassert (constraintExpr_isDefined(l) );
126 ret->lexpr = constraintExpr_copy (l);
128 if (relOp.tok == GE_OP)
130 else if (relOp.tok == LE_OP)
132 else if (relOp.tok == EQ_OP)
135 llfatalbug( message("Unsupported relational operator") );
137 ret->expr = constraintExpr_copy (r);
141 ret->orig = constraint_copy(ret);
143 ret = constraint_simplify (ret);
146 DPRINTF(("GENERATED CONSTRAINT:"));
147 DPRINTF( (message ("%s", constraint_print(ret) ) ) );
151 constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
155 llassert (constraint_isDefined(c) );
156 // DPRINTF((message("Copying constraint %q", constraint_print) ));
158 ret = constraint_makeNew();
159 ret->lexpr = constraintExpr_copy (c->lexpr);
161 ret->expr = constraintExpr_copy (c->expr);
164 ret->generatingExpr = c->generatingExpr;
169 ret->orig = constraint_copy (c->orig);
174 ret->or = constraint_copy (c->or);
178 ret->fcnPre = c->fcnPre;
183 /*like copy expect it doesn't allocate memory for the constraint*/
185 void constraint_overWrite (constraint c1, constraint c2)
187 llassert (constraint_isDefined(c1) );
191 DPRINTF((message("OverWriteing constraint %q with %q", constraint_print(c1),
192 constraint_print(c2) ) ));
194 constraintExpr_free(c1->lexpr);
195 constraintExpr_free(c1->expr);
197 c1->lexpr = constraintExpr_copy (c2->lexpr);
199 c1->expr = constraintExpr_copy (c2->expr);
202 if (c1->orig != NULL)
203 constraint_free (c1->orig);
205 if (c2->orig != NULL)
206 c1->orig = constraint_copy (c2->orig);
210 /*@i33 make sure that the or is freed correctly*/
212 constraint_free (c1->or);
215 c1->or = constraint_copy (c2->or);
219 c1->fcnPre = c2->fcnPre;
222 c1->generatingExpr = c2->generatingExpr;
228 static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
229 /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/
230 /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
233 ret = dmalloc(sizeof (*ret) );
240 ret->generatingExpr = NULL;
245 constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e)
248 if (c->generatingExpr == NULL)
250 c->generatingExpr = e;
251 DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
255 DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
260 constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
263 if (c->orig != constraint_undefined)
265 c->orig = constraint_addGeneratingExpr(c->orig, e);
269 DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
274 constraint constraint_setFcnPre (/*@returned@*/ constraint c )
277 if (c->orig != constraint_undefined)
279 c->orig->fcnPre = TRUE;
284 // DPRINTF(( message("Warning Setting fcnPre directly") ));
292 fileloc constraint_getFileloc (constraint c)
294 if (exprNode_isDefined(c->generatingExpr) )
295 return (fileloc_copy (exprNode_getfileloc (c->generatingExpr) ) );
297 return (constraintExpr_getFileloc (c->lexpr) );
302 static bool checkForMaxSet (constraint c)
304 if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) )
310 bool constraint_hasMaxSet(constraint c)
312 if (checkForMaxSet(c) )
317 if (checkForMaxSet(c->orig) )
324 constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
326 constraint ret = constraint_makeNew();
327 // constraintTerm term;
330 ret->lexpr = constraintExpr_makeMaxReadExpr(po);
332 ret->expr = constraintExpr_makeValueExpr (ind);
337 constraint constraint_makeWriteSafeInt ( exprNode po, int ind)
339 constraint ret = constraint_makeNew();
342 ret->lexpr =constraintExpr_makeMaxSetExpr(po);
344 ret->expr = constraintExpr_makeIntLiteral (ind);
348 constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
350 constraint ret = constraint_makeNew();
351 ret->lexpr = constraintExpr_makeSRefMaxset (s);
353 ret->expr = constraintExpr_makeIntLiteral ((int)size);
358 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
360 constraint ret = constraint_makeNew();
363 ret->lexpr = constraintExpr_makeSRefMaxset ( s );
365 ret->expr = constraintExpr_makeIntLiteral (ind);
370 /* drl added 01/12/2000
372 makes the constraint: Ensures index <= MaxRead(buffer) */
374 constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer)
376 constraint ret = constraint_makeNew();
378 ret->lexpr = constraintExpr_makeValueExpr (index);
380 ret->expr = constraintExpr_makeMaxReadExpr(buffer);
385 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
387 constraint ret = constraint_makeNew();
390 ret->lexpr =constraintExpr_makeMaxSetExpr(po);
392 ret->expr = constraintExpr_makeValueExpr (ind);
397 constraint constraint_makeReadSafeInt ( exprNode t1, int index)
399 constraint ret = constraint_makeNew();
401 ret->lexpr = constraintExpr_makeMaxReadExpr(t1);
403 ret->expr = constraintExpr_makeIntLiteral (index);
408 constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
410 constraint ret = constraint_makeNew();
413 ret->lexpr = constraintExpr_makeSRefMaxRead (s );
415 ret->expr = constraintExpr_makeIntLiteral (ind);
420 constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
424 ret = constraint_makeReadSafeExprNode(t1, t2);
426 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
430 // fileloc_incColumn (ret->lexpr->term->loc);
434 static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2, fileloc sequencePoint, arithType ar)
439 llassert(constraintExpr_isDefined(c1) && constraintExpr_isDefined(c2) );
440 // llassert(sequencePoint);
442 ret = constraint_makeNew();
448 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
452 static constraint constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode e2, fileloc sequencePoint, arithType ar)
454 constraintExpr c1, c2;
458 if (! (exprNode_isDefined(e1) && exprNode_isDefined(e2) ) )
460 llcontbug((message("null exprNode, Exprnodes are %s and %s",
461 exprNode_unparse(e1), exprNode_unparse(e2) )
465 // llassert (sequencePoint);
468 c1 = constraintExpr_makeValueExpr (e);
471 c2 = constraintExpr_makeValueExpr (e);
473 ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
479 /* make constraint ensures e1 == e2 */
481 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
483 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
486 /*make constraint ensures e1 < e2 */
487 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
489 constraintExpr t1, t2;
491 t1 = constraintExpr_makeValueExpr (e1);
492 t2 = constraintExpr_makeValueExpr (e2);
494 /*change this to e1 <= (e2 -1) */
496 t2 = constraintExpr_makeDecConstraintExpr (t2);
498 return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE) );
501 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
503 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
506 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
508 constraintExpr t1, t2;
510 t1 = constraintExpr_makeValueExpr (e1);
511 t2 = constraintExpr_makeValueExpr (e2);
514 /* change this to e1 >= (e2 + 1) */
515 t2 = constraintExpr_makeIncConstraintExpr (t2);
518 return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE) );
521 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
523 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
527 exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
529 constraintList_free(dst->ensuresConstraints);
530 constraintList_free(dst->requiresConstraints);
531 constraintList_free(dst->trueEnsuresConstraints);
532 constraintList_free(dst->falseEnsuresConstraints);
534 dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
535 dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
536 dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
537 dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
541 /* Makes the constraint e = e + f */
542 constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint)
544 constraintExpr x1, x2, y;
547 ret = constraint_makeNew();
549 x1 = constraintExpr_makeValueExpr (e);
550 x2 = constraintExpr_copy(x1);
551 y = constraintExpr_makeValueExpr (f);
556 ret->expr = constraintExpr_makeAddExpr (x2, y);
558 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
564 /* Makes the constraint e = e - f */
565 constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint)
567 constraintExpr x1, x2, y;
570 ret = constraint_makeNew();
572 x1 = constraintExpr_makeValueExpr (e);
573 x2 = constraintExpr_copy(x1);
574 y = constraintExpr_makeValueExpr (f);
579 ret->expr = constraintExpr_makeSubtractExpr (x2, y);
581 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
586 constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
588 constraint ret = constraint_makeNew();
589 //constraintTerm term;
591 // e = exprNode_fakeCopy(e);
592 ret->lexpr = constraintExpr_makeValueExpr (e);
595 ret->expr = constraintExpr_makeValueExpr (e);
596 ret->expr = constraintExpr_makeDecConstraintExpr (ret->expr);
598 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
599 // fileloc_incColumn ( ret->lexpr->term->loc);
600 // fileloc_incColumn ( ret->lexpr->term->loc);
603 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
605 constraint ret = constraint_makeNew();
606 //constraintTerm term;
608 // e = exprNode_fakeCopy(e);
609 ret->lexpr = constraintExpr_makeValueExpr (e);
612 ret->expr = constraintExpr_makeValueExpr (e);
613 ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr);
615 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
616 // fileloc_incColumn ( ret->lexpr->term->loc);
617 // fileloc_incColumn ( ret->lexpr->term->loc);
622 void constraint_free (/*@only@*/ constraint c)
624 llassert(constraint_isDefined (c) );
627 if (constraint_isDefined(c->orig) )
628 constraint_free (c->orig);
629 if ( constraint_isDefined(c->or) )
630 constraint_free (c->or);
633 constraintExpr_free(c->lexpr);
634 constraintExpr_free(c->expr);
646 // constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
648 // constraint ret = constraint_makeNew();
649 // //constraintTerm term;
651 // e = exprNode_fakeCopy(e);
652 // ret->lexpr = constraintExpr_makeMaxReadExpr(e);
655 // ret->expr = constraintExpr_makeIncConstraintExpr (e);
656 // ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
661 cstring arithType_print (arithType ar) /*@*/
663 cstring st = cstring_undefined;
667 st = cstring_makeLiteral (" < ");
670 st = cstring_makeLiteral (" <= ");
673 st = cstring_makeLiteral (" > ");
676 st = cstring_makeLiteral (" >= ");
679 st = cstring_makeLiteral (" == ");
682 st = cstring_makeLiteral (" NONNEGATIVE ");
685 st = cstring_makeLiteral (" POSITIVE ");
694 void constraint_printErrorPostCondition (constraint c, fileloc loc)
697 fileloc errorLoc, temp;
699 string = constraint_printDetailedPostCondition (c);
705 temp = constraint_getFileloc(c);
707 if (fileloc_isDefined(temp) )
710 voptgenerror ( FLG_CHECKPOST, string, errorLoc);
715 voptgenerror ( FLG_CHECKPOST, string, errorLoc);
722 void constraint_printError (constraint c, fileloc loc)
725 fileloc errorLoc, temp;
727 string = constraint_printDetailed (c);
733 temp = constraint_getFileloc(c);
735 if (fileloc_isDefined(temp) )
741 voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
745 if (constraint_hasMaxSet (c) )
746 voptgenerror (FLG_ARRAYBOUNDS, string, errorLoc);
748 voptgenerror (FLG_ARRAYBOUNDSREAD, string, errorLoc);
757 voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
761 voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
768 static cstring constraint_printDeep (constraint c)
771 cstring st = cstring_undefined;
773 st = constraint_print(c);
776 if (c->orig != constraint_undefined)
778 st = cstring_appendChar(st, '\n');
779 genExpr = exprNode_unparse(c->orig->generatingExpr);
783 st = cstring_concatFree(st, (message(" derived from %s precondition: %q", genExpr, constraint_printDeep(c->orig) )
786 st = cstring_concatFree(st,(message(" needed to satisfy precondition:\n%q",
787 constraint_printDeep(c->orig) )
793 st = cstring_concatFree(st,(message("derived from: %q",
794 constraint_printDeep(c->orig) )
804 static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
806 cstring st = cstring_undefined;
809 st = message ("Unsatisfied ensures constraint condition:\nLCLint is unable to verify the constraint %q", constraint_printDeep (c) );
811 genExpr = exprNode_unparse (c->generatingExpr);
813 if (context_getFlag (FLG_CONSTRAINTLOCATION) )
816 // llassert (c->generatingExpr);
817 temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
819 st = cstring_concatFree (st, temp);
821 if (constraint_hasMaxSet(c) )
823 temp = message ("Has MaxSet\n");
824 st = cstring_concatFree (st, temp);
830 cstring constraint_printDetailed (constraint c)
832 cstring st = cstring_undefined;
833 cstring temp = cstring_undefined;
838 st = message ("Unable to resolve constraint:\n%q", constraint_printDeep (c) );
842 st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c) );
845 if (constraint_hasMaxSet(c) )
847 temp = cstring_makeLiteral("Possible out-of-bounds store. ");
851 temp = cstring_makeLiteral("Possible out-of-bounds read. ");
854 st = cstring_concatFree(temp,st);
856 genExpr = exprNode_unparse (c->generatingExpr);
858 if (context_getFlag (FLG_CONSTRAINTLOCATION) )
860 temp = message ("\nConstraint generated from expression: %s at %q\n",
862 fileloc_unparse( exprNode_getfileloc (c->generatingExpr) )
864 st = cstring_concatFree (st, temp);
869 /*@only@*/ cstring constraint_print (constraint c) /*@*/
871 cstring st = cstring_undefined;
872 cstring type = cstring_undefined;
876 type = cstring_makeLiteral ("ensures: ");
880 type = cstring_makeLiteral ("requires: ");
882 st = message ("%q: %q %q %q",
884 constraintExpr_print (c->lexpr),
885 arithType_print(c->ar),
886 constraintExpr_print(c->expr)
891 cstring constraint_printOr (constraint c) /*@*/
896 ret = cstring_undefined;
899 ret = cstring_concatFree (ret, constraint_print(temp) );
903 while ( constraint_isDefined(temp) )
905 ret = cstring_concatFree (ret, cstring_makeLiteral (" OR ") );
906 ret = cstring_concatFree (ret, constraint_print(temp) );
914 /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
915 exprNodeList arglist)
917 precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
919 precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
926 constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exprNode fcnCall)
928 postcondition = constraint_copy (postcondition);
929 postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
930 postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
932 return postcondition;
935 /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
936 exprNodeList arglist)
939 precondition = constraint_copy (precondition);
940 precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
941 precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
943 precondition->fcnPre = FALSE;
947 // bool constraint_hasTerm (constraint c, constraintTerm term)
949 // DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
951 // if (constraintExpr_includesTerm (c->lexpr, term) )
954 // if (constraintExpr_includesTerm (c->expr, term) )
960 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
963 DPRINTF( (message("Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
965 if (c->orig == constraint_undefined)
966 c->orig = constraint_copy (c);
968 else if (c->orig->fcnPre)
974 /* avoid infinite loop */
976 c->orig = constraint_copy (c);
977 if (c->orig->orig == NULL)
979 c->orig->orig = temp;
984 llcontbug((message("Expected c->orig->orig to be null" ) ));
985 constraint_free(c->orig->orig);
986 c->orig->orig = temp;
992 DPRINTF( (message("Not changing constraint") ));
995 DPRINTF( (message("After Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
1004 constraint constraint_togglePost (/*@returned@*/ constraint c)
1010 constraint constraint_togglePostOrig (/*@returned@*/ constraint c)
1012 if (c->orig != NULL)
1013 c->orig = constraint_togglePost(c->orig);
1017 bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint c)
1019 if (c->orig == NULL)
1026 constraint constraint_undump (FILE *f)
1033 constraintExpr lexpr;
1034 constraintExpr expr;
1041 s = mstring_create (MAX_DUMP_LINE_LENGTH);
1045 s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1047 /*@i33*/ /*this should probably be wrappered...*/
1049 fcnPre = (bool) reader_getInt (&s);
1051 post = (bool) reader_getInt (&s);
1053 ar = (arithType) reader_getInt (&s);
1055 s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1057 reader_checkChar (&s, 'l');
1059 lexpr = constraintExpr_undump (f);
1061 s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1063 reader_checkChar (&s, 'r');
1064 expr = constraintExpr_undump (f);
1066 c = constraint_makeNew();
1080 void constraint_dump (/*@observer@*/ constraint c, FILE *f)
1086 constraintExpr lexpr;
1087 constraintExpr expr;
1096 fprintf(f, "%d@%d@%d\n", (int) fcnPre, (int) post, (int) ar);
1098 constraintExpr_dump (lexpr, f);
1100 constraintExpr_dump (expr, f);
1104 int constraint_compare (/*@observer@*/ /*@temp@*/ constraint * c1, /*@observer@*/ /*@temp@*/ constraint * c2) /*@*/
1110 llassert(constraint_isDefined(*c1) );
1111 llassert(constraint_isDefined(*c2) );
1113 if (constraint_isUndefined(*c1) )
1115 if (constraint_isUndefined(*c2) )
1121 if (constraint_isUndefined(*c2) )
1126 loc1 = constraint_getFileloc(*c1);
1127 loc2 = constraint_getFileloc(*c2);
1129 ret = fileloc_compare(loc1, loc2);