src/constraintResolve.c

   1 /*
   2 ** Splint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2003 University of Virginia,
   4 **         Massachusetts Institute of Technology
   5 **
   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.
  10 **
  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.
  15 **
  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.
  19 **
  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
  23 */
  24
  25 /*
  26 *
  27 ** constraintResolve.c
  28 */
  29
  30 /* #define DEBUGPRINT 1 */
  31
  32 # include <ctype.h> /* for isdigit */
  33 # include "splintMacros.nf"
  34 # include "basic.h"
  35 # include "cgrammar.h"
  36 # include "cgrammar_tokens.h"
  37
  38 # include "exprChecks.h"
  39 # include "exprNodeSList.h"
  40
  41
  42 /*@access constraint, exprNode @*/ /*!!! NO! Don't do this so recklessly - design your code more carefully so you don't need to! */
  43
  44 static constraint  inequalitySubstitute  (/*@returned@*/ constraint p_c, constraintList p_p);
  45
  46
  47 static bool rangeCheck (arithType p_ar1, /*@observer@*/ constraintExpr p_expr1, arithType p_ar2, /*@observer@*/ constraintExpr p_expr2);
  48
  49 static constraint  inequalitySubstituteUnsound  (/*@returned@*/ constraint p_c, constraintList p_p);
  50
  51 static constraint  inequalitySubstituteStrong  (/*@returned@*/ constraint p_c, constraintList p_p);
  52
  53 static constraint constraint_searchandreplace (/*@returned@*/ constraint p_c, constraintExpr p_old, constraintExpr p_newExpr);
  54
  55
  56 static constraint constraint_addOr (/*@returned@*/ constraint p_orig, /*@observer@*/ constraint p_orConstr);
  57
  58 static bool constraint_resolveOr (/*@temp@*/constraint p_c, /*@observer@*/ /*@temp@*/ constraintList p_list);
  59
  60 static /*@only@*/ constraintList reflectChangesEnsuresFree1 (/*@only@*/ constraintList p_pre2, constraintList p_post1);
  61
  62 /*@only@*/ constraintList
  63 constraintList_mergeEnsuresFreeFirst (constraintList list1, constraintList list2)
  64 {
  65   constraintList ret = constraintList_mergeEnsures (list1, list2);
  66   constraintList_free (list1);
  67   return ret;
  68 }
  69
  70 /*@only@*/ constraintList
  71 constraintList_mergeEnsures (constraintList list1, constraintList list2)
  72 {
  73   constraintList ret;
  74   constraintList temp;
  75
  76   llassert (constraintList_isDefined (list1));
  77   llassert (constraintList_isDefined (list2));
  78
  79   DPRINTF (("constraintList_mergeEnsures: list1 %s list2 %s",
  80             constraintList_unparse (list1), constraintList_unparse (list2)));
  81
  82   ret = constraintList_fixConflicts (list1, list2);
  83   ret = reflectChangesEnsuresFree1 (ret, list2);
  84   temp = constraintList_subsumeEnsures (ret, list2);
  85   constraintList_free (ret);
  86
  87   ret = temp;
  88   temp = constraintList_subsumeEnsures (list2, ret);
  89   temp = constraintList_addList (temp, ret);
  90   constraintList_free (ret);
  91
  92   DPRINTF (("constraintList_mergeEnsures: returning %s", constraintList_unparse (temp)));
  93   return temp;
  94 }
  95
  96 /*@only@*/ constraintList
  97 constraintList_mergeRequiresFreeFirst (/*@only@*/ constraintList list1,
  98                                        constraintList list2)
  99 {
 100   constraintList ret = constraintList_mergeRequires (list1, list2);
 101   constraintList_free (list1);
 102   return ret;
 103 }
 104
 105 /*@only@*/ constraintList
 106 constraintList_mergeRequires (constraintList list1, constraintList list2)
 107 {
 108   constraintList ret;
 109   constraintList temp;
 110
 111   DPRINTF (("constraintList_mergeRequires: merging  %s and %s",
 112             constraintList_unparse (list1), constraintList_unparse (list2)));
 113
 114   if (context_getFlag (FLG_REDUNDANTCONSTRAINTS))
 115     {
 116       ret = constraintList_copy (list1);
 117       ret = constraintList_addList (ret, list2);
 118       return ret;
 119     }
 120
 121   /* get constraints in list1 not satified by list2 */
 122   temp = constraintList_reflectChanges (list1, list2);
 123   DPRINTF (("constraintList_mergeRequires: temp = %s", constraintList_unparse (temp)));
 124
 125   /* get constraints in list2 not satified by temp*/
 126   ret = constraintList_reflectChanges (list2, temp);
 127   DPRINTF (("constraintList_mergeRequires: ret =  %s", constraintList_unparse(ret)));
 128
 129   ret = constraintList_addListFree (ret, temp);
 130   DPRINTF (("constraintList_mergeRequires: returning  %s", constraintList_unparse(ret)));
 131
 132   return ret;
 133 }
 134
 135 /* old name mergeResolve renamed for czech naming convention */
 136 void exprNode_mergeResolve (exprNode parent, exprNode child1, exprNode child2)
 137 {
 138   constraintList temp, temp2;
 139
 140   DPRINTF((message ("magically merging constraint into parent:%s for", exprNode_unparse (parent))));
 141
 142   DPRINTF((message (" children:  %s and %s", exprNode_unparse (child1), exprNode_unparse(child2))));
 143
 144   if (exprNode_isUndefined (parent))
 145     {
 146       llassert (exprNode_isDefined (parent));
 147       return;
 148     }
 149
 150
 151   if (exprNode_isError (child1) || exprNode_isError (child2))
 152     {
 153       if (exprNode_isError (child1) && !exprNode_isError (child2))
 154          {
 155            constraintList_free (parent->requiresConstraints);
 156            parent->requiresConstraints = constraintList_copy (child2->requiresConstraints);
 157            constraintList_free (parent->ensuresConstraints);
 158
 159            parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints);
 160            DPRINTF (("Copied child constraints: pre: %s and post: %s",
 161                      constraintList_unparse(child2->requiresConstraints),
 162                      constraintList_unparse (child2->ensuresConstraints)));
 163            return;
 164          }
 165        else
 166          {
 167            llassert (exprNode_isError (child2));
 168            return;
 169          }
 170      }
 171
 172    llassert (!exprNode_isError (child1) && !exprNode_isError (child2));
 173
 174    DPRINTF (("Child constraints are %s %s and %s %s",
 175              constraintList_unparse (child1->requiresConstraints),
 176              constraintList_unparse (child1->ensuresConstraints),
 177              constraintList_unparse (child2->requiresConstraints),
 178              constraintList_unparse (child2->ensuresConstraints)));
 179
 180    constraintList_free (parent->requiresConstraints);
 181    parent->requiresConstraints = constraintList_copy (child1->requiresConstraints);
 182
 183    if (context_getFlag (FLG_ORCONSTRAINT))
 184      {
 185        temp = constraintList_reflectChangesOr (child2->requiresConstraints, child1->ensuresConstraints);
 186      }
 187    else
 188      {
 189        temp = constraintList_reflectChanges(child2->requiresConstraints, child1->ensuresConstraints);
 190      }
 191
 192    temp2 = constraintList_mergeRequires (parent->requiresConstraints, temp);
 193    constraintList_free (parent->requiresConstraints);
 194    constraintList_free (temp);
 195
 196    parent->requiresConstraints = temp2;
 197
 198    DPRINTF (("Parent requires constraints are %s  ",
 199              constraintList_unparse (parent->requiresConstraints)));
 200
 201    constraintList_free (parent->ensuresConstraints);
 202
 203    parent->ensuresConstraints = constraintList_mergeEnsures (child1->ensuresConstraints,
 204                                                              child2->ensuresConstraints);
 205
 206
 207    DPRINTF (("Parent constraints are %s and %s ",
 208              constraintList_unparse (parent->requiresConstraints),
 209              constraintList_unparse (parent->ensuresConstraints)));
 210 }
 211
 212 /*@only@*/ constraintList
 213 constraintList_subsumeEnsures (constraintList list1, constraintList list2)
 214 {
 215   constraintList ret = constraintList_makeNew ();
 216
 217   constraintList_elements (list1, el)
 218     {
 219       DPRINTF (("Examining %s", constraint_unparse (el)));
 220       if (!constraintList_resolve (el, list2))
 221         {
 222           constraint temp = constraint_copy (el);
 223           ret = constraintList_add (ret, temp);
 224         }
 225       else
 226         {
 227           DPRINTF (("Subsuming %s", constraint_unparse (el)));
 228         }
 229     } end_constraintList_elements;
 230
 231     return ret;
 232 }
 233
 234 /* tries to resolve constraints in list pre2 using post1 */
 235 /*@only@*/ constraintList
 236 constraintList_reflectChangesFreePre (/*@only@*/ constraintList pre2, /*@observer@*/ constraintList post1)
 237 {
 238   constraintList ret = constraintList_reflectChanges(pre2, post1);
 239   constraintList_free (pre2);
 240   return ret;
 241 }
 242
 243
 244
 245 /* tries to resolve constraints in list pre2 using post1 */
 246 static /*@only@*/ constraintList
 247 constraintList_reflectChangesNoOr (/*@observer@*/ /*@temp@*/ constraintList pre2,
 248                     /*@observer@*/ /*@temp@*/ constraintList post1)
 249 {
 250   constraintList ret = constraintList_makeNew ();
 251
 252   llassert  (!context_getFlag (FLG_ORCONSTRAINT));
 253
 254   DPRINTF (("reflectChanges: lists %s and %s",
 255             constraintList_unparse (pre2), constraintList_unparse (post1)));
 256
 257   constraintList_elements (pre2, el)
 258     {
 259       if (!constraintList_resolve (el, post1))
 260         {
 261           constraint temp = constraint_substitute (el, post1);
 262
 263           if (!constraintList_resolve (temp, post1))
 264             {
 265               /* try inequality substitution
 266                  the inequality substitution may cause us to lose information
 267                  so we don't want to store the result but we do it anyway
 268               */
 269               constraint temp2 = constraint_copy (temp);
 270               temp2 = inequalitySubstitute (temp2, post1);
 271
 272               if (!constraintList_resolve (temp2, post1))
 273                 {
 274                   temp2 = inequalitySubstituteUnsound (temp2, post1);
 275                   if (!constraintList_resolve (temp2, post1))
 276                     {
 277                       ret = constraintList_add (ret, temp2);
 278                     }
 279                   else
 280                     {
 281                       constraint_free (temp2);
 282                     }
 283                 }
 284               else
 285                 {
 286                   constraint_free (temp2);
 287                 }
 288             }
 289           constraint_free (temp);
 290         }
 291     } end_constraintList_elements;
 292
 293   DPRINTF (("reflectChanges: returning %s", constraintList_unparse(ret)));
 294   return ret;
 295 }
 296
 297 /* tries to resolve constraints in list pre2 using post1 */
 298 /*@only@*/ constraintList
 299 constraintList_reflectChanges (/*@observer@*/ constraintList pre2, /*@observer@*/ constraintList post1)
 300 {
 301   if (context_getFlag (FLG_ORCONSTRAINT))
 302     {
 303       return constraintList_reflectChangesOr (pre2, post1);
 304     }
 305   else
 306     {
 307       return constraintList_reflectChangesNoOr (pre2, post1);
 308     }
 309 }
 310
 311 static constraint
 312 constraint_addOr (/*@returned@*/ constraint orig, /*@observer@*/ constraint orConstr)
 313 {
 314   constraint c = orig;
 315   llassert (constraint_isDefined (c));
 316
 317   DPRINTF (("constraint_addor: oring %s onto %s",
 318             constraint_unparseOr (orConstr), constraint_unparseOr (orig)));
 319
 320   while (c->or != NULL)
 321     {
 322       c = c->or;
 323     }
 324
 325   c->or = constraint_copy (orConstr);
 326
 327   DPRINTF (("constraint_addor: returning %s",constraint_unparseOr (orig)));
 328   return orig;
 329 }
 330
 331 static bool constraint_resolveOr (/*@temp@*/ constraint c, /*@observer@*/ /*@temp@*/ constraintList list)
 332 {
 333   constraint temp = c;
 334   int numberOr = 0;
 335
 336   llassert (constraint_isDefined(c));
 337   DPRINTF (("constraint_resolveOr: constraint %s and list %s",
 338             constraint_printOr (c), constraintList_print (list)));
 339
 340   do
 341     {
 342       if (constraintList_resolve (temp, list))
 343         {
 344           return TRUE;
 345         }
 346
 347       temp = temp->or;
 348       numberOr++;
 349       llassert(numberOr <= 10);
 350     }
 351   while (constraint_isDefined (temp));
 352
 353   return FALSE;
 354 }
 355
 356 /* This is a "helper" function for doResolveOr */
 357
 358 static /*@only@*/ constraint doResolve (/*@only@*/ constraint c, constraintList post1, bool * resolved)
 359 {
 360   llassert (constraint_isDefined (c));
 361
 362   DPRINTF (("doResolve:: call on constraint c = : %q and constraintList %q",
 363             constraint_unparseOr (c), constraintList_unparse (post1)));
 364
 365   if (!constraint_resolveOr (c, post1))
 366     {
 367       constraint temp = constraint_substitute (c, post1);
 368       DPRINTF (("doResolve:: after substitute temp is %q", constraint_unparseOr (temp)));
 369
 370       if (!constraint_resolveOr (temp, post1))
 371         {
 372           /* try inequality substitution */
 373           constraint temp2 = constraint_copy (c);
 374
 375           /*
 376           ** the inequality substitution may cause us to lose information
 377           ** so we don't want to store the result but we do anyway
 378           */
 379
 380           temp2 = inequalitySubstitute (temp2, post1);
 381
 382           if (!constraint_resolveOr (temp2, post1))
 383             {
 384               constraint temp3 = constraint_copy(temp2);
 385               temp3 = inequalitySubstituteStrong (temp3, post1);
 386
 387               if (!constraint_resolveOr (temp3, post1))
 388                 {
 389                   temp2 = inequalitySubstituteUnsound (temp2, post1);
 390
 391                   if (!constraint_resolveOr (temp2, post1))
 392                     {
 393                       if (!constraint_same (temp, temp2))
 394                         {
 395                           /* drl added 8/28/2002*/
 396                           /*make sure that the information from
 397                             a post condition like i = i + 1 is transfered
 398                           */
 399                           constraint tempSub;
 400                           tempSub = constraint_substitute (temp2, post1);
 401
 402                           DPRINTF (("doResolve: adding %s", constraint_unparseOr (tempSub)));
 403                           DPRINTF (("doResolve: not adding %s", constraint_unparseOr (temp2)));
 404
 405                           temp = constraint_addOr (temp, tempSub);
 406                           constraint_free (tempSub);
 407                         }
 408
 409                       if (!constraint_same (temp, temp3) && !constraint_same (temp3, temp2))
 410                         {
 411                           /* drl added 8/28/2002*/
 412                           /* make sure that the information from
 413                              a post condition like i = i + 1 is transfered
 414                           */
 415                           constraint tempSub;
 416
 417                           tempSub = constraint_substitute (temp3, post1);
 418
 419                           DPRINTF (("doResolve: adding %s", constraint_unparseOr (tempSub)));
 420                           DPRINTF (("doResolve: not adding %s", constraint_unparseOr(temp3)));
 421
 422                           temp = constraint_addOr (temp, tempSub);
 423                           constraint_free(tempSub);
 424                         }
 425
 426                       *resolved = FALSE;
 427
 428                       constraint_free (temp2);
 429                       constraint_free (temp3);
 430                       constraint_free (c);
 431
 432                       return temp;
 433                     }
 434
 435                   constraint_free (temp2);
 436                   constraint_free (temp3);
 437                 }
 438               else
 439                 {
 440                   constraint_free (temp2);
 441                   constraint_free (temp3);
 442                 }
 443             }
 444           else
 445             {
 446               constraint_free (temp2);
 447             }
 448
 449         }
 450       constraint_free (temp);
 451     }
 452
 453   constraint_free (c);
 454   /*@i523@*/ /*drl bee: pbr*/ *resolved = TRUE;
 455   return NULL;
 456 }
 457
 458 static /*@only@*/ constraint
 459 doResolveOr (/*@observer@*/ /*@temp@*/ constraint c, constraintList post1, /*@out@*/ bool *resolved)
 460 {
 461   constraint ret;
 462   constraint next;
 463   constraint curr;
 464
 465   DPRINTF (("doResolveOr: constraint %s and list %s",
 466             constraint_unparseOr (c), constraintList_unparse (post1)));
 467
 468   /*@i523@*/ /*drl bee: pbr*/ *resolved = FALSE;
 469
 470   llassert (constraint_isDefined (c));
 471   ret = constraint_copy (c);
 472
 473   llassert (constraint_isDefined (ret));
 474
 475   if (constraintList_isEmpty (post1))
 476     {
 477       return ret;
 478     }
 479
 480   next = ret->or;
 481   ret->or = NULL;
 482
 483   ret = doResolve (ret, post1, resolved);
 484
 485   if (*resolved)
 486     {
 487       if (next != NULL)
 488         {
 489           constraint_free (next);
 490         }
 491
 492       /* we don't need to free ret when resolved is false because ret is null*/
 493       llassert (ret == NULL);
 494       return NULL;
 495     }
 496
 497   while (next != NULL)
 498     {
 499       curr = next;
 500       next = curr->or;
 501       curr->or = NULL;
 502
 503       curr = doResolve (curr, post1, resolved);
 504
 505       /*@i423@*/ /*drl bee: pbr*/    if (*resolved)
 506         {
 507           /* curr is null so we don't try to free it*/
 508           llassert (curr == NULL);
 509
 510           if (next != NULL)
 511             {
 512               constraint_free (next);
 513             }
 514
 515           constraint_free (ret);
 516           return NULL;
 517         }
 518       ret = constraint_addOr (ret, curr);
 519       constraint_free(curr);
 520     }
 521   return ret;
 522 }
 523
 524 /* tries to resolve constraints in list pr2 using post1 */
 525 /*@only@*/ constraintList
 526 constraintList_reflectChangesOr (constraintList pre2, constraintList post1)
 527 {
 528   bool resolved;
 529   constraintList ret;
 530   constraint temp;
 531   ret = constraintList_makeNew();
 532
 533   DPRINTF (("constraintList_reflectChangesOr: lists %s and %s",
 534             constraintList_unparse (pre2), constraintList_unparse (post1)));
 535
 536   constraintList_elements (pre2, el)
 537     {
 538       temp = doResolveOr (el, post1, &resolved);
 539
 540       if (!resolved)
 541         {
 542           ret = constraintList_add(ret, temp);
 543         }
 544       else
 545         {
 546           /* we don't need to free temp when
 547              resolved is false because temp is null */
 548           llassert (temp == NULL);
 549         }
 550     } end_constraintList_elements;
 551
 552   DPRINTF (("constraintList_reflectChangesOr: returning %s", constraintList_unparse (ret)));
 553   return ret;
 554 }
 555
 556 static /*@only@*/ constraintList
 557 reflectChangesEnsures (/*@observer@*/ constraintList pre2, constraintList post1)
 558 {
 559   constraintList ret = constraintList_makeNew ();
 560
 561   constraintList_elements (pre2, el)
 562     {
 563       if (!constraintList_resolve (el, post1))
 564         {
 565           constraint temp = constraint_substitute (el, post1);
 566           llassert (temp != NULL);
 567
 568           if (!constraintList_resolve (temp, post1))
 569             {
 570               ret = constraintList_add (ret, temp);
 571             }
 572           else
 573             {
 574               constraint_free (temp);
 575             }
 576         }
 577       else
 578         {
 579           DPRINTF (("Resolved away %s ", constraint_unparse(el)));
 580         }
 581     } end_constraintList_elements;
 582
 583   return ret;
 584 }
 585
 586
 587 static /*@only@*/ constraintList
 588 reflectChangesEnsuresFree1 (/*@only@*/ constraintList pre2, constraintList post1)
 589 {
 590   constraintList ret = reflectChangesEnsures (pre2, post1);
 591   constraintList_free(pre2);
 592   return ret;
 593 }
 594
 595
 596 static bool constraint_conflict (constraint c1, constraint c2)
 597 {
 598   llassert (constraint_isDefined (c1));
 599   llassert (constraint_isDefined (c2));
 600
 601   if (constraintExpr_similar (c1->lexpr, c2->lexpr))
 602     {
 603       if (c1->ar == EQ && (c1->ar == c2->ar))
 604         {
 605           DPRINTF (("%s conflicts with %s ", constraint_unparse (c1), constraint_unparse(c2)));
 606           return TRUE;
 607         }
 608     }
 609
 610   /*
 611   ** This is a slight kludge to prevent circular constraints like
 612   ** strlen(str) == maxRead(s) + strlen(str);
 613   */
 614
 615   if (c1->ar == EQ && (c1->ar == c2->ar))
 616     {
 617       if (constraintExpr_search (c1->lexpr, c2->expr))
 618         {
 619           if (constraintExpr_isTerm (c1->lexpr))
 620             {
 621               constraintTerm term = constraintExpr_getTerm (c1->lexpr);
 622
 623               if (constraintTerm_isExprNode (term))
 624                 {
 625                   DPRINTF (("%s conflicts with %s ", constraint_unparse (c1),
 626                             constraint_unparse (c2)));
 627                   return TRUE;
 628                 }
 629             }
 630         }
 631     }
 632
 633   if (constraint_tooDeep (c1) || constraint_tooDeep (c2))
 634     {
 635       DPRINTF (("%s conflicts with %s (constraint is too deep)",
 636                 constraint_unparse (c1), constraint_unparse (c2)));
 637       return TRUE;
 638     }
 639
 640   DPRINTF (("%s doesn't conflict with %s",
 641             constraint_unparse (c1), constraint_unparse (c2)));
 642   return FALSE;
 643 }
 644
 645 static void
 646 constraint_fixConflict (/*@temp@*/ constraint good,
 647                         /*@temp@*/ /*@observer@*/ constraint conflicting)
 648    /*@modifies good@*/
 649 {
 650   llassert (constraint_isDefined (conflicting));
 651
 652   if (conflicting->ar ==EQ)
 653     {
 654       llassert (constraint_isDefined (good));
 655       good->expr = constraintExpr_searchandreplace (good->expr, conflicting->lexpr, conflicting->expr);
 656       good = constraint_simplify (good);
 657     }
 658 }
 659
 660 static bool conflict (constraint c, constraintList list)
 661 {
 662   constraintList_elements (list, el)
 663     {
 664       if (constraint_conflict (el, c))
 665         {
 666           constraint_fixConflict (el, c);
 667           return TRUE;
 668         }
 669     } end_constraintList_elements;
 670
 671   return FALSE;
 672 }
 673
 674 /*
 675 ** Check if constraint in list1 conflicts with constraints in List2.  If so we
 676 ** remove form list1 and change list2.
 677 */
 678
 679 constraintList constraintList_fixConflicts (constraintList list1, constraintList list2)
 680 {
 681   constraintList ret = constraintList_makeNew ();
 682   llassert (constraintList_isDefined (list1));
 683
 684   constraintList_elements (list1, el)
 685     {
 686       if (!conflict (el, list2))
 687         {
 688           constraint temp = constraint_copy (el);
 689           ret = constraintList_add (ret, temp);
 690         }
 691     } end_constraintList_elements;
 692
 693   return ret;
 694 }
 695
 696 /* Returns true if constraint post satifies constraint pre */
 697 static bool satifies (constraint pre, constraint post)
 698 {
 699   llassert (constraint_isDefined (pre));
 700   llassert (constraint_isDefined (post));
 701
 702   if (constraint_isAlwaysTrue (pre))
 703     {
 704       return TRUE;
 705     }
 706
 707   if (!constraintExpr_similar (pre->lexpr, post->lexpr))
 708     {
 709       return TRUE;
 710     }
 711
 712   if (!constraintExpr_similar (pre->lexpr, post->lexpr))
 713     {
 714       return FALSE;
 715     }
 716
 717   llassertretval (!constraintExpr_isUndefined (post->expr), FALSE);
 718   return rangeCheck (pre->ar, pre->expr, post->ar, post->expr);
 719 }
 720
 721 bool
 722 constraintList_resolve (/*@observer@*/ constraint c,
 723                         /*@observer@*/ constraintList p)
 724 {
 725   constraintList_elements (p, el)
 726     {
 727       if (satifies (c, el))
 728         {
 729           DPRINTF (("%s satifies %s", constraint_unparse (el), constraint_unparse(c)));
 730           return TRUE;
 731         }
 732       DPRINTF (("%s does not satify %s", constraint_unparse (el), constraint_unparse (c)));
 733     } end_constraintList_elements;
 734
 735   DPRINTF (("no constraints satisfy %s", constraint_unparse (c)));
 736   return FALSE;
 737 }
 738
 739 static bool arithType_canResolve (arithType ar1, arithType ar2)
 740 {
 741   switch (ar1)
 742     {
 743     case GTE:
 744     case GT:
 745       if ((ar2 == GT) || (ar2 == GTE) || (ar2 == EQ))
 746         {
 747           return TRUE;
 748         }
 749       break;
 750
 751     case EQ:
 752       if (ar2 == EQ)
 753         return TRUE;
 754       break;
 755
 756     case LT:
 757     case LTE:
 758       if ((ar2 == LT) || (ar2 == LTE) || (ar2 == EQ))
 759         return TRUE;
 760       break;
 761     default:
 762       return FALSE;
 763     }
 764   return FALSE;
 765 }
 766
 767 /* Checks for the case expr2 == sizeof buf1  and buf1 is a fixed array*/
 768 static bool  sizeofBufComp(constraintExpr buf1, constraintExpr expr2)
 769 {
 770   constraintTerm ct;
 771   exprNode e, t;
 772   sRef s1, s2;
 773
 774   llassert (constraintExpr_isDefined (buf1) && constraintExpr_isDefined (expr2));
 775
 776   /*@i6343 rewrite this to not need access, or move to constraintExpr module */
 777   /*@access constraintExpr@*/
 778
 779   if ((expr2->kind != term) && (buf1->kind != term))
 780     {
 781       return FALSE;
 782     }
 783
 784   ct = constraintExprData_termGetTerm(expr2->data);
 785
 786   if (!constraintTerm_isExprNode(ct))
 787     {
 788       return FALSE;
 789     }
 790
 791   e = constraintTerm_getExprNode (ct);
 792
 793   llassert (exprNode_isDefined(e));
 794
 795   if (!exprNode_isDefined (e))
 796     {
 797       return FALSE;
 798     }
 799
 800   if (e->kind != XPR_SIZEOF)
 801     {
 802       return FALSE;
 803     }
 804
 805   t = exprData_getSingle (e->edata);
 806
 807   s1 = exprNode_getSref (t);
 808   s2 = constraintTerm_getsRef(constraintExprData_termGetTerm(buf1->data));
 809
 810   /*@i223@*/ /*this may be the wronge thing to test for */
 811   if (sRef_similarRelaxed(s1, s2) || sRef_sameName (s1, s2))
 812     {
 813       /*@i22*/ /* get rid of this test of now */
 814       /* if (ctype_isFixedArray (sRef_getType (s2))) */
 815         return TRUE;
 816     }
 817   return FALSE;
 818 }
 819
 820 /* look for the special case of
 821    maxSet(buf) >= sizeof(buf) - 1
 822 */
 823
 824 /*@i223@*/ /*need to add some type checking */
 825
 826 static bool sizeOfMaxSet( /*@observer@*/ /*@temp@*/ constraint c)
 827 {
 828   constraintExpr l, r, buf1, buf2, con;
 829
 830   DPRINTF (("sizeOfMaxSet: checking %s ", constraint_unparse (c)));
 831   llassert (constraint_isDefined (c));
 832
 833   l = c->lexpr;
 834   r = c->expr;
 835
 836   if (!((c->ar == EQ) || (c->ar == GTE) || (c->ar == LTE)))
 837     {
 838       return FALSE;
 839     }
 840
 841   llassert (constraintExpr_isDefined (l));
 842   llassert (constraintExpr_isDefined (r));
 843
 844   /* Check if the constraintExpr is MaxSet(buf) */
 845
 846   if (l->kind == unaryExpr)
 847     {
 848       if (constraintExprData_unaryExprGetOp(l->data) == MAXSET)
 849         {
 850           buf1 = constraintExprData_unaryExprGetExpr(l->data);
 851         }
 852       else
 853         {
 854           return FALSE;
 855         }
 856     }
 857   else
 858     {
 859       return FALSE;
 860     }
 861
 862   if (r->kind != binaryexpr)
 863     {
 864       return FALSE;
 865     }
 866
 867   buf2 = constraintExprData_binaryExprGetExpr1 (r->data);
 868   con = constraintExprData_binaryExprGetExpr2 (r->data);
 869
 870   if (constraintExprData_binaryExprGetOp (r->data) == BINARYOP_MINUS)
 871     {
 872       if (constraintExpr_canGetValue (con))
 873         {
 874           long i = constraintExpr_getValue (con);
 875
 876           if (i != 1)
 877             {
 878               return FALSE;
 879             }
 880         }
 881       else
 882         {
 883           return FALSE;
 884         }
 885     }
 886
 887   if (constraintExprData_binaryExprGetOp (r->data) == BINARYOP_PLUS)
 888     {
 889       if (constraintExpr_canGetValue (con))
 890         {
 891           long i = constraintExpr_getValue (con);
 892
 893           if (i != -1)
 894             {
 895               return FALSE;
 896             }
 897         }
 898       else
 899         {
 900           return FALSE;
 901         }
 902     }
 903
 904   return (sizeofBufComp (buf1, buf2));
 905 }
 906 /*@i8423@*/
 907 /*@noaccess constraintExpr@*/
 908
 909 /* We look for constraint which are tautologies */
 910
 911 bool constraint_isAlwaysTrue (/*@observer@*/ /*@temp@*/ constraint c)
 912 {
 913   constraintExpr l, r;
 914   bool rHasConstant;
 915   int rConstant;
 916
 917   llassert (constraint_isDefined (c));
 918
 919   l = c->lexpr;
 920   r = c->expr;
 921
 922   DPRINTF((message("constraint_IsAlwaysTrue:examining %s", constraint_unparse(c))));
 923
 924   if (sizeOfMaxSet(c))
 925     return TRUE;
 926
 927   if (constraintExpr_canGetValue(l) && constraintExpr_canGetValue(r))
 928     {
 929       int cmp;
 930       cmp = constraintExpr_compare (l, r);
 931       switch (c->ar)
 932         {
 933         case EQ:
 934           return (cmp == 0);
 935         case GT:
 936           return (cmp > 0);
 937         case GTE:
 938           return (cmp >= 0);
 939         case LTE:
 940           return (cmp <= 0);
 941         case LT:
 942           return (cmp < 0);
 943
 944         default:
 945           BADEXIT;
 946           /*@notreached@*/
 947           break;
 948         }
 949     }
 950
 951   if (constraintExpr_similar (l,r))
 952     {
 953       switch (c->ar)
 954         {
 955         case EQ:
 956         case GTE:
 957         case LTE:
 958           return TRUE;
 959
 960         case GT:
 961         case LT:
 962           break;
 963         default:
 964           BADEXIT;
 965           /*@notreached@*/
 966           break;
 967         }
 968     }
 969
 970   l = constraintExpr_copy (c->lexpr);
 971   r = constraintExpr_copy (c->expr);
 972
 973   r = constraintExpr_propagateConstants (r, &rHasConstant, &rConstant);
 974
 975   if (constraintExpr_similar (l,r) && (rHasConstant))
 976     {
 977       DPRINTF((message("constraint_IsAlwaysTrue: after removing constants  %s and %s are similar", constraintExpr_unparse(l), constraintExpr_unparse(r))));
 978       DPRINTF((message("constraint_IsAlwaysTrue: rconstant is  %d", rConstant)));
 979
 980       constraintExpr_free(l);
 981       constraintExpr_free(r);
 982
 983       switch (c->ar)
 984         {
 985         case EQ:
 986           return (rConstant == 0);
 987         case LT:
 988           return (rConstant > 0);
 989         case LTE:
 990           return (rConstant >= 0);
 991         case GTE:
 992           return (rConstant <= 0);
 993         case GT:
 994           return (rConstant < 0);
 995
 996         default:
 997           BADEXIT;
 998           /*@notreached@*/
 999           break;
1000         }
1001     }
1002       else
1003       {
1004         constraintExpr_free(l);
1005         constraintExpr_free(r);
1006         DPRINTF((message("Constraint %s is not always true", constraint_unparse(c))));
1007         return FALSE;
1008       }
1009
1010   BADEXIT;
1011 }
1012
1013 static bool rangeCheck (arithType ar1, /*@observer@*/ constraintExpr expr1, arithType ar2, /*@observer@*/ constraintExpr expr2)
1014
1015 {
1016   DPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2))));
1017
1018   if (! arithType_canResolve (ar1, ar2))
1019     return FALSE;
1020
1021   switch (ar1)
1022  {
1023  case GTE:
1024        if (constraintExpr_similar (expr1, expr2))
1025           return TRUE;
1026        /*@fallthrough@*/
1027   case GT:
1028     if (!  (constraintExpr_canGetValue (expr1) &&
1029                constraintExpr_canGetValue (expr2)))
1030            {
1031                   constraintExpr e1, e2;
1032                   bool p1, p2;
1033                   int const1, const2;
1034
1035                   e1 = constraintExpr_copy(expr1);
1036                   e2 = constraintExpr_copy(expr2);
1037
1038                   e1 = constraintExpr_propagateConstants (e1, &p1, &const1);
1039
1040                   e2 = constraintExpr_propagateConstants (e2, &p2, &const2);
1041
1042                   if (p1 || p2)
1043                      {
1044                       if (!p1)
1045                            const1 = 0;
1046
1047                       if (!p2)
1048                            const2 = 0;
1049
1050                       if (const1 <= const2)
1051                            if (constraintExpr_similar (e1, e2))
1052                                   {
1053                                          constraintExpr_free(e1);
1054                                          constraintExpr_free(e2);
1055                                          return TRUE;
1056                                        }
1057                       }
1058                   DPRINTF(("Can't Get value"));
1059
1060                   constraintExpr_free(e1);
1061                   constraintExpr_free(e2);
1062                   return FALSE;
1063                 }
1064
1065     if (constraintExpr_compare (expr2, expr1) >= 0)
1066            return TRUE;
1067
1068    return FALSE;
1069   case EQ:
1070     if (constraintExpr_similar (expr1, expr2))
1071        return TRUE;
1072
1073     return FALSE;
1074   case LTE:
1075     if (constraintExpr_similar (expr1, expr2))
1076        return TRUE;
1077     /*@fallthrough@*/
1078   case LT:
1079      if (!  (constraintExpr_canGetValue (expr1) &&
1080                 constraintExpr_canGetValue (expr2)))
1081             {
1082                   constraintExpr e1, e2;
1083                    bool p1, p2;
1084                    int const1, const2;
1085
1086                    e1 = constraintExpr_copy(expr1);
1087                    e2 = constraintExpr_copy(expr2);
1088
1089                    e1 = constraintExpr_propagateConstants (e1, &p1, &const1);
1090
1091                    e2 = constraintExpr_propagateConstants (e2, &p2, &const2);
1092
1093                    if (p1 || p2)
1094                       {
1095                        if (!p1)
1096                             const1 = 0;
1097
1098                        if (!p2)
1099                             const2 = 0;
1100
1101                        if (const1 >= const2)
1102                             if (constraintExpr_similar (e1, e2))
1103                                    {
1104                                           constraintExpr_free(e1);
1105                                           constraintExpr_free(e2);
1106                                           return TRUE;
1107                                         }
1108                        }
1109                    constraintExpr_free(e1);
1110                    constraintExpr_free(e2);
1111
1112                    DPRINTF(("Can't Get value"));
1113                    return FALSE;
1114                  }
1115
1116     if (constraintExpr_compare (expr2, expr1) <= 0)
1117            return TRUE;
1118
1119     return FALSE;
1120
1121   default:
1122       llcontbug((message("Unhandled case in switch: %q", arithType_print(ar1))));
1123   }
1124   BADEXIT;
1125 }
1126
1127 static constraint constraint_searchandreplace (/*@returned@*/ constraint c, constraintExpr old, constraintExpr newExpr)
1128 {
1129   llassert (constraint_isDefined (c));
1130   DPRINTF (("Doing replace for lexpr"));
1131
1132   c->lexpr = constraintExpr_searchandreplace (c->lexpr, old, newExpr);
1133   DPRINTF (("Doing replace for expr"));
1134   c->expr = constraintExpr_searchandreplace (c->expr, old, newExpr);
1135   return c;
1136 }
1137
1138 bool constraint_search (constraint c, constraintExpr old) /*@*/
1139 {
1140   bool ret = FALSE;
1141
1142   llassert (constraint_isDefined (c));
1143
1144   ret  = constraintExpr_search (c->lexpr, old);
1145   ret = ret || constraintExpr_search (c->expr, old);
1146   return ret;
1147 }
1148
1149 /* adjust file locs and stuff */
1150 static constraint constraint_adjust (/*@returned@*/ constraint substitute, /*@observer@*/ constraint old)
1151 {
1152   fileloc loc1, loc2, loc3;
1153
1154   DPRINTF (("Start adjust on %s and %s", constraint_unparse (substitute),
1155             constraint_unparse (old)));
1156
1157   llassert (constraint_isDefined (substitute));
1158   llassert (constraint_isDefined (old));
1159
1160   loc1 = constraint_getFileloc (old);
1161   loc2 = constraintExpr_getFileloc (substitute->lexpr);
1162   loc3 = constraintExpr_getFileloc (substitute->expr);
1163
1164   /* special case of an equality that "contains itself" */
1165   if (constraintExpr_search (substitute->expr, substitute->lexpr))
1166     {
1167       if (fileloc_closer (loc1, loc3, loc2))
1168         {
1169           constraintExpr temp;
1170           DPRINTF (("Doing adjust on %s", constraint_unparse(substitute)));
1171           temp = substitute->lexpr;
1172           substitute->lexpr = substitute->expr;
1173           substitute->expr  = temp;
1174           substitute = constraint_simplify(substitute);
1175         }
1176     }
1177
1178   fileloc_free (loc1);
1179   fileloc_free (loc2);
1180   fileloc_free (loc3);
1181   return substitute;
1182 }
1183
1184 /*
1185 ** If function preforms substitutes based on inequality
1186 ** It uses the rule x >= y && b < y  ===> x >= b + 1
1187 ** warning this is sound but throws out information.
1188 */
1189
1190 constraint inequalitySubstitute  (/*@returned@*/ constraint c, constraintList p)
1191 {
1192   llassert (constraint_isDefined (c));
1193
1194   if (c->ar != GTE)
1195     {
1196       return c;
1197     }
1198
1199   constraintList_elements (p, el)
1200     {
1201       llassert (constraint_isDefined (el));
1202
1203       if ((el->ar == LT ))
1204           /* if (!constraint_conflict (c, el) ) */ /*@i523 explain this! */
1205         {
1206           constraintExpr temp2;
1207
1208           /*@i22*/
1209
1210           if (constraintExpr_same (el->expr, c->expr))
1211             {
1212               DPRINTF (("inequalitySubstitute Replacing %q in %q with  %q",
1213                         constraintExpr_print (c->expr),
1214                         constraint_unparse (c),
1215                         constraintExpr_print (el->expr)));
1216               temp2 = constraintExpr_copy (el->lexpr);
1217               constraintExpr_free(c->expr);
1218               c->expr =  constraintExpr_makeIncConstraintExpr (temp2);
1219             }
1220         }
1221     } end_constraintList_elements;
1222
1223   c = constraint_simplify (c);
1224   return c;
1225 }
1226
1227 /* drl7x 7/26/001
1228
1229    THis function is like inequalitySubstitute but it adds the rule
1230    added the rules x >= y &&  y <= b  ===> x >= b
1231     x >= y &&  y < b  ===> x >= b + 1
1232
1233    This is sound but sonce it throws out additional information it should only one used
1234    if we're oring constraints.
1235  */
1236
1237 static constraint inequalitySubstituteStrong (/*@returned@*/ constraint c, constraintList p)
1238 {
1239   DPRINTF (("inequalitySubstituteStrong examining substituting for %q", constraint_unparse(c)));
1240   llassert (constraint_isDefined (c));
1241
1242   if (!constraint_isDefined (c))
1243     {
1244       return c;
1245     }
1246
1247   if (c->ar != GTE)
1248     {
1249       return c;
1250     }
1251
1252   DPRINTF (("inequalitySubstituteStrong examining substituting for %q with %q",
1253             constraint_unparse (c), constraintList_unparse (p)));
1254
1255   constraintList_elements (p, el)
1256     {
1257       DPRINTF (("inequalitySubstituteStrong examining substituting %s on %s",
1258                 constraint_unparse (el), constraint_unparse (c)));
1259
1260       llassert (constraint_isDefined (el));
1261
1262       if ((el->ar == LT ) || (el->ar == LTE))
1263         /* if (!constraint_conflict (c, el) ) */ /*@i523@*/
1264         {
1265           constraintExpr temp2;
1266
1267           /*@i22*/
1268           if (constraintExpr_same (el->lexpr, c->expr))
1269             {
1270               DPRINTF (("inequalitySubstitute Replacing %s in %s with %s",
1271                         constraintExpr_print (c->expr),
1272                         constraint_unparse (c),
1273                         constraintExpr_print (el->expr)));
1274
1275               temp2 = constraintExpr_copy (el->expr);
1276               constraintExpr_free (c->expr);
1277
1278               if ((el->ar == LTE))
1279                 {
1280                   c->expr = temp2;
1281                 }
1282               else
1283                 {
1284                   c->expr =  constraintExpr_makeIncConstraintExpr (temp2);
1285                 }
1286             }
1287
1288         }
1289     } end_constraintList_elements;
1290
1291   c = constraint_simplify(c);
1292   return c;
1293 }
1294
1295
1296 /* This function performs substitutions based on the rule:
1297    for a constraint of the form expr1 >= expr2;   a < b =>
1298    a = b -1 for all a in expr1.  This will work in most cases.
1299
1300    Like inequalitySubstitute we're throwing away some information
1301 */
1302
1303 static constraint inequalitySubstituteUnsound (/*@returned@*/ constraint c, constraintList p)
1304 {
1305   DPRINTF (("Doing inequalitySubstituteUnsound"));
1306   llassert (constraint_isDefined (c));
1307
1308   if (c->ar != GTE)
1309     {
1310       return c;
1311     }
1312
1313   constraintList_elements (p, el)
1314     {
1315       llassert (constraint_isDefined (el));
1316
1317       DPRINTF (("inequalitySubstituteUnsound examining substituting %s on %s",
1318                 constraint_unparse (el), constraint_unparse (c)));
1319       if (( el->ar == LTE) || (el->ar == LT))
1320         /* if (!constraint_conflict (c, el) ) */ /*@i532@*/
1321         {
1322           constraintExpr temp2 = constraintExpr_copy (el->expr);
1323
1324           if (el->ar == LT)
1325             {
1326               temp2 = constraintExpr_makeDecConstraintExpr (temp2);
1327             }
1328
1329           DPRINTF (("Replacing %s in %s with  %s",
1330                     constraintExpr_print (el->lexpr),
1331                     constraintExpr_print (c->lexpr),
1332                     constraintExpr_print (temp2)));
1333
1334           c->lexpr = constraintExpr_searchandreplace (c->lexpr, el->lexpr, temp2);
1335           constraintExpr_free(temp2);
1336         }
1337     } end_constraintList_elements;
1338
1339   c = constraint_simplify (c);
1340   return c;
1341 }
1342
1343 /*@only@*/ constraint constraint_substitute (/*@observer@*/ /*@temp@*/ constraint c, constraintList p)
1344 {
1345   constraint ret = constraint_copy (c);
1346
1347   constraintList_elements (p, el)
1348     {
1349       llassert (constraint_isDefined (el));
1350       if (el->ar == EQ)
1351         {
1352           if (!constraint_conflict (ret, el))
1353             {
1354               constraint temp = constraint_copy (el);
1355               temp = constraint_adjust (temp, ret);
1356
1357               llassert (constraint_isDefined (temp));
1358
1359               DPRINTF (("constraint_substitute :: Substituting in %s using %s",
1360                         constraint_unparse (ret), constraint_unparse (temp)));
1361
1362               ret = constraint_searchandreplace (ret, temp->lexpr, temp->expr);
1363
1364               DPRINTF (("constraint_substitute :: The new constraint is %s", constraint_unparse (ret)));
1365               constraint_free (temp);
1366             }
1367         }
1368     } end_constraintList_elements;
1369
1370   ret = constraint_simplify (ret);
1371   DPRINTF (("constraint_substitute :: The final new constraint is %s", constraint_unparse (ret)));
1372   return ret;
1373 }
1374
1375 /*@only@*/ constraintList
1376 constraintList_substituteFreeTarget (/*@only@*/ constraintList target,
1377                                      /*@observer@*/ constraintList subList)
1378 {
1379   constraintList ret = constraintList_substitute (target, subList);
1380   constraintList_free(target);
1381   return ret;
1382 }
1383
1384 /* we try to do substitutions on each constraint in target using the constraint in sublist*/
1385
1386 /*@only@*/ constraintList
1387 constraintList_substitute (constraintList target, /*@observer@*/ constraintList subList)
1388 {
1389   constraintList ret = constraintList_makeNew();
1390
1391   constraintList_elements(target, el)
1392     {
1393       constraint temp = constraint_substitute (el, subList);
1394       /*@i3232@*/ /* drl possible problem : warning make sure that a side effect is not expected */
1395       ret = constraintList_add (ret, temp);
1396     } end_constraintList_elements;
1397
1398   return ret;
1399 }
1400
1401 static constraint constraint_solve (/*@returned@*/ constraint c)
1402 {
1403   llassert (constraint_isDefined (c));
1404   DPRINTF (("Solving %s", constraint_unparse (c)));
1405   c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr);
1406   DPRINTF (("Solved and got %s", constraint_unparse (c)));
1407   return c;
1408 }
1409
1410 static arithType flipAr (arithType ar)
1411 {
1412   switch (ar)
1413     {
1414     case LT:      return GT;
1415     case LTE:     return GTE;
1416     case EQ:      return EQ;
1417     case GT:      return LT;
1418     case GTE:     return LTE;
1419     default:      llcontbuglit ("unexpected value: case not handled");
1420     }
1421   BADEXIT;
1422 }
1423
1424 static constraint constraint_swapLeftRight (/*@returned@*/ constraint c)
1425 {
1426   constraintExpr temp;
1427
1428   llassert (constraint_isDefined (c));
1429
1430   c->ar = flipAr (c->ar);
1431   temp = c->lexpr;
1432   c->lexpr = c->expr;
1433   c->expr = temp;
1434   DPRINTF (("Swaped left and right sides of constraint"));
1435   return c;
1436 }
1437
1438 constraint constraint_simplify (/*@returned@*/ constraint c)
1439 {
1440   llassert (constraint_isDefined (c));
1441   DPRINTF (("constraint_simplify on %q ", constraint_unparse (c)));
1442
1443   if (constraint_tooDeep(c))
1444     {
1445       DPRINTF (("constraint_simplify: constraint to complex aborting %q", constraint_unparse (c)));
1446       return c;
1447     }
1448
1449   c->lexpr = constraintExpr_simplify (c->lexpr);
1450   c->expr  = constraintExpr_simplify (c->expr);
1451
1452   if (constraintExpr_isBinaryExpr (c->lexpr))
1453     {
1454       c = constraint_solve (c);
1455       c->lexpr = constraintExpr_simplify (c->lexpr);
1456       c->expr  = constraintExpr_simplify (c->expr);
1457     }
1458
1459   if (constraintExpr_isLit(c->lexpr) && (!constraintExpr_isLit(c->expr)))
1460     {
1461       c = constraint_swapLeftRight (c);
1462       /* I don't think this will be an infinite loop */
1463       c = constraint_simplify (c);
1464     }
1465
1466   DPRINTF (("constraint_simplify returning %q", constraint_unparse (c)));
1467   return c;
1468 }
1469
1470 /* returns true if fileloc for term1 is closer to file for term2 than term3*/
1471
1472 bool fileloc_closer (fileloc loc1, fileloc loc2, fileloc loc3)
1473 {
1474   if (!fileloc_isDefined (loc1))
1475     return FALSE;
1476
1477   if (!fileloc_isDefined (loc2))
1478     return FALSE;
1479
1480   if (!fileloc_isDefined (loc3))
1481     return TRUE;
1482
1483   if (fileloc_equal (loc2, loc3))
1484     return FALSE;
1485
1486   if (fileloc_equal (loc1, loc2))
1487     return TRUE;
1488
1489   if (fileloc_equal (loc1, loc3))
1490     return FALSE;
1491
1492   if (fileloc_lessthan (loc1, loc2))
1493     {
1494       if (fileloc_lessthan (loc2, loc3))
1495         {
1496           llassert (fileloc_lessthan (loc1, loc3));
1497           return TRUE;
1498         }
1499       else
1500         {
1501           return FALSE;
1502         }
1503     }
1504
1505   if (!fileloc_lessthan (loc1, loc2))
1506     {
1507       if (!fileloc_lessthan (loc2, loc3))
1508         {
1509           llassert (!fileloc_lessthan (loc1, loc3));
1510           return TRUE;
1511         }
1512       else
1513         {
1514           return FALSE;
1515         }
1516     }
1517
1518   llassert(FALSE);
1519   return FALSE;
1520 }
1521
1522