src/constraint.c

   1 /*
   2 ** constraintList.c
   3 */
   4
   5 //#define DEBUGPRINT 1
   6
   7 # include <ctype.h> /* for isdigit */
   8 # include "lclintMacros.nf"
   9 # include "basic.h"
  10 # include "cgrammar.h"
  11 # include "cgrammar_tokens.h"
  12
  13 # include "exprChecks.h"
  14 # include "aliasChecks.h"
  15 # include "exprNodeSList.h"
  16 //# include "exprData.i"
  17
  18 /*@i33*/
  19 /*@-fcnuse*/
  20 /*@-assignexpose*/
  21
  22 /*@notnull@*/ constraint constraint_makeNew (void);
  23
  24
  25 constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant)
  26
  27 {
  28   char *t;
  29   int c;
  30   constraint ret;
  31   ret = constraint_makeNew();
  32   llassert (sRef_isValid(x) );
  33   if (!sRef_isValid(x))
  34     return ret;
  35
  36
  37   ret->lexpr = constraintExpr_makeTermsRef (x);
  38   #warning fix abstraction
  39
  40   if (relOp.tok == GE_OP)
  41       ret->ar = GTE;
  42   else if (relOp.tok == LE_OP)
  43     ret->ar = LTE;
  44   else if (relOp.tok == EQ_OP)
  45     ret->ar = EQ;
  46   else
  47     llfatalbug(message ("Unsupported relational operator") );
  48
  49
  50   t =  cstring_toCharsSafe (exprNode_unparse(cconstant));
  51   c = atoi( t );
  52   ret->expr = constraintExpr_makeIntLiteral (c);
  53
  54   ret->post = TRUE;
  55   //  ret->orig = ret;
  56   DPRINTF(("GENERATED CONSTRAINT:"));
  57   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
  58   return ret;
  59 }
  60
  61 constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
  62
  63 {
  64   char *t;
  65   int c;
  66   constraint ret;
  67   ret = constraint_makeNew();
  68   llassert (l!=NULL);
  69   if (!l)
  70     return ret;
  71
  72
  73   ret->lexpr = constraintExpr_copy (l);
  74   #warning fix abstraction
  75
  76   if (relOp.tok == GE_OP)
  77       ret->ar = GTE;
  78   else if (relOp.tok == LE_OP)
  79     ret->ar = LTE;
  80   else if (relOp.tok == EQ_OP)
  81     ret->ar = EQ;
  82   else
  83   llfatalbug(message("Unsupported relational operator") );
  84
  85
  86   t =  cstring_toCharsSafe (exprNode_unparse(cconstant));
  87   c = atoi( t );
  88   ret->expr = constraintExpr_makeIntLiteral (c);
  89
  90   ret->post = TRUE;
  91   //  ret->orig = ret;
  92   DPRINTF(("GENERATED CONSTRAINT:"));
  93   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
  94   return ret;
  95 }
  96
  97 constraint constraint_same (constraint c1, constraint c2)
  98 {
  99
 100   if (c1->ar != c2->ar)
 101     return FALSE;
 102
 103   if (!constraintExpr_similar (c1->lexpr, c2->lexpr) )
 104     return FALSE;
 105
 106   if (!constraintExpr_similar (c1->expr, c2->expr) )
 107     return FALSE;
 108
 109   return TRUE;
 110 }
 111
 112 constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
 113 {
 114   constraint ret;
 115   ret = constraint_makeNew();
 116   llassert (l !=NULL);
 117   if (!l)
 118     return ret;
 119
 120
 121   ret->lexpr = constraintExpr_copy (l);
 122   #warning fix abstraction
 123
 124   if (relOp.tok == GE_OP)
 125       ret->ar = GTE;
 126   else if (relOp.tok == LE_OP)
 127     ret->ar = LTE;
 128   else if (relOp.tok == EQ_OP)
 129     ret->ar = EQ;
 130   else
 131   llfatalbug( message("Unsupported relational operator") );
 132
 133   ret->expr = constraintExpr_copy (r);
 134
 135   ret->post = TRUE;
 136
 137   ret->orig = constraint_copy(ret);
 138
 139   ret = constraint_simplify (ret);
 140
 141   //  ret->orig = ret;
 142   DPRINTF(("GENERATED CONSTRAINT:"));
 143   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
 144   return ret;
 145 }
 146
 147 constraint constraint_copy (constraint c)
 148 {
 149   constraint ret;
 150
 151   llassert (c);
 152
 153   ret = constraint_makeNew();
 154   ret->lexpr = constraintExpr_copy (c->lexpr);
 155   ret->ar = c->ar;
 156   ret->expr =  constraintExpr_copy (c->expr);
 157   ret->post = c->post;
 158   ret->generatingExpr = exprNode_fakeCopy(c->generatingExpr);
 159
 160   /*@i33 fix this*/
 161   if (c->orig != NULL)
 162     ret->orig = constraint_copy (c->orig);
 163   else
 164     ret->orig = NULL;
 165
 166   if (c->or != NULL)
 167     ret->or = constraint_copy (c->or);
 168   else
 169     ret->or = NULL;
 170
 171   return ret;
 172 }
 173
 174 /*like copy expect it doesn't allocate memory for the constraint*/
 175
 176 void constraint_overWrite (constraint c1, constraint c2)
 177 {
 178   c1->lexpr = constraintExpr_copy (c2->lexpr);
 179   c1->ar = c2->ar;
 180   c1->expr =  constraintExpr_copy (c2->expr);
 181   c1->post = c2->post;
 182   /*@i33 fix this*/
 183   if (c2->orig != NULL)
 184     c1->orig = constraint_copy (c2->orig);
 185   else
 186     c1->orig = NULL;
 187
 188   if (c2->or != NULL)
 189     c1->or = constraint_copy (c2->or);
 190   else
 191     c1->or = NULL;
 192
 193   c1->generatingExpr = exprNode_fakeCopy (c2->generatingExpr );
 194 }
 195
 196 bool constraint_resolve (/*@unused@*/ constraint c)
 197 {
 198   return FALSE;
 199 }
 200
 201
 202
 203 /*@notnull@*/ constraint constraint_makeNew (void)
 204 {
 205   constraint ret;
 206   ret = dmalloc(sizeof (*ret) );
 207   ret->lexpr = NULL;
 208   ret->expr = NULL;
 209   ret->ar = LT;
 210   ret->post = FALSE;
 211   ret->orig = NULL;
 212   ret->or = NULL;
 213   ret->generatingExpr = NULL;
 214   return ret;
 215 }
 216
 217 constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
 218 {
 219
 220   if (c->generatingExpr == NULL)
 221     {
 222       c->generatingExpr = exprNode_fakeCopy(e);
 223       DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
 224     }
 225   else
 226     {
 227       DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
 228     }
 229   return c;
 230 }
 231
 232 fileloc constraint_getFileloc (constraint c)
 233 {
 234   if (c->generatingExpr)
 235     return (exprNode_getfileloc (c->generatingExpr) );
 236
 237   return (constraintExpr_getFileloc (c->lexpr) );
 238
 239
 240 }
 241
 242 static bool checkForMaxSet (constraint c)
 243 {
 244   if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) )
 245     return TRUE;
 246
 247   return FALSE;
 248 }
 249
 250 bool constraint_hasMaxSet(constraint c)
 251 {
 252   if (c->orig != NULL)
 253     {
 254       if (checkForMaxSet(c->orig) )
 255         return TRUE;
 256     }
 257
 258   return (checkForMaxSet(c) );
 259 }
 260
 261 constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
 262 {
 263   constraint ret = constraint_makeNew();
 264   //  constraintTerm term;
 265   po = exprNode_fakeCopy(po);
 266   ind = exprNode_fakeCopy(ind);
 267   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 268   ret->ar    = GTE;
 269   ret->expr  = constraintExpr_makeValueExpr (ind);
 270   return ret;
 271 }
 272
 273 constraint constraint_makeWriteSafeInt (exprNode po, int ind)
 274 {
 275   constraint ret = constraint_makeNew();
 276
 277
 278   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 279   ret->ar = GTE;
 280   ret->expr =  constraintExpr_makeValueInt (ind);
 281   /*@i1*/return ret;
 282 }
 283
 284 constraint constraint_makeSRefSetBufferSize (sRef s, int size)
 285 {
 286  constraint ret = constraint_makeNew();
 287  ret->lexpr = constraintExpr_makeSRefMaxset (s);
 288  ret->ar = EQ;
 289  ret->expr =  constraintExpr_makeValueInt (size);
 290  ret->post = TRUE;
 291  /*@i1*/return ret;
 292 }
 293
 294 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
 295 {
 296   constraint ret = constraint_makeNew();
 297
 298
 299   ret->lexpr = constraintExpr_makeSRefMaxset (s);
 300   ret->ar = GTE;
 301   ret->expr =  constraintExpr_makeValueInt (ind);
 302   ret->post = TRUE;
 303   /*@i1*/return ret;
 304 }
 305
 306 /* drl added 01/12/2000
 307
 308   makes the constraint: Ensures index <= MaxRead(buffer) */
 309
 310 constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer)
 311 {
 312   constraint ret = constraint_makeNew();
 313
 314   ret->lexpr = constraintExpr_makeValueExpr (index);
 315   ret->ar = LTE;
 316   ret->expr = constraintExpr_makeMaxReadExpr(buffer);
 317   ret->post = TRUE;
 318   return ret;
 319 }
 320
 321 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
 322 {
 323   constraint ret = constraint_makeNew();
 324
 325
 326   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 327   ret->ar = GTE;
 328   ret->expr =  constraintExpr_makeValueExpr (ind);
 329   /*@i1*/return ret;
 330 }
 331
 332
 333 constraint constraint_makeReadSafeInt ( exprNode po, int ind)
 334 {
 335   constraint ret = constraint_makeNew();
 336
 337   po = exprNode_fakeCopy(po);
 338
 339   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 340   ret->ar    = GTE;
 341   ret->expr  = constraintExpr_makeValueInt (ind);
 342   return ret;
 343 }
 344
 345 constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
 346 {
 347   constraint ret = constraint_makeNew();
 348
 349
 350   ret->lexpr = constraintExpr_makeSRefMaxRead (s);
 351   ret->ar = GTE;
 352   ret->expr =  constraintExpr_makeValueInt (ind);
 353   ret->post = TRUE;
 354   /*@i1*/return ret;
 355 }
 356
 357 constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
 358 {
 359   constraint ret = constraint_makeNew();
 360
 361
 362   e1 = exprNode_fakeCopy (e1);
 363   t2 = exprNode_fakeCopy (t2);
 364
 365   ret = constraint_makeReadSafeExprNode(e1, t2);
 366
 367   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 368
 369   ret->post = TRUE;
 370
 371   //  fileloc_incColumn (ret->lexpr->term->loc);
 372   return ret;
 373 }
 374
 375 static constraint constraint_makeEnsuresOpConstraintExpr (constraintExpr c1, constraintExpr c2, fileloc sequencePoint,  arithType  ar)
 376 {
 377
 378   constraint ret;
 379
 380   llassert(c1 && c2);
 381   //  llassert(sequencePoint);
 382
 383   ret = constraint_makeNew();
 384
 385   ret->lexpr = c1;
 386   ret->ar = ar;
 387   ret->post = TRUE;
 388   ret->expr =  c2;
 389   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 390   return ret;
 391 }
 392
 393 static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint,  arithType  ar)
 394 {
 395   constraintExpr c1, c2;
 396   constraint ret;
 397   exprNode e;
 398
 399   if (! (e1 && e2) )
 400     {
 401       llcontbug((message("null exprNode, Exprnodes are %s and %s",
 402                        exprNode_unparse(e1), exprNode_unparse(e2) )
 403                ));
 404     }
 405
 406   //  llassert (sequencePoint);
 407
 408   e  =  exprNode_fakeCopy(e1);
 409   c1 =  constraintExpr_makeValueExpr (e);
 410
 411   e  =  exprNode_fakeCopy(e2);
 412   c2 =  constraintExpr_makeValueExpr (e);
 413
 414   ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
 415
 416   return ret;
 417 }
 418
 419
 420 /* make constraint ensures e1 == e2 */
 421
 422 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 423 {
 424   return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
 425 }
 426
 427 /*make constraint ensures e1 < e2 */
 428 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 429 {
 430   constraintExpr t1, t2;
 431
 432   t1 = constraintExpr_makeValueExpr (e1);
 433   t2 = constraintExpr_makeValueExpr (e2);
 434
 435   /*change this to e1 <= (e2 -1) */
 436
 437   t2 = constraintExpr_makeDecConstraintExpr (t2);
 438
 439  return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE) );
 440 }
 441
 442 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 443 {
 444  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
 445 }
 446
 447 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 448 {
 449   constraintExpr t1, t2;
 450
 451   t1 = constraintExpr_makeValueExpr (e1);
 452   t2 = constraintExpr_makeValueExpr (e2);
 453
 454
 455   /* change this to e1 >= (e2 + 1) */
 456   t2 = constraintExpr_makeIncConstraintExpr (t2);
 457
 458
 459  return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE) );
 460 }
 461
 462 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 463 {
 464  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
 465 }
 466
 467
 468 exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
 469 {
 470   dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
 471   dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
 472   dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
 473   dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
 474   return dst;
 475 }
 476
 477 constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
 478 {
 479   constraint ret = constraint_makeNew();
 480   //constraintTerm term;
 481
 482   e = exprNode_fakeCopy(e);
 483   ret->lexpr = constraintExpr_makeValueExpr (e);
 484   ret->ar = EQ;
 485   ret->post = TRUE;
 486   ret->expr =  constraintExpr_makeValueExpr (e);
 487   ret->expr =  constraintExpr_makeDecConstraintExpr (ret->expr);
 488
 489   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 490 //   fileloc_incColumn (  ret->lexpr->term->loc);
 491 //   fileloc_incColumn (  ret->lexpr->term->loc);
 492   return ret;
 493 }
 494 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 495 {
 496   constraint ret = constraint_makeNew();
 497   //constraintTerm term;
 498
 499   e = exprNode_fakeCopy(e);
 500   ret->lexpr = constraintExpr_makeValueExpr (e);
 501   ret->ar = EQ;
 502   ret->post = TRUE;
 503   ret->expr =  constraintExpr_makeValueExpr (e);
 504   ret->expr =  constraintExpr_makeIncConstraintExpr (ret->expr);
 505
 506   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 507 //   fileloc_incColumn (  ret->lexpr->term->loc);
 508 //   fileloc_incColumn (  ret->lexpr->term->loc);
 509   return ret;
 510 }
 511
 512
 513
 514 // constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 515 // {
 516 //   constraint ret = constraint_makeNew();
 517 //   //constraintTerm term;
 518
 519 //   e = exprNode_fakeCopy(e);
 520 //   ret->lexpr = constraintExpr_makeMaxReadExpr(e);
 521 //   ret->ar = EQ;
 522 //   ret->post = TRUE;
 523 //   ret->expr = constraintExpr_makeIncConstraintExpr (e);
 524 //   ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
 525 //   return ret;
 526 // }
 527
 528
 529 cstring arithType_print (arithType ar) /*@*/
 530 {
 531   cstring st = cstring_undefined;
 532   switch (ar)
 533     {
 534     case LT:
 535       st = cstring_makeLiteral (" < ");
 536       break;
 537     case        LTE:
 538       st = cstring_makeLiteral (" <= ");
 539       break;
 540     case        GT:
 541       st = cstring_makeLiteral (" > ");
 542       break;
 543     case        GTE:
 544       st = cstring_makeLiteral (" >= ");
 545       break;
 546     case        EQ:
 547       st = cstring_makeLiteral (" == ");
 548       break;
 549     case        NONNEGATIVE:
 550       st = cstring_makeLiteral (" NONNEGATIVE ");
 551       break;
 552     case        POSITIVE:
 553       st = cstring_makeLiteral (" POSITIVE ");
 554       break;
 555     default:
 556       llassert(FALSE);
 557       break;
 558     }
 559   return st;
 560 }
 561
 562 void constraint_printError (constraint c, fileloc loc)
 563 {
 564   cstring string;
 565   fileloc errorLoc;
 566
 567   string = constraint_printDetailed (c);
 568
 569   errorLoc = loc;
 570
 571   if (constraint_getFileloc(c) )
 572     /*@-branchstate@*/
 573       errorLoc = constraint_getFileloc(c);
 574   /*@=branchstate@*/
 575
 576   if (c->post)
 577     {
 578        voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
 579     }
 580   else
 581     {
 582       voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
 583     }
 584
 585 }
 586
 587 cstring  constraint_printDetailed (constraint c)
 588 {
 589   cstring st = cstring_undefined;
 590
 591
 592   if (!c->post)
 593     {
 594     if (c->orig != NULL)
 595       st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisfy %s", constraint_print (c), constraint_print(c->orig) );
 596     else
 597       st = message ("Unresolved constraint:\nLclint is unable to resolve %s", constraint_print (c));
 598
 599     }
 600   else
 601     {
 602       if (c->orig != NULL)
 603         st = message ("Block Post condition:\nThis function block has the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
 604       else
 605         st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c));
 606     }
 607
 608   if (context_getFlag (FLG_CONSTRAINTLOCATION) )
 609     {
 610       cstring temp;
 611       // llassert (c->generatingExpr);
 612       temp = message ("\nOriginal Generating expression %s: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
 613                       exprNode_unparse(c->generatingExpr) );
 614       st = cstring_concat (st, temp);
 615
 616       if (constraint_hasMaxSet(c) )
 617         {
 618           cstring temp2;
 619           temp2 = message ("\nHas MaxSet\n");
 620           st = cstring_concat (st, temp2);
 621         }
 622     }
 623   return st;
 624 }
 625
 626 cstring  constraint_print (constraint c) /*@*/
 627 {
 628   cstring st = cstring_undefined;
 629   cstring type = cstring_undefined;
 630   llassert (c !=NULL);
 631   if (c->post)
 632     {
 633       type = cstring_makeLiteral ("Ensures: ");
 634     }
 635   else
 636     {
 637       type = cstring_makeLiteral ("Requires: ");
 638     }
 639   st = message ("%s: %s %s %s",
 640                 type,
 641                 constraintExpr_print (c->lexpr),
 642                 arithType_print(c->ar),
 643                 constraintExpr_print(c->expr)
 644                 );
 645   return st;
 646 }
 647
 648 cstring  constraint_printOr (constraint c) /*@*/
 649 {
 650   cstring ret;
 651   constraint temp;
 652
 653   ret = cstring_undefined;
 654   temp = c;
 655
 656   ret = cstring_concat (ret, constraint_print(temp) );
 657
 658   temp = temp->or;
 659
 660   while (temp)
 661     {
 662       ret = cstring_concat (ret, cstring_makeLiteral (" OR ") );
 663       ret = cstring_concat (ret, constraint_print(temp) );
 664       temp = temp->or;
 665     }
 666
 667   return ret;
 668
 669 }
 670
 671 /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
 672                                                    exprNodeList arglist)
 673 {
 674   precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
 675                                                            arglist);
 676   precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
 677                                                            arglist);
 678
 679   return precondition;
 680 }
 681
 682
 683 constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
 684 {
 685   postcondition = constraint_copy (postcondition);
 686   postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
 687   postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
 688
 689   return postcondition;
 690 }
 691
 692 constraint constraint_doSRefFixConstraintParam (constraint precondition,
 693                                                    exprNodeList arglist)
 694 {
 695
 696   precondition = constraint_copy (precondition);
 697   precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
 698   precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
 699
 700   return precondition;
 701 }
 702
 703 // bool constraint_hasTerm (constraint c, constraintTerm term)
 704 // {
 705 //   DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
 706
 707 //   if (constraintExpr_includesTerm (c->lexpr, term) )
 708 //     return TRUE;
 709
 710 //   if (constraintExpr_includesTerm (c->expr, term) )
 711 //     return TRUE;
 712
 713 //   return FALSE;
 714 // }
 715
 716 /*@only@*/ constraint constraint_preserveOrig (/*@returned@*/ /*@only@*/ constraint c) /*@modifies c @*/
 717 {
 718   c->orig = constraint_copy (c);
 719   return c;
 720 }
 721 /*@=fcnuse*/
 722 /*@=assignexpose*/
 723 /*@=czechfcns@*/