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)
115 llassert (constraint_isDefined (c));
117 ret = constraint_makeNew ();
118 ret->lexpr = constraintExpr_copy (c->lexpr);
120 ret->expr = constraintExpr_copy (c->expr);
123 ret->generatingExpr = c->generatingExpr;
127 ret->orig = constraint_copy (c->orig);
132 ret->or = constraint_copy (c->or);
136 ret->fcnPre = c->fcnPre;
141 /*like copy except it doesn't allocate memory for the constraint*/
143 void constraint_overWrite (constraint c1, constraint c2)
145 llassert (constraint_isDefined (c1) && constraint_isDefined (c2));
149 DPRINTF ((message ("OverWriteing constraint %q with %q", constraint_unparse (c1),
150 constraint_unparse (c2))));
152 constraintExpr_free (c1->lexpr);
153 constraintExpr_free (c1->expr);
155 c1->lexpr = constraintExpr_copy (c2->lexpr);
157 c1->expr = constraintExpr_copy (c2->expr);
160 if (c1->orig != NULL)
161 constraint_free (c1->orig);
163 if (c2->orig != NULL)
164 c1->orig = constraint_copy (c2->orig);
169 constraint_free (c1->or);
172 c1->or = constraint_copy (c2->or);
176 c1->fcnPre = c2->fcnPre;
179 c1->generatingExpr = c2->generatingExpr;
185 static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
186 /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/
187 /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
190 ret = dmalloc (sizeof (*ret));
197 ret->generatingExpr = NULL;
202 /*@access exprNode@*/
204 constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e)
207 llassert (constraint_isDefined (c) );
209 if (c->generatingExpr == NULL)
211 c->generatingExpr = e;
212 DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_unparse (c), exprNode_unparse (e)) ));
216 DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_unparse (c), exprNode_unparse (e)) ));
220 /*@noaccess exprNode@*/
222 constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
224 llassert (constraint_isDefined (c) );
226 if (c->orig != constraint_undefined)
228 c->orig = constraint_addGeneratingExpr (c->orig, e);
232 DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_unparse (c), exprNode_unparse (e)) ));
237 constraint constraint_setFcnPre (/*@returned@*/ constraint c)
240 llassert (constraint_isDefined (c) );
242 if (c->orig != constraint_undefined)
244 c->orig->fcnPre = TRUE;
249 DPRINTF (( message ("Warning Setting fcnPre directly")));
257 fileloc constraint_getFileloc (constraint c)
260 llassert (constraint_isDefined (c) );
262 if (exprNode_isDefined (c->generatingExpr))
263 return (fileloc_copy (exprNode_getfileloc (c->generatingExpr)));
265 return (constraintExpr_getFileloc (c->lexpr));
270 static bool checkForMaxSet (constraint c)
273 llassert (constraint_isDefined (c) );
275 if (constraintExpr_hasMaxSet (c->lexpr) || constraintExpr_hasMaxSet (c->expr))
281 bool constraint_hasMaxSet (constraint c)
284 llassert (constraint_isDefined (c) );
286 if (checkForMaxSet (c))
291 if (checkForMaxSet (c->orig))
298 constraint constraint_makeReadSafeExprNode (exprNode po, exprNode ind)
300 constraint ret = constraint_makeNew ();
304 ret->lexpr = constraintExpr_makeMaxReadExpr (po);
306 ret->expr = constraintExpr_makeValueExpr (ind);
311 constraint constraint_makeWriteSafeInt ( exprNode po, int ind)
313 constraint ret = constraint_makeNew ();
315 ret->lexpr =constraintExpr_makeMaxSetExpr (po);
317 ret->expr = constraintExpr_makeIntLiteral (ind);
321 constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
323 constraint ret = constraint_makeNew ();
324 ret->lexpr = constraintExpr_makeSRefMaxset (s);
326 ret->expr = constraintExpr_makeIntLiteral ((int)size);
331 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
333 constraint ret = constraint_makeNew ();
336 ret->lexpr = constraintExpr_makeSRefMaxset ( s);
338 ret->expr = constraintExpr_makeIntLiteral (ind);
343 /* drl added 01/12/2000
345 makes the constraint: Ensures index <= MaxRead (buffer) */
347 constraint constraint_makeEnsureLteMaxRead (exprNode index, exprNode buffer)
349 constraint ret = constraint_makeNew ();
351 ret->lexpr = constraintExpr_makeValueExpr (index);
353 ret->expr = constraintExpr_makeMaxReadExpr (buffer);
358 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
360 constraint ret = constraint_makeNew ();
363 ret->lexpr =constraintExpr_makeMaxSetExpr (po);
365 ret->expr = constraintExpr_makeValueExpr (ind);
370 constraint constraint_makeReadSafeInt ( exprNode t1, int index)
372 constraint ret = constraint_makeNew ();
374 ret->lexpr = constraintExpr_makeMaxReadExpr (t1);
376 ret->expr = constraintExpr_makeIntLiteral (index);
381 constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
383 constraint ret = constraint_makeNew ();
386 ret->lexpr = constraintExpr_makeSRefMaxRead (s);
388 ret->expr = constraintExpr_makeIntLiteral (ind);
393 constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
397 ret = constraint_makeReadSafeExprNode (t1, t2);
398 llassert (constraint_isDefined (ret) );
400 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
406 static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2, fileloc sequencePoint, arithType ar)
411 llassert (constraintExpr_isDefined (c1) && constraintExpr_isDefined (c2));
413 ret = constraint_makeNew ();
419 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
423 static constraint constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode e2, fileloc sequencePoint, arithType ar)
425 constraintExpr c1, c2;
429 if (! (exprNode_isDefined (e1) && exprNode_isDefined (e2)))
431 llcontbug ((message ("null exprNode, Exprnodes are %s and %s",
432 exprNode_unparse (e1), exprNode_unparse (e2))
437 c1 = constraintExpr_makeValueExpr (e);
440 c2 = constraintExpr_makeValueExpr (e);
442 ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
448 /* make constraint ensures e1 == e2 */
450 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
452 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ));
455 /*make constraint ensures e1 < e2 */
456 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
458 constraintExpr t1, t2;
461 t1 = constraintExpr_makeValueExpr (e1);
462 t2 = constraintExpr_makeValueExpr (e2);
464 /*change this to e1 <= (e2 -1) */
466 t2 = constraintExpr_makeDecConstraintExpr (t2);
468 t3 = constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE);
470 t3 = constraint_simplify(t3);
474 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
476 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE));
479 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
481 constraintExpr t1, t2;
484 t1 = constraintExpr_makeValueExpr (e1);
485 t2 = constraintExpr_makeValueExpr (e2);
488 /* change this to e1 >= (e2 + 1) */
489 t2 = constraintExpr_makeIncConstraintExpr (t2);
491 t3 = constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE);
493 t3 = constraint_simplify(t3);
498 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
500 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE));
505 /* Makes the constraint e = e + f */
506 constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint)
508 constraintExpr x1, x2, y;
511 ret = constraint_makeNew ();
513 x1 = constraintExpr_makeValueExpr (e);
514 x2 = constraintExpr_copy (x1);
515 y = constraintExpr_makeValueExpr (f);
520 ret->expr = constraintExpr_makeAddExpr (x2, y);
522 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
528 /* Makes the constraint e = e - f */
529 constraint constraint_makeSubtractAssign (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_makeSubtractExpr (x2, y);
545 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
550 constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
552 constraint ret = constraint_makeNew ();
554 ret->lexpr = constraintExpr_makeValueExpr (e);
557 ret->expr = constraintExpr_makeValueExpr (e);
558 ret->expr = constraintExpr_makeDecConstraintExpr (ret->expr);
559 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
562 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
564 constraint ret = constraint_makeNew ();
566 ret->lexpr = constraintExpr_makeValueExpr (e);
569 ret->expr = constraintExpr_makeValueExpr (e);
570 ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr);
572 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
577 void constraint_free (/*@only@*/ constraint c)
579 llassert (constraint_isDefined (c));
582 if (constraint_isDefined (c->orig))
583 constraint_free (c->orig);
584 if ( constraint_isDefined (c->or))
585 constraint_free (c->or);
588 constraintExpr_free (c->lexpr);
589 constraintExpr_free (c->expr);
600 cstring arithType_print (arithType ar) /*@*/
602 cstring st = cstring_undefined;
606 st = cstring_makeLiteral ("<");
609 st = cstring_makeLiteral ("<=");
612 st = cstring_makeLiteral (">");
615 st = cstring_makeLiteral (">=");
618 st = cstring_makeLiteral ("==");
621 st = cstring_makeLiteral ("NONNEGATIVE");
624 st = cstring_makeLiteral ("POSITIVE");
633 void constraint_printErrorPostCondition (constraint c, fileloc loc)
636 fileloc errorLoc, temp;
638 string = constraint_unparseDetailedPostCondition (c);
644 temp = constraint_getFileloc (c);
647 if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
649 string = cstring_replaceChar(string, '\n', ' ');
652 if (fileloc_isDefined (temp))
655 voptgenerror ( FLG_CHECKPOST, string, errorLoc);
660 voptgenerror ( FLG_CHECKPOST, string, errorLoc);
664 /*drl added 8-11-001*/
665 cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint c) /*@*/
670 string = constraint_unparse (c);
672 errorLoc = constraint_getFileloc (c);
674 ret = message ("constraint: %q @ %q", string, fileloc_unparse (errorLoc));
676 fileloc_free (errorLoc);
683 void constraint_printError (constraint c, fileloc loc)
686 fileloc errorLoc, temp;
691 llassert (constraint_isDefined (c) );
693 /*drl 11/26/2001 avoid printing tautological constraints */
694 if (constraint_isAlwaysTrue (c))
700 string = constraint_unparseDetailed (c);
704 temp = constraint_getFileloc (c);
706 if (fileloc_isDefined (temp))
713 DPRINTF (("constraint %s had undefined fileloc %s", constraint_unparse (c), fileloc_unparse (temp)));
715 errorLoc = fileloc_copy (errorLoc);
719 if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
721 string = cstring_replaceChar(string, '\n', ' ');
724 /*drl added 12/19/2002 print
725 a different error fro "likely" bounds-errors*/
727 isLikely = constraint_isConstantOnly(c);
733 voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
737 if (constraint_hasMaxSet (c))
739 voptgenerror (FLG_LIKELYBOUNDSWRITE, string, errorLoc);
743 voptgenerror (FLG_LIKELYBOUNDSREAD, string, errorLoc);
749 voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
753 if (constraint_hasMaxSet (c))
755 voptgenerror (FLG_BOUNDSWRITE, string, errorLoc);
759 voptgenerror (FLG_BOUNDSREAD, string, errorLoc);
763 fileloc_free(errorLoc);
766 static cstring constraint_unparseDeep (constraint c)
771 llassert (constraint_isDefined (c));
772 st = constraint_unparse (c);
774 if (c->orig != constraint_undefined)
776 st = cstring_appendChar (st, '\n');
777 genExpr = exprNode_unparse (c->orig->generatingExpr);
783 st = cstring_concatFree (st, message (" derived from %s precondition: %q",
784 genExpr, constraint_unparseDeep (c->orig)));
788 st = cstring_concatFree (st, message (" needed to satisfy precondition:\n%q",
789 constraint_unparseDeep (c->orig)));
794 st = cstring_concatFree (st, message ("derived from: %q",
795 constraint_unparseDeep (c->orig)));
803 static /*@only@*/ cstring constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
805 cstring st = cstring_undefined;
808 llassert (constraint_isDefined (c) );
810 st = message ("Unsatisfied ensures constraint condition:\nSplint is unable to verify the constraint %q",
811 constraint_unparseDeep (c));
813 genExpr = exprNode_unparse (c->generatingExpr);
815 if (context_getFlag (FLG_CONSTRAINTLOCATION))
819 temp = message ("\nOriginal Generating expression %q: %s\n",
820 fileloc_unparse ( exprNode_getfileloc (c->generatingExpr)),
822 st = cstring_concatFree (st, temp);
824 if (constraint_hasMaxSet (c))
826 temp = message ("Has MaxSet\n");
827 st = cstring_concatFree (st, temp);
833 cstring constraint_unparseDetailed (constraint c)
835 cstring st = cstring_undefined;
836 cstring temp = cstring_undefined;
840 llassert (constraint_isDefined (c) );
844 st = message ("Unable to resolve constraint:\n%q", constraint_unparseDeep (c));
848 st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_unparseDeep (c));
851 isLikely = constraint_isConstantOnly(c);
855 if (constraint_hasMaxSet (c))
857 temp = cstring_makeLiteral ("Likely out-of-bounds store:\n");
861 temp = cstring_makeLiteral ("Likely out-of-bounds read:\n");
867 if (constraint_hasMaxSet (c))
869 temp = cstring_makeLiteral ("Possible out-of-bounds store:\n");
873 temp = cstring_makeLiteral ("Possible out-of-bounds read:\n");
877 genExpr = exprNode_unparse (c->generatingExpr);
879 if (context_getFlag (FLG_CONSTRAINTLOCATION))
882 temp2 = message ("%s\n", genExpr);
883 temp = cstring_concatFree (temp, temp2);
886 st = cstring_concatFree (temp,st);
891 /*@only@*/ cstring constraint_unparse (constraint c) /*@*/
893 cstring st = cstring_undefined;
894 cstring type = cstring_undefined;
898 if (context_getFlag (FLG_PARENCONSTRAINT))
900 type = cstring_makeLiteral ("ensures: ");
904 type = cstring_makeLiteral ("ensures");
909 if (context_getFlag (FLG_PARENCONSTRAINT))
911 type = cstring_makeLiteral ("requires: ");
915 type = cstring_makeLiteral ("requires");
919 if (context_getFlag (FLG_PARENCONSTRAINT))
921 st = message ("%q: %q %q %q",
923 constraintExpr_print (c->lexpr),
924 arithType_print (c->ar),
925 constraintExpr_print (c->expr));
929 st = message ("%q %q %q %q",
931 constraintExpr_print (c->lexpr),
932 arithType_print (c->ar),
933 constraintExpr_print (c->expr));
938 cstring constraint_unparseOr (constraint c) /*@*/
943 ret = cstring_undefined;
945 llassert (constraint_isDefined (c) );
949 ret = cstring_concatFree (ret, constraint_unparse (temp));
953 while ( constraint_isDefined (temp))
955 ret = cstring_concatFree (ret, cstring_makeLiteral (" OR "));
956 ret = cstring_concatFree (ret, constraint_unparse (temp));
964 /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
965 exprNodeList arglist)
968 llassert (constraint_isDefined (precondition) );
970 precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
972 precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
979 constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exprNode fcnCall)
981 postcondition = constraint_copy (postcondition);
983 llassert (constraint_isDefined (postcondition) );
986 postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
987 postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
989 return postcondition;
991 /*Commenting out temporally
993 / *@only@* /constraint constraint_doSRefFixInvarConstraint(constraint invar, sRef s, ctype ct )
996 invar = constraint_copy (invar);
997 invar->lexpr = constraintExpr_doSRefFixInvarConstraint (invar->lexpr, s, ct);
998 invar->expr = constraintExpr_doSRefFixInvarConstraint (invar->expr, s, ct);
1004 /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
1005 exprNodeList arglist)
1008 precondition = constraint_copy (precondition);
1010 llassert (constraint_isDefined (precondition) );
1012 precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
1013 precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
1015 precondition->fcnPre = FALSE;
1016 return constraint_simplify(precondition);
1019 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
1021 DPRINTF (("Doing constraint_preserverOrig for %q", constraint_printDetailed (c)));
1022 llassert (constraint_isDefined (c));
1024 if (c->orig == constraint_undefined)
1026 c->orig = constraint_copy (c);
1028 else if (c->orig->fcnPre)
1030 constraint temp = c->orig;
1032 /* avoid infinite loop */
1034 c->orig = constraint_copy (c);
1035 /*drl 03/2/2003 if c != NULL then the copy of c will != null*/
1036 llassert (constraint_isDefined (c->orig) );
1038 if (c->orig->orig == NULL)
1040 c->orig->orig = temp;
1045 llcontbug ((message ("Expected c->orig->orig to be null")));
1046 constraint_free (c->orig->orig);
1047 c->orig->orig = temp;
1053 DPRINTF (("Not changing constraint"));
1056 DPRINTF ((message ("After Doing constraint_preserverOrig for %q ", constraint_unparseDetailed (c))));
1060 constraint constraint_togglePost (/*@returned@*/ constraint c)
1062 llassert (constraint_isDefined (c));
1067 constraint constraint_togglePostOrig (/*@returned@*/ constraint c)
1069 llassert (constraint_isDefined (c));
1071 if (c->orig != NULL)
1073 c->orig = constraint_togglePost (c->orig);
1079 bool constraint_hasOrig ( /*@observer@*/ /*@temp@*/ constraint c)
1081 llassert (constraint_isDefined (c));
1082 return (c->orig != NULL);
1086 constraint constraint_undump (FILE *f)
1091 constraintExpr lexpr, expr;
1094 os = mstring_create (MAX_DUMP_LINE_LENGTH);
1095 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1097 if (!mstring_isDefined (s))
1099 llfatalbug (message ("Library file is corrupted") );
1102 fcnPre = (bool) reader_getInt (&s);
1104 post = (bool) reader_getInt (&s);
1106 ar = (arithType) reader_getInt (&s);
1108 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1110 if (! mstring_isDefined(s) )
1112 llfatalbug(message("Library file is corrupted") );
1115 reader_checkChar (&s, 'l');
1117 lexpr = constraintExpr_undump (f);
1119 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1121 reader_checkChar (&s, 'r');
1123 if (! mstring_isDefined(s) )
1125 llfatalbug(message("Library file is corrupted") );
1128 expr = constraintExpr_undump (f);
1130 c = constraint_makeNew ();
1140 c = constraint_preserveOrig (c);
1145 void constraint_dump (/*@observer@*/ constraint c, FILE *f)
1151 constraintExpr lexpr;
1152 constraintExpr expr;
1154 llassert (constraint_isDefined (c) );
1162 fprintf (f, "%d@%d@%d\n", (int) fcnPre, (int) post, (int) ar);
1164 constraintExpr_dump (lexpr, f);
1166 constraintExpr_dump (expr, f);
1170 int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * c1, /*@observer@*/ /*@temp@*/ const constraint * c2) /*@*/
1176 llassert (constraint_isDefined (*c1));
1177 llassert (constraint_isDefined (*c2));
1179 if (constraint_isUndefined (*c1))
1181 if (constraint_isUndefined (*c2))
1187 if (constraint_isUndefined (*c2))
1192 loc1 = constraint_getFileloc (*c1);
1193 loc2 = constraint_getFileloc (*c2);
1195 ret = fileloc_compare (loc1, loc2);
1197 fileloc_free (loc1);
1198 fileloc_free (loc2);
1204 bool constraint_isPost (/*@observer@*/ /*@temp@*/ constraint c)
1206 llassert (constraint_isDefined (c));
1208 if (constraint_isUndefined (c))
1215 static int constraint_getDepth (/*@observer@*/ /*@temp@*/ constraint c)
1219 llassert (constraint_isDefined (c) );
1221 l = constraintExpr_getDepth (c->lexpr);
1222 r = constraintExpr_getDepth (c->expr);
1226 DPRINTF (( message ("constraint depth returning %d for %s", l, constraint_unparse (c))));
1231 DPRINTF (( message ("constraint depth returning %d for %s", r, constraint_unparse (c))));
1237 bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint c)
1241 temp = constraint_getDepth (c);
1252 /*drl added 12/19/2002*/
1253 /*whether constraints consist only of
1254 terms which are constants*/
1255 bool constraint_isConstantOnly (constraint c)
1259 llassert (constraint_isDefined (c) );
1261 l = constraintExpr_isConstantOnly(c->lexpr);
1262 r = constraintExpr_isConstantOnly(c->expr);