2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 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: info@splint.org
21 ** To report a bug: splint-bug@splint.org
22 ** For more information: http://www.splint.org
29 /* #define DEBUGPRINT 1 */
31 # include "splintMacros.nf"
33 # include "cgrammar.h"
34 # include "cgrammar_tokens.h"
35 # include "exprChecks.h"
36 # include "exprNodeSList.h"
38 static /*@only@*/ cstring
39 constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
41 static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
42 /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/
43 /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
46 advanceField (char **s)
48 reader_checkChar (s, '@');
51 bool constraint_same (constraint c1, constraint c2)
53 llassert (c1 != NULL);
54 llassert (c2 != NULL);
61 if (!constraintExpr_similar (c1->lexpr, c2->lexpr))
66 if (!constraintExpr_similar (c1->expr, c2->expr))
74 constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
77 ret = constraint_makeNew ();
78 llassert (constraintExpr_isDefined (l));
80 ret->lexpr = constraintExpr_copy (l);
82 if (lltok_getTok (relOp) == GE_OP)
86 else if (lltok_getTok (relOp) == LE_OP)
90 else if (lltok_getTok (relOp) == EQ_OP)
95 llfatalbug ( message ("Unsupported relational operator"));
97 ret->expr = constraintExpr_copy (r);
101 ret->orig = constraint_copy (ret);
103 ret = constraint_simplify (ret);
104 /* ret->orig = ret; */
106 DPRINTF (("GENERATED CONSTRAINT:"));
107 DPRINTF ((message ("%s", constraint_unparse (ret))));
111 constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
113 if (!constraint_isDefined (c))
115 return constraint_undefined;
119 constraint ret = constraint_makeNew ();
120 ret->lexpr = constraintExpr_copy (c->lexpr);
122 ret->expr = constraintExpr_copy (c->expr);
125 ret->generatingExpr = c->generatingExpr;
129 ret->orig = constraint_copy (c->orig);
134 ret->or = constraint_copy (c->or);
138 ret->fcnPre = c->fcnPre;
144 /*like copy except it doesn't allocate memory for the constraint*/
146 void constraint_overWrite (constraint c1, constraint c2)
148 llassert (constraint_isDefined (c1) && constraint_isDefined (c2));
152 DPRINTF ((message ("OverWriteing constraint %q with %q", constraint_unparse (c1),
153 constraint_unparse (c2))));
155 constraintExpr_free (c1->lexpr);
156 constraintExpr_free (c1->expr);
158 c1->lexpr = constraintExpr_copy (c2->lexpr);
160 c1->expr = constraintExpr_copy (c2->expr);
163 if (c1->orig != NULL)
164 constraint_free (c1->orig);
166 if (c2->orig != NULL)
167 c1->orig = constraint_copy (c2->orig);
172 constraint_free (c1->or);
175 c1->or = constraint_copy (c2->or);
179 c1->fcnPre = c2->fcnPre;
182 c1->generatingExpr = c2->generatingExpr;
188 static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
189 /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/
190 /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
193 ret = dmalloc (sizeof (*ret));
200 ret->generatingExpr = NULL;
205 /*@access exprNode@*/
207 constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e)
209 if (!constraint_isDefined (c))
214 if (c->generatingExpr == NULL)
216 c->generatingExpr = e;
217 DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_unparse (c), exprNode_unparse (e)) ));
221 DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_unparse (c), exprNode_unparse (e)) ));
225 /*@noaccess exprNode@*/
227 constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
229 llassert (constraint_isDefined (c) );
231 if (c->orig != constraint_undefined)
233 c->orig = constraint_addGeneratingExpr (c->orig, e);
237 DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_unparse (c), exprNode_unparse (e)) ));
242 constraint constraint_setFcnPre (/*@returned@*/ constraint c)
245 llassert (constraint_isDefined (c) );
247 if (c->orig != constraint_undefined)
249 c->orig->fcnPre = TRUE;
254 DPRINTF (( message ("Warning Setting fcnPre directly")));
262 fileloc constraint_getFileloc (constraint c)
264 llassert (constraint_isDefined (c) );
266 if (exprNode_isDefined (c->generatingExpr))
267 return (fileloc_copy (exprNode_loc (c->generatingExpr)));
269 return (constraintExpr_loc (c->lexpr));
272 static bool checkForMaxSet (constraint c)
274 llassert (constraint_isDefined (c));
275 return (constraintExpr_hasMaxSet (c->lexpr) || constraintExpr_hasMaxSet (c->expr));
278 bool constraint_hasMaxSet (constraint c)
280 llassert (constraint_isDefined (c) );
282 if (checkForMaxSet (c))
287 if (checkForMaxSet (c->orig))
294 constraint constraint_makeReadSafeExprNode (exprNode po, exprNode ind)
296 constraint ret = constraint_makeNew ();
300 ret->lexpr = constraintExpr_makeMaxReadExpr (po);
302 ret->expr = constraintExpr_makeValueExpr (ind);
307 constraint constraint_makeWriteSafeInt (exprNode po, int ind)
309 constraint ret = constraint_makeNew ();
310 ret->lexpr =constraintExpr_makeMaxSetExpr (po);
312 ret->expr = constraintExpr_makeIntLiteral (ind);
316 constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
318 constraint ret = constraint_makeNew ();
319 ret->lexpr = constraintExpr_makeSRefMaxset (s);
321 ret->expr = constraintExpr_makeIntLiteral ((int)size);
326 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
328 constraint ret = constraint_makeNew ();
329 ret->lexpr = constraintExpr_makeSRefMaxset ( s);
331 ret->expr = constraintExpr_makeIntLiteral (ind);
336 /* drl added 01/12/2000
337 ** makes the constraint: Ensures index <= MaxRead (buffer)
340 constraint constraint_makeEnsureLteMaxRead (exprNode index, exprNode buffer)
342 constraint ret = constraint_makeNew ();
344 ret->lexpr = constraintExpr_makeValueExpr (index);
346 ret->expr = constraintExpr_makeMaxReadExpr (buffer);
351 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
353 constraint ret = constraint_makeNew ();
355 ret->lexpr =constraintExpr_makeMaxSetExpr (po);
357 ret->expr = constraintExpr_makeValueExpr (ind);
362 constraint constraint_makeReadSafeInt (exprNode t1, int index)
364 constraint ret = constraint_makeNew ();
366 ret->lexpr = constraintExpr_makeMaxReadExpr (t1);
368 ret->expr = constraintExpr_makeIntLiteral (index);
373 constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
375 constraint ret = constraint_makeNew ();
377 ret->lexpr = constraintExpr_makeSRefMaxRead (s);
379 ret->expr = constraintExpr_makeIntLiteral (ind);
384 constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
386 constraint ret = constraint_makeReadSafeExprNode (t1, t2);
387 llassert (constraint_isDefined (ret));
389 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
396 constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2,
397 fileloc sequencePoint, arithType ar)
399 if (constraintExpr_isDefined (c1) && constraintExpr_isDefined (c2))
401 constraint ret = constraint_makeNew ();
406 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
411 return constraint_undefined;
416 constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode e2,
417 fileloc sequencePoint, arithType ar)
419 constraintExpr c1, c2;
421 if (!(exprNode_isDefined (e1) && exprNode_isDefined (e2)))
423 llcontbug (message ("Invalid exprNode, Exprnodes are %s and %s",
424 exprNode_unparse (e1), exprNode_unparse (e2)));
427 c1 = constraintExpr_makeValueExpr (e1);
428 c2 = constraintExpr_makeValueExpr (e2);
430 return constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
433 /* make constraint ensures e1 == e2 */
435 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
437 return (constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ));
440 /* make constraint ensures e1 < e2 */
441 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
443 constraintExpr t1, t2;
446 t1 = constraintExpr_makeValueExpr (e1);
447 t2 = constraintExpr_makeValueExpr (e2);
449 /* change this to e1 <= (e2 -1) */
451 t2 = constraintExpr_makeDecConstraintExpr (t2);
452 t3 = constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE);
453 t3 = constraint_simplify (t3);
457 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
459 return (constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE));
462 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
464 constraintExpr t1, t2;
467 t1 = constraintExpr_makeValueExpr (e1);
468 t2 = constraintExpr_makeValueExpr (e2);
470 /* change this to e1 >= (e2 + 1) */
471 t2 = constraintExpr_makeIncConstraintExpr (t2);
473 t3 = constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE);
474 t3 = constraint_simplify(t3);
479 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
481 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE));
486 /* Makes the constraint e = e + f */
487 constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint)
489 constraintExpr x1, x2, y;
492 ret = constraint_makeNew ();
494 x1 = constraintExpr_makeValueExpr (e);
495 x2 = constraintExpr_copy (x1);
496 y = constraintExpr_makeValueExpr (f);
501 ret->expr = constraintExpr_makeAddExpr (x2, y);
503 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
509 /* Makes the constraint e = e - f */
510 constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint)
512 constraintExpr x1, x2, y;
515 ret = constraint_makeNew ();
517 x1 = constraintExpr_makeValueExpr (e);
518 x2 = constraintExpr_copy (x1);
519 y = constraintExpr_makeValueExpr (f);
524 ret->expr = constraintExpr_makeSubtractExpr (x2, y);
526 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
531 constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
533 constraint ret = constraint_makeNew ();
535 ret->lexpr = constraintExpr_makeValueExpr (e);
538 ret->expr = constraintExpr_makeValueExpr (e);
539 ret->expr = constraintExpr_makeDecConstraintExpr (ret->expr);
540 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
543 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
545 constraint ret = constraint_makeNew ();
547 ret->lexpr = constraintExpr_makeValueExpr (e);
550 ret->expr = constraintExpr_makeValueExpr (e);
551 ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr);
553 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
558 void constraint_free (/*@only@*/ constraint c)
560 if (constraint_isDefined (c))
562 constraint_free (c->orig);
565 constraint_free (c->or);
568 constraintExpr_free (c->lexpr);
571 constraintExpr_free (c->expr);
578 cstring arithType_print (arithType ar) /*@*/
580 cstring st = cstring_undefined;
584 st = cstring_makeLiteral ("<");
587 st = cstring_makeLiteral ("<=");
590 st = cstring_makeLiteral (">");
593 st = cstring_makeLiteral (">=");
596 st = cstring_makeLiteral ("==");
599 st = cstring_makeLiteral ("NONNEGATIVE");
602 st = cstring_makeLiteral ("POSITIVE");
611 void constraint_printErrorPostCondition (constraint c, fileloc loc)
614 fileloc errorLoc, temp;
616 string = constraint_unparseDetailedPostCondition (c);
620 temp = constraint_getFileloc (c);
622 if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES))
624 string = cstring_replaceChar (string, '\n', ' ');
627 if (fileloc_isDefined (temp))
630 voptgenerror (FLG_CHECKPOST, string, errorLoc);
635 voptgenerror (FLG_CHECKPOST, string, errorLoc);
639 /*drl added 8-11-001*/
640 cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint c) /*@*/
645 string = constraint_unparse (c);
647 errorLoc = constraint_getFileloc (c);
649 ret = message ("constraint: %q @ %q", string, fileloc_unparse (errorLoc));
650 fileloc_free (errorLoc);
657 void constraint_printError (constraint c, fileloc loc)
660 fileloc errorLoc, temp;
664 llassert (constraint_isDefined (c) );
666 /*drl 11/26/2001 avoid printing tautological constraints */
667 if (constraint_isAlwaysTrue (c))
673 string = constraint_unparseDetailed (c);
677 temp = constraint_getFileloc (c);
679 if (fileloc_isDefined (temp))
686 DPRINTF (("constraint %s had undefined fileloc %s",
687 constraint_unparse (c), fileloc_unparse (temp)));
689 errorLoc = fileloc_copy (errorLoc);
693 if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES))
695 string = cstring_replaceChar(string, '\n', ' ');
698 /*drl added 12/19/2002 print
699 a different error fro "likely" bounds-errors*/
701 isLikely = constraint_isConstantOnly (c);
707 voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
711 if (constraint_hasMaxSet (c))
713 voptgenerror (FLG_LIKELYBOUNDSWRITE, string, errorLoc);
717 voptgenerror (FLG_LIKELYBOUNDSREAD, string, errorLoc);
723 voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
727 if (constraint_hasMaxSet (c))
729 voptgenerror (FLG_BOUNDSWRITE, string, errorLoc);
733 voptgenerror (FLG_BOUNDSREAD, string, errorLoc);
737 fileloc_free(errorLoc);
740 static cstring constraint_unparseDeep (constraint c)
745 llassert (constraint_isDefined (c));
746 st = constraint_unparse (c);
748 if (c->orig != constraint_undefined)
750 st = cstring_appendChar (st, '\n');
751 genExpr = exprNode_unparse (c->orig->generatingExpr);
757 st = cstring_concatFree (st, message (" derived from %s precondition: %q",
758 genExpr, constraint_unparseDeep (c->orig)));
762 st = cstring_concatFree (st, message (" needed to satisfy precondition:\n%q",
763 constraint_unparseDeep (c->orig)));
768 st = cstring_concatFree (st, message ("derived from: %q",
769 constraint_unparseDeep (c->orig)));
777 static /*@only@*/ cstring constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
779 cstring st = cstring_undefined;
782 llassert (constraint_isDefined (c) );
784 st = message ("Unsatisfied ensures constraint condition:\nSplint is unable to verify the constraint %q",
785 constraint_unparseDeep (c));
787 genExpr = exprNode_unparse (c->generatingExpr);
789 if (context_getFlag (FLG_CONSTRAINTLOCATION))
793 temp = message ("\nOriginal Generating expression %q: %s\n",
794 fileloc_unparse (exprNode_loc (c->generatingExpr)),
796 st = cstring_concatFree (st, temp);
798 if (constraint_hasMaxSet (c))
800 temp = message ("Has MaxSet\n");
801 st = cstring_concatFree (st, temp);
807 cstring constraint_unparseDetailed (constraint c)
809 cstring st = cstring_undefined;
810 cstring temp = cstring_undefined;
814 llassert (constraint_isDefined (c));
818 st = message ("Unable to resolve constraint:\n%q", constraint_unparseDeep (c));
822 st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_unparseDeep (c));
825 isLikely = constraint_isConstantOnly (c);
829 if (constraint_hasMaxSet (c))
831 temp = cstring_makeLiteral ("Likely out-of-bounds store: ");
835 temp = cstring_makeLiteral ("Likely out-of-bounds read: ");
841 if (constraint_hasMaxSet (c))
843 temp = cstring_makeLiteral ("Possible out-of-bounds store: ");
847 temp = cstring_makeLiteral ("Possible out-of-bounds read: ");
851 genExpr = exprNode_unparse (c->generatingExpr);
853 if (context_getFlag (FLG_CONSTRAINTLOCATION))
856 temp2 = message ("%s\n", genExpr);
857 temp = cstring_concatFree (temp, temp2);
860 st = cstring_concatFree (temp,st);
865 /*@only@*/ cstring constraint_unparse (constraint c) /*@*/
867 cstring st = cstring_undefined;
868 cstring type = cstring_undefined;
872 if (context_getFlag (FLG_PARENCONSTRAINT))
874 type = cstring_makeLiteral ("ensures: ");
878 type = cstring_makeLiteral ("ensures");
883 if (context_getFlag (FLG_PARENCONSTRAINT))
885 type = cstring_makeLiteral ("requires: ");
889 type = cstring_makeLiteral ("requires");
893 if (context_getFlag (FLG_PARENCONSTRAINT))
895 st = message ("%q: %q %q %q",
897 constraintExpr_print (c->lexpr),
898 arithType_print (c->ar),
899 constraintExpr_print (c->expr));
903 st = message ("%q %q %q %q",
905 constraintExpr_print (c->lexpr),
906 arithType_print (c->ar),
907 constraintExpr_print (c->expr));
912 cstring constraint_unparseOr (constraint c) /*@*/
917 ret = cstring_undefined;
919 llassert (constraint_isDefined (c) );
923 ret = cstring_concatFree (ret, constraint_unparse (temp));
927 while ( constraint_isDefined (temp))
929 ret = cstring_concatFree (ret, cstring_makeLiteral (" OR "));
930 ret = cstring_concatFree (ret, constraint_unparse (temp));
938 /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
939 exprNodeList arglist)
942 llassert (constraint_isDefined (precondition) );
944 precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
946 precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
953 constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exprNode fcnCall)
955 postcondition = constraint_copy (postcondition);
957 llassert (constraint_isDefined (postcondition) );
960 postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
961 postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
963 return postcondition;
965 /*Commenting out temporally
967 / *@only@* /constraint constraint_doSRefFixInvarConstraint(constraint invar, sRef s, ctype ct )
970 invar = constraint_copy (invar);
971 invar->lexpr = constraintExpr_doSRefFixInvarConstraint (invar->lexpr, s, ct);
972 invar->expr = constraintExpr_doSRefFixInvarConstraint (invar->expr, s, ct);
978 /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
979 exprNodeList arglist)
982 precondition = constraint_copy (precondition);
984 llassert (constraint_isDefined (precondition) );
986 precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
987 precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
989 precondition->fcnPre = FALSE;
990 return constraint_simplify(precondition);
993 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
995 if (constraint_isDefined (c))
997 DPRINTF (("Doing constraint_preserverOrig for %q", constraint_printLocation (c)));
999 if (c->orig == constraint_undefined)
1001 c->orig = constraint_copy (c);
1003 else if (c->orig->fcnPre)
1005 constraint temp = c->orig;
1007 /* avoid infinite loop */
1009 c->orig = constraint_copy (c);
1010 /*drl 03/2/2003 if c != NULL then the copy of c will != null*/
1011 llassert (constraint_isDefined (c->orig) );
1013 if (c->orig->orig == NULL)
1015 c->orig->orig = temp;
1020 llcontbug ((message ("Expected c->orig->orig to be null")));
1021 constraint_free (c->orig->orig);
1022 c->orig->orig = temp;
1028 DPRINTF (("Not changing constraint"));
1032 DPRINTF ((message ("After Doing constraint_preserverOrig for %q ", constraint_unparseDetailed (c))));
1036 constraint constraint_togglePost (/*@returned@*/ constraint c)
1038 llassert (constraint_isDefined (c));
1043 constraint constraint_togglePostOrig (/*@returned@*/ constraint c)
1045 llassert (constraint_isDefined (c));
1047 if (c->orig != NULL)
1049 c->orig = constraint_togglePost (c->orig);
1055 bool constraint_hasOrig ( /*@observer@*/ /*@temp@*/ constraint c)
1057 llassert (constraint_isDefined (c));
1058 return (c->orig != NULL);
1062 constraint constraint_undump (FILE *f)
1067 constraintExpr lexpr, expr;
1070 os = mstring_create (MAX_DUMP_LINE_LENGTH);
1071 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1073 if (!mstring_isDefined (s))
1075 llfatalbug (message ("Library file is corrupted") );
1078 fcnPre = (bool) reader_getInt (&s);
1080 post = (bool) reader_getInt (&s);
1082 ar = (arithType) reader_getInt (&s);
1084 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1086 if (! mstring_isDefined(s) )
1088 llfatalbug(message("Library file is corrupted") );
1091 reader_checkChar (&s, 'l');
1093 lexpr = constraintExpr_undump (f);
1095 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1097 reader_checkChar (&s, 'r');
1099 if (! mstring_isDefined(s) )
1101 llfatalbug(message("Library file is corrupted") );
1104 expr = constraintExpr_undump (f);
1106 c = constraint_makeNew ();
1116 c = constraint_preserveOrig (c);
1121 void constraint_dump (/*@observer@*/ constraint c, FILE *f)
1127 constraintExpr lexpr;
1128 constraintExpr expr;
1130 llassert (constraint_isDefined (c) );
1138 fprintf (f, "%d@%d@%d\n", (int) fcnPre, (int) post, (int) ar);
1140 constraintExpr_dump (lexpr, f);
1142 constraintExpr_dump (expr, f);
1146 int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * c1, /*@observer@*/ /*@temp@*/ const constraint * c2) /*@*/
1152 llassert (constraint_isDefined (*c1));
1153 llassert (constraint_isDefined (*c2));
1155 if (constraint_isUndefined (*c1))
1157 if (constraint_isUndefined (*c2))
1163 if (constraint_isUndefined (*c2))
1168 loc1 = constraint_getFileloc (*c1);
1169 loc2 = constraint_getFileloc (*c2);
1171 ret = fileloc_compare (loc1, loc2);
1173 fileloc_free (loc1);
1174 fileloc_free (loc2);
1180 bool constraint_isPost (/*@observer@*/ /*@temp@*/ constraint c)
1182 llassert (constraint_isDefined (c));
1184 if (constraint_isUndefined (c))
1191 static int constraint_getDepth (/*@observer@*/ /*@temp@*/ constraint c)
1195 llassert (constraint_isDefined (c) );
1197 l = constraintExpr_getDepth (c->lexpr);
1198 r = constraintExpr_getDepth (c->expr);
1202 DPRINTF (( message ("constraint depth returning %d for %s", l, constraint_unparse (c))));
1207 DPRINTF (( message ("constraint depth returning %d for %s", r, constraint_unparse (c))));
1213 bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint c)
1217 temp = constraint_getDepth (c);
1228 /*drl added 12/19/2002*/
1229 /*whether constraints consist only of
1230 terms which are constants*/
1231 bool constraint_isConstantOnly (constraint c)
1235 llassert (constraint_isDefined (c) );
1237 l = constraintExpr_isConstantOnly(c->lexpr);
1238 r = constraintExpr_isConstantOnly(c->expr);