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 <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"
41 static /*@only@*/ cstring constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
43 static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
44 /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/
45 /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
48 advanceField (char **s)
50 reader_checkChar (s, '@');
54 static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
59 ret = constraint_makeNew ();
60 llassert (constraintExpr_isDefined (l));
62 ret->lexpr = constraintExpr_copy (l);
65 if (relOp.tok == GE_OP)
67 else if (relOp.tok == LE_OP)
69 else if (relOp.tok == EQ_OP)
72 llfatalbug (message ("Unsupported relational operator"));
75 t = cstring_toCharsSafe (exprNode_unparse (cconstant));
77 ret->expr = constraintExpr_makeIntLiteral (c);
80 DPRINTF (("GENERATED CONSTRAINT:"));
81 DPRINTF ((message ("%s", constraint_unparse (ret))));
86 bool constraint_same (constraint c1, constraint c2)
88 llassert (c1 != NULL);
89 llassert (c2 != NULL);
96 if (!constraintExpr_similar (c1->lexpr, c2->lexpr))
101 if (!constraintExpr_similar (c1->expr, c2->expr))
109 constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
112 ret = constraint_makeNew ();
113 llassert (constraintExpr_isDefined (l));
115 ret->lexpr = constraintExpr_copy (l);
117 if (lltok_getTok (relOp) == GE_OP)
121 else if (lltok_getTok (relOp) == LE_OP)
125 else if (lltok_getTok (relOp) == EQ_OP)
130 llfatalbug ( message ("Unsupported relational operator"));
132 ret->expr = constraintExpr_copy (r);
136 ret->orig = constraint_copy (ret);
138 ret = constraint_simplify (ret);
139 /* ret->orig = ret; */
141 DPRINTF (("GENERATED CONSTRAINT:"));
142 DPRINTF ((message ("%s", constraint_unparse (ret))));
146 constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
150 llassert (constraint_isDefined (c));
152 ret = constraint_makeNew ();
153 ret->lexpr = constraintExpr_copy (c->lexpr);
155 ret->expr = constraintExpr_copy (c->expr);
158 ret->generatingExpr = c->generatingExpr;
163 ret->orig = constraint_copy (c->orig);
168 ret->or = constraint_copy (c->or);
172 ret->fcnPre = c->fcnPre;
177 /*like copy expect it doesn't allocate memory for the constraint*/
179 void constraint_overWrite (constraint c1, constraint c2)
181 llassert (constraint_isDefined (c1) && constraint_isDefined (c2));
185 DPRINTF ((message ("OverWriteing constraint %q with %q", constraint_unparse (c1),
186 constraint_unparse (c2))));
188 constraintExpr_free (c1->lexpr);
189 constraintExpr_free (c1->expr);
191 c1->lexpr = constraintExpr_copy (c2->lexpr);
193 c1->expr = constraintExpr_copy (c2->expr);
196 if (c1->orig != NULL)
197 constraint_free (c1->orig);
199 if (c2->orig != NULL)
200 c1->orig = constraint_copy (c2->orig);
204 /*@i33 make sure that the or is freed correctly*/
206 constraint_free (c1->or);
209 c1->or = constraint_copy (c2->or);
213 c1->fcnPre = c2->fcnPre;
216 c1->generatingExpr = c2->generatingExpr;
222 static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
223 /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/
224 /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
227 ret = dmalloc (sizeof (*ret));
234 ret->generatingExpr = NULL;
239 /*@access exprNode@*/
241 constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e)
244 llassert (constraint_isDefined (c) );
246 if (c->generatingExpr == NULL)
248 c->generatingExpr = e;
249 DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_unparse (c), exprNode_unparse (e)) ));
253 DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_unparse (c), exprNode_unparse (e)) ));
257 /*@noaccess exprNode@*/
259 constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
261 llassert (constraint_isDefined (c) );
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_unparse (c), exprNode_unparse (e)) ));
274 constraint constraint_setFcnPre (/*@returned@*/ constraint c)
277 llassert (constraint_isDefined (c) );
279 if (c->orig != constraint_undefined)
281 c->orig->fcnPre = TRUE;
286 DPRINTF (( message ("Warning Setting fcnPre directly")));
294 fileloc constraint_getFileloc (constraint c)
297 llassert (constraint_isDefined (c) );
299 if (exprNode_isDefined (c->generatingExpr))
300 return (fileloc_copy (exprNode_getfileloc (c->generatingExpr)));
302 return (constraintExpr_getFileloc (c->lexpr));
307 static bool checkForMaxSet (constraint c)
310 llassert (constraint_isDefined (c) );
312 if (constraintExpr_hasMaxSet (c->lexpr) || constraintExpr_hasMaxSet (c->expr))
318 bool constraint_hasMaxSet (constraint c)
321 llassert (constraint_isDefined (c) );
323 if (checkForMaxSet (c))
328 if (checkForMaxSet (c->orig))
335 constraint constraint_makeReadSafeExprNode (exprNode po, exprNode ind)
337 constraint ret = constraint_makeNew ();
341 ret->lexpr = constraintExpr_makeMaxReadExpr (po);
343 ret->expr = constraintExpr_makeValueExpr (ind);
348 constraint constraint_makeWriteSafeInt ( exprNode po, int ind)
350 constraint ret = constraint_makeNew ();
353 ret->lexpr =constraintExpr_makeMaxSetExpr (po);
355 ret->expr = constraintExpr_makeIntLiteral (ind);
359 constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
361 constraint ret = constraint_makeNew ();
362 ret->lexpr = constraintExpr_makeSRefMaxset (s);
364 ret->expr = constraintExpr_makeIntLiteral ((int)size);
370 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
372 constraint ret = constraint_makeNew ();
375 ret->lexpr = constraintExpr_makeSRefMaxset ( s);
377 ret->expr = constraintExpr_makeIntLiteral (ind);
383 /* drl added 01/12/2000
385 makes the constraint: Ensures index <= MaxRead (buffer) */
387 constraint constraint_makeEnsureLteMaxRead (exprNode index, exprNode buffer)
389 constraint ret = constraint_makeNew ();
391 ret->lexpr = constraintExpr_makeValueExpr (index);
393 ret->expr = constraintExpr_makeMaxReadExpr (buffer);
398 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
400 constraint ret = constraint_makeNew ();
403 ret->lexpr =constraintExpr_makeMaxSetExpr (po);
405 ret->expr = constraintExpr_makeValueExpr (ind);
410 constraint constraint_makeReadSafeInt ( exprNode t1, int index)
412 constraint ret = constraint_makeNew ();
414 ret->lexpr = constraintExpr_makeMaxReadExpr (t1);
416 ret->expr = constraintExpr_makeIntLiteral (index);
421 constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
423 constraint ret = constraint_makeNew ();
426 ret->lexpr = constraintExpr_makeSRefMaxRead (s);
428 ret->expr = constraintExpr_makeIntLiteral (ind);
433 constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
437 ret = constraint_makeReadSafeExprNode (t1, t2);
438 llassert (constraint_isDefined (ret) );
440 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
446 static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2, fileloc sequencePoint, arithType ar)
451 llassert (constraintExpr_isDefined (c1) && constraintExpr_isDefined (c2));
453 ret = constraint_makeNew ();
459 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
463 static constraint constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode e2, fileloc sequencePoint, arithType ar)
465 constraintExpr c1, c2;
469 if (! (exprNode_isDefined (e1) && exprNode_isDefined (e2)))
471 llcontbug ((message ("null exprNode, Exprnodes are %s and %s",
472 exprNode_unparse (e1), exprNode_unparse (e2))
477 c1 = constraintExpr_makeValueExpr (e);
480 c2 = constraintExpr_makeValueExpr (e);
482 ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
488 /* make constraint ensures e1 == e2 */
490 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
492 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ));
495 /*make constraint ensures e1 < e2 */
496 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
498 constraintExpr t1, t2;
501 t1 = constraintExpr_makeValueExpr (e1);
502 t2 = constraintExpr_makeValueExpr (e2);
504 /*change this to e1 <= (e2 -1) */
506 t2 = constraintExpr_makeDecConstraintExpr (t2);
508 t3 = constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE);
510 t3 = constraint_simplify(t3);
514 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
516 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE));
519 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
521 constraintExpr t1, t2;
524 t1 = constraintExpr_makeValueExpr (e1);
525 t2 = constraintExpr_makeValueExpr (e2);
528 /* change this to e1 >= (e2 + 1) */
529 t2 = constraintExpr_makeIncConstraintExpr (t2);
531 t3 = constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE);
533 t3 = constraint_simplify(t3);
538 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
540 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE));
545 /* Makes the constraint e = e + f */
546 constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint)
548 constraintExpr x1, x2, y;
551 ret = constraint_makeNew ();
553 x1 = constraintExpr_makeValueExpr (e);
554 x2 = constraintExpr_copy (x1);
555 y = constraintExpr_makeValueExpr (f);
560 ret->expr = constraintExpr_makeAddExpr (x2, y);
562 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
568 /* Makes the constraint e = e - f */
569 constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint)
571 constraintExpr x1, x2, y;
574 ret = constraint_makeNew ();
576 x1 = constraintExpr_makeValueExpr (e);
577 x2 = constraintExpr_copy (x1);
578 y = constraintExpr_makeValueExpr (f);
583 ret->expr = constraintExpr_makeSubtractExpr (x2, y);
585 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
590 constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
592 constraint ret = constraint_makeNew ();
594 ret->lexpr = constraintExpr_makeValueExpr (e);
597 ret->expr = constraintExpr_makeValueExpr (e);
598 ret->expr = constraintExpr_makeDecConstraintExpr (ret->expr);
599 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
602 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
604 constraint ret = constraint_makeNew ();
606 ret->lexpr = constraintExpr_makeValueExpr (e);
609 ret->expr = constraintExpr_makeValueExpr (e);
610 ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr);
612 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
617 void constraint_free (/*@only@*/ constraint c)
619 llassert (constraint_isDefined (c));
622 if (constraint_isDefined (c->orig))
623 constraint_free (c->orig);
624 if ( constraint_isDefined (c->or))
625 constraint_free (c->or);
628 constraintExpr_free (c->lexpr);
629 constraintExpr_free (c->expr);
640 cstring arithType_print (arithType ar) /*@*/
642 cstring st = cstring_undefined;
646 st = cstring_makeLiteral ("<");
649 st = cstring_makeLiteral ("<=");
652 st = cstring_makeLiteral (">");
655 st = cstring_makeLiteral (">=");
658 st = cstring_makeLiteral ("==");
661 st = cstring_makeLiteral ("NONNEGATIVE");
664 st = cstring_makeLiteral ("POSITIVE");
673 void constraint_printErrorPostCondition (constraint c, fileloc loc)
676 fileloc errorLoc, temp;
678 string = constraint_unparseDetailedPostCondition (c);
684 temp = constraint_getFileloc (c);
687 if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
689 string = cstring_replaceChar(string, '\n', ' ');
692 if (fileloc_isDefined (temp))
695 voptgenerror ( FLG_CHECKPOST, string, errorLoc);
700 voptgenerror ( FLG_CHECKPOST, string, errorLoc);
704 /*drl added 8-11-001*/
705 cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint c) /*@*/
710 string = constraint_unparse (c);
712 errorLoc = constraint_getFileloc (c);
714 ret = message ("constraint: %q @ %q", string, fileloc_unparse (errorLoc));
716 fileloc_free (errorLoc);
723 void constraint_printError (constraint c, fileloc loc)
726 fileloc errorLoc, temp;
731 llassert (constraint_isDefined (c) );
733 /*drl 11/26/2001 avoid printing tautological constraints */
734 if (constraint_isAlwaysTrue (c))
740 string = constraint_unparseDetailed (c);
744 temp = constraint_getFileloc (c);
746 if (fileloc_isDefined (temp))
753 DPRINTF (("constraint %s had undefined fileloc %s", constraint_unparse (c), fileloc_unparse (temp)));
755 errorLoc = fileloc_copy (errorLoc);
759 if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
761 string = cstring_replaceChar(string, '\n', ' ');
764 /*drl added 12/19/2002 print
765 a different error fro "likely" bounds-errors*/
767 isLikely = constraint_isConstantOnly(c);
773 voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
777 if (constraint_hasMaxSet (c))
779 voptgenerror (FLG_LIKELYBOUNDSWRITE, string, errorLoc);
783 voptgenerror (FLG_LIKELYBOUNDSREAD, string, errorLoc);
789 voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
793 if (constraint_hasMaxSet (c))
795 voptgenerror (FLG_BOUNDSWRITE, string, errorLoc);
799 voptgenerror (FLG_BOUNDSREAD, string, errorLoc);
803 fileloc_free(errorLoc);
806 static cstring constraint_unparseDeep (constraint c)
811 llassert (constraint_isDefined (c));
812 st = constraint_unparse (c);
814 if (c->orig != constraint_undefined)
816 st = cstring_appendChar (st, '\n');
817 genExpr = exprNode_unparse (c->orig->generatingExpr);
823 st = cstring_concatFree (st, message (" derived from %s precondition: %q",
824 genExpr, constraint_unparseDeep (c->orig)));
828 st = cstring_concatFree (st, message (" needed to satisfy precondition:\n%q",
829 constraint_unparseDeep (c->orig)));
834 st = cstring_concatFree (st, message ("derived from: %q",
835 constraint_unparseDeep (c->orig)));
843 static /*@only@*/ cstring constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
845 cstring st = cstring_undefined;
848 llassert (constraint_isDefined (c) );
850 st = message ("Unsatisfied ensures constraint condition:\nSplint is unable to verify the constraint %q",
851 constraint_unparseDeep (c));
853 genExpr = exprNode_unparse (c->generatingExpr);
855 if (context_getFlag (FLG_CONSTRAINTLOCATION))
859 temp = message ("\nOriginal Generating expression %q: %s\n",
860 fileloc_unparse ( exprNode_getfileloc (c->generatingExpr)),
862 st = cstring_concatFree (st, temp);
864 if (constraint_hasMaxSet (c))
866 temp = message ("Has MaxSet\n");
867 st = cstring_concatFree (st, temp);
873 cstring constraint_unparseDetailed (constraint c)
875 cstring st = cstring_undefined;
876 cstring temp = cstring_undefined;
880 llassert (constraint_isDefined (c) );
884 st = message ("Unable to resolve constraint:\n%q", constraint_unparseDeep (c));
888 st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_unparseDeep (c));
891 isLikely = constraint_isConstantOnly(c);
895 if (constraint_hasMaxSet (c))
897 temp = cstring_makeLiteral ("Likely out-of-bounds store:\n");
901 temp = cstring_makeLiteral ("Likely out-of-bounds read:\n");
907 if (constraint_hasMaxSet (c))
909 temp = cstring_makeLiteral ("Possible out-of-bounds store:\n");
913 temp = cstring_makeLiteral ("Possible out-of-bounds read:\n");
917 genExpr = exprNode_unparse (c->generatingExpr);
919 if (context_getFlag (FLG_CONSTRAINTLOCATION))
922 temp2 = message ("%s\n", genExpr);
923 temp = cstring_concatFree (temp, temp2);
926 st = cstring_concatFree (temp,st);
931 /*@only@*/ cstring constraint_unparse (constraint c) /*@*/
933 cstring st = cstring_undefined;
934 cstring type = cstring_undefined;
938 if (context_getFlag (FLG_PARENCONSTRAINT))
940 type = cstring_makeLiteral ("ensures: ");
944 type = cstring_makeLiteral ("ensures");
949 if (context_getFlag (FLG_PARENCONSTRAINT))
951 type = cstring_makeLiteral ("requires: ");
955 type = cstring_makeLiteral ("requires");
959 if (context_getFlag (FLG_PARENCONSTRAINT))
961 st = message ("%q: %q %q %q",
963 constraintExpr_print (c->lexpr),
964 arithType_print (c->ar),
965 constraintExpr_print (c->expr));
969 st = message ("%q %q %q %q",
971 constraintExpr_print (c->lexpr),
972 arithType_print (c->ar),
973 constraintExpr_print (c->expr));
978 cstring constraint_unparseOr (constraint c) /*@*/
983 ret = cstring_undefined;
985 llassert (constraint_isDefined (c) );
989 ret = cstring_concatFree (ret, constraint_unparse (temp));
993 while ( constraint_isDefined (temp))
995 ret = cstring_concatFree (ret, cstring_makeLiteral (" OR "));
996 ret = cstring_concatFree (ret, constraint_unparse (temp));
1004 /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
1005 exprNodeList arglist)
1008 llassert (constraint_isDefined (precondition) );
1010 precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
1012 precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
1015 return precondition;
1019 constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exprNode fcnCall)
1021 postcondition = constraint_copy (postcondition);
1023 llassert (constraint_isDefined (postcondition) );
1026 postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
1027 postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
1029 return postcondition;
1031 /*Commenting out temporally
1033 / *@only@* /constraint constraint_doSRefFixInvarConstraint(constraint invar, sRef s, ctype ct )
1036 invar = constraint_copy (invar);
1037 invar->lexpr = constraintExpr_doSRefFixInvarConstraint (invar->lexpr, s, ct);
1038 invar->expr = constraintExpr_doSRefFixInvarConstraint (invar->expr, s, ct);
1044 /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
1045 exprNodeList arglist)
1048 precondition = constraint_copy (precondition);
1050 llassert (constraint_isDefined (precondition) );
1052 precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
1053 precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
1055 precondition->fcnPre = FALSE;
1056 return constraint_simplify(precondition);
1059 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
1061 DPRINTF (("Doing constraint_preserverOrig for %q", constraint_printDetailed (c)));
1062 llassert (constraint_isDefined (c));
1064 if (c->orig == constraint_undefined)
1066 c->orig = constraint_copy (c);
1068 else if (c->orig->fcnPre)
1070 constraint temp = c->orig;
1072 /* avoid infinite loop */
1074 c->orig = constraint_copy (c);
1075 /*drl 03/2/2003 if c != NULL then the copy of c will != null*/
1076 llassert (constraint_isDefined (c->orig) );
1078 if (c->orig->orig == NULL)
1080 c->orig->orig = temp;
1085 llcontbug ((message ("Expected c->orig->orig to be null")));
1086 constraint_free (c->orig->orig);
1087 c->orig->orig = temp;
1093 DPRINTF (("Not changing constraint"));
1096 DPRINTF ((message ("After Doing constraint_preserverOrig for %q ", constraint_unparseDetailed (c))));
1100 constraint constraint_togglePost (/*@returned@*/ constraint c)
1102 llassert (constraint_isDefined (c));
1107 constraint constraint_togglePostOrig (/*@returned@*/ constraint c)
1109 llassert (constraint_isDefined (c));
1111 if (c->orig != NULL)
1113 c->orig = constraint_togglePost (c->orig);
1119 bool constraint_hasOrig ( /*@observer@*/ /*@temp@*/ constraint c)
1121 llassert (constraint_isDefined (c));
1122 return (c->orig != NULL);
1126 constraint constraint_undump (FILE *f)
1131 constraintExpr lexpr, expr;
1134 os = mstring_create (MAX_DUMP_LINE_LENGTH);
1135 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1137 if (!mstring_isDefined (s))
1139 llfatalbug (message ("Library file is corrupted") );
1142 fcnPre = (bool) reader_getInt (&s);
1144 post = (bool) reader_getInt (&s);
1146 ar = (arithType) reader_getInt (&s);
1148 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1150 if (! mstring_isDefined(s) )
1152 llfatalbug(message("Library file is corrupted") );
1155 reader_checkChar (&s, 'l');
1157 lexpr = constraintExpr_undump (f);
1159 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1161 reader_checkChar (&s, 'r');
1163 if (! mstring_isDefined(s) )
1165 llfatalbug(message("Library file is corrupted") );
1168 expr = constraintExpr_undump (f);
1170 c = constraint_makeNew ();
1180 c = constraint_preserveOrig (c);
1185 void constraint_dump (/*@observer@*/ constraint c, FILE *f)
1191 constraintExpr lexpr;
1192 constraintExpr expr;
1194 llassert (constraint_isDefined (c) );
1202 fprintf (f, "%d@%d@%d\n", (int) fcnPre, (int) post, (int) ar);
1204 constraintExpr_dump (lexpr, f);
1206 constraintExpr_dump (expr, f);
1210 int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * c1, /*@observer@*/ /*@temp@*/ const constraint * c2) /*@*/
1216 llassert (constraint_isDefined (*c1));
1217 llassert (constraint_isDefined (*c2));
1219 if (constraint_isUndefined (*c1))
1221 if (constraint_isUndefined (*c2))
1227 if (constraint_isUndefined (*c2))
1232 loc1 = constraint_getFileloc (*c1);
1233 loc2 = constraint_getFileloc (*c2);
1235 ret = fileloc_compare (loc1, loc2);
1237 fileloc_free (loc1);
1238 fileloc_free (loc2);
1244 bool constraint_isPost (/*@observer@*/ /*@temp@*/ constraint c)
1246 llassert (constraint_isDefined (c));
1248 if (constraint_isUndefined (c))
1255 static int constraint_getDepth (/*@observer@*/ /*@temp@*/ constraint c)
1259 llassert (constraint_isDefined (c) );
1261 l = constraintExpr_getDepth (c->lexpr);
1262 r = constraintExpr_getDepth (c->expr);
1266 DPRINTF (( message ("constraint depth returning %d for %s", l, constraint_unparse (c))));
1271 DPRINTF (( message ("constraint depth returning %d for %s", r, constraint_unparse (c))));
1277 bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint c)
1281 temp = constraint_getDepth (c);
1292 /*drl added 12/19/2002*/
1293 /*whether constraints consist only of
1294 terms which are constants*/
1295 bool constraint_isConstantOnly (constraint c)
1299 llassert (constraint_isDefined (c) );
1301 l = constraintExpr_isConstantOnly(c->lexpr);
1302 r = constraintExpr_isConstantOnly(c->expr);