Fixed bug cause spurious bounds errors.

Made +orconstraint the default
Also small bug fix in code reading in splint libraries

The bug was that
code like:
int a[12];
for (i = 0; i < 12; i++)
  a[i] = 0;

  would be marked as a potential bounds error.

diff --git a/Makefile.am b/Makefile.am
index 3beeb1d1ed222197099ad1811f6c2b65bd5794f6..38450a1f1346237a22814f93537338d5b135e8fa 100644 (file)
--- a/Makefile.am
+++ b/Makefile.am
@@ -29,7 +29,7 @@
 AUTOMAKE_OPTIONS = 1.5 foreign
 
 binaryfixscript = ./fixBinaryDist.sh
-SUBDIRS =   lib imports test doc src
+SUBDIRS =   src lib imports test doc
 
 binaryDir = bin
 binaryDirFiles =  $(binaryDir)/Makefile.am $(binaryDir)/Makefile.in

diff --git a/Makefile.in b/Makefile.in
index d299af7123db05a7f70815643b3f4ae755e8e7d7..70349f6f5dea82d36a77560083c6903509aacf17 100644 (file)
--- a/Makefile.in
+++ b/Makefile.in
@@ -88,7 +88,7 @@ install_sh = @install_sh@
 AUTOMAKE_OPTIONS = 1.5 foreign
 
 binaryfixscript = ./fixBinaryDist.sh
-SUBDIRS = lib imports test doc src
+SUBDIRS = src lib imports test doc
 
 binaryDir = bin
 binaryDirFiles = $(binaryDir)/Makefile.am $(binaryDir)/Makefile.in

diff --git a/src/cgrammar.c.der b/src/cgrammar.c.der
index 4be861899be702be091292f73c53a87ff6c2151d..8d84bff8c2ec0efb4bd3b523beae9140aa0d0bba 100644 (file)
--- a/src/cgrammar.c.der
+++ b/src/cgrammar.c.der
@@ -759,37 +759,37 @@ static const short yyrline[] = { 0,
   1217,  1218,  1219,  1220,  1221,  1222,  1223,  1224,  1225,  1232,
   1233,  1234,  1235,  1236,  1237,  1238,  1239,  1240,  1241,  1242,
   1243,  1244,  1245,  1248,  1252,  1253,  1257,  1258,  1262,  1263,
-  1264,  1267,  1268,  1272,  1279,  1281,  1283,  1285,  1287,  1289,
-  1290,  1292,  1294,  1296,  1298,  1299,  1300,  1303,  1304,  1306,
-  1308,  1309,  1312,  1315,  1316,  1317,  1320,  1322,  1326,  1328,
-  1332,  1333,  1334,  1338,  1340,  1340,  1342,  1345,  1347,  1349,
-  1352,  1357,  1364,  1365,  1366,  1372,  1376,  1377,  1381,  1382,
-  1385,  1386,  1387,  1390,  1391,  1394,  1395,  1396,  1397,  1400,
-  1401,  1404,  1405,  1408,  1409,  1410,  1413,  1413,  1414,  1415,
-  1418,  1430,  1446,  1447,  1450,  1451,  1452,  1455,  1456,  1459,
-  1461,  1462,  1464,  1465,  1467,  1469,  1471,  1473,  1479,  1480,
-  1481,  1482,  1483,  1484,  1485,  1486,  1487,  1491,  1494,  1497,
-  1498,  1502,  1504,  1506,  1508,  1512,  1513,  1515,  1519,  1521,
-  1523,  1526,  1527,  1528,  1529,  1530,  1531,  1532,  1533,  1534,
-  1535,  1536,  1537,  1538,  1541,  1542,  1547,  1550,  1553,  1554,
-  1557,  1558,  1559,  1560,  1561,  1562,  1563,  1564,  1565,  1566,
-  1567,  1570,  1571,  1578,  1579,  1585,  1586,  1587,  1588,  1591,
-  1592,  1593,  1594,  1597,  1598,  1602,  1605,  1608,  1611,  1614,
-  1617,  1620,  1621,  1622,  1623,  1625,  1626,  1628,  1630,  1636,
-  1640,  1642,  1644,  1646,  1650,  1651,  1654,  1655,  1658,  1659,
-  1662,  1663,  1666,  1667,  1670,  1671,  1674,  1675,  1676,  1679,
-  1692,  1697,  1698,  1702,  1703,  1706,  1711,  1714,  1715,  1716,
-  1724,  1725,  1725,  1729,  1730,  1731,  1742,  1749,  1750,  1753,
-  1754,  1757,  1758,  1759,  1760,  1761,  1763,  1764,  1765,  1766,
-  1769,  1770,  1771,  1772,  1773,  1774,  1775,  1776,  1777,  1778,
-  1781,  1782,  1785,  1786,  1787,  1788,  1791,  1792,  1793,  1796,
-  1797,  1798,  1801,  1802,  1803,  1804,  1805,  1808,  1809,  1810,
-  1813,  1814,  1817,  1818,  1822,  1823,  1826,  1827,  1830,  1831,
-  1834,  1835,  1836,  1837,  1840,  1841,  1842,  1843,  1844,  1845,
-  1846,  1847,  1848,  1849,  1850,  1851,  1854,  1855,  1858,  1861,
-  1863,  1865,  1869,  1870,  1872,  1874,  1877,  1878,  1879,  1881,
-  1882,  1883,  1884,  1885,  1886,  1887,  1890,  1891,  1894,  1895,
-  1898,  1901,  1902,  1903,  1904,  1905,  1908,  1909,  1910,  1911
+  1264,  1267,  1268,  1272,  1277,  1279,  1281,  1283,  1285,  1287,
+  1288,  1290,  1292,  1294,  1296,  1297,  1298,  1301,  1302,  1304,
+  1306,  1307,  1310,  1313,  1314,  1315,  1318,  1320,  1324,  1326,
+  1330,  1331,  1332,  1336,  1338,  1338,  1340,  1343,  1345,  1347,
+  1350,  1355,  1362,  1363,  1364,  1370,  1374,  1375,  1379,  1380,
+  1383,  1384,  1385,  1388,  1389,  1392,  1393,  1394,  1395,  1398,
+  1399,  1402,  1403,  1406,  1407,  1408,  1411,  1411,  1412,  1413,
+  1416,  1428,  1444,  1445,  1448,  1449,  1450,  1453,  1454,  1457,
+  1459,  1460,  1462,  1463,  1465,  1467,  1469,  1471,  1477,  1478,
+  1479,  1480,  1481,  1482,  1483,  1484,  1485,  1489,  1492,  1495,
+  1496,  1500,  1502,  1504,  1506,  1510,  1511,  1513,  1517,  1519,
+  1521,  1524,  1525,  1526,  1527,  1528,  1529,  1530,  1531,  1532,
+  1533,  1534,  1535,  1536,  1539,  1540,  1545,  1548,  1551,  1552,
+  1555,  1556,  1557,  1558,  1559,  1560,  1561,  1562,  1563,  1564,
+  1565,  1568,  1569,  1576,  1577,  1583,  1584,  1585,  1586,  1589,
+  1590,  1591,  1592,  1595,  1596,  1600,  1603,  1606,  1609,  1612,
+  1615,  1618,  1619,  1620,  1621,  1623,  1624,  1626,  1628,  1634,
+  1638,  1640,  1642,  1644,  1648,  1649,  1652,  1653,  1656,  1657,
+  1660,  1661,  1664,  1665,  1668,  1669,  1672,  1673,  1674,  1677,
+  1690,  1695,  1696,  1700,  1701,  1704,  1709,  1712,  1713,  1714,
+  1722,  1723,  1723,  1727,  1728,  1729,  1740,  1747,  1748,  1751,
+  1752,  1755,  1756,  1757,  1758,  1759,  1761,  1762,  1763,  1764,
+  1767,  1768,  1769,  1770,  1771,  1772,  1773,  1774,  1775,  1776,
+  1779,  1780,  1783,  1784,  1785,  1786,  1789,  1790,  1791,  1794,
+  1795,  1796,  1799,  1800,  1801,  1802,  1803,  1806,  1807,  1808,
+  1811,  1812,  1815,  1816,  1820,  1821,  1824,  1825,  1828,  1829,
+  1832,  1833,  1834,  1835,  1838,  1839,  1840,  1841,  1842,  1843,
+  1844,  1845,  1846,  1847,  1848,  1849,  1852,  1853,  1856,  1859,
+  1861,  1863,  1867,  1868,  1870,  1872,  1875,  1876,  1877,  1879,
+  1880,  1881,  1882,  1883,  1884,  1885,  1888,  1889,  1892,  1893,
+  1896,  1899,  1900,  1901,  1902,  1903,  1906,  1907,  1908,  1909
 };
 #endif
 
@@ -4447,7 +4447,7 @@ case 396:
 { sRef_clearGlobalScopeSafe (); ;
     break;}
 case 397:
-{ ctype ct; ct = declareStruct (yyvsp[-9].cname, yyvsp[-4].flist); /* setGlobalStructInfo(ct, $12);*/ yyval.ctyp = ct; ;
+{ ctype ct; ct = declareStruct (yyvsp[-9].cname, yyvsp[-4].flist); setGlobalStructInfo(ct, yyvsp[0].conL); yyval.ctyp = ct; ;
     break;}
 case 398:
 { sRef_setGlobalScopeSafe (); ;

diff --git a/src/cgrammar.y b/src/cgrammar.y
index 4a08b45a6a67832750e8596b6b4c274248ae08b9..da66257091702d0c4139e5c236930dd0676ad23a 100644 (file)
--- a/src/cgrammar.y
+++ b/src/cgrammar.y
@@ -1270,18 +1270,16 @@ optCompleteType
 
 optStructInvariant
 : /* empty */ { $$ = constraintList_undefined; }
-/* don't want to have support for structure invariant until we're
-   sure it's stable
+/*  drl commenting before a CVS commit 
    |  QINVARIANT BufConstraintList QENDMACRO { $$ = $2 }
 */
-
 suSpc
  : NotType CSTRUCT newId IsType TLBRACE { sRef_setGlobalScopeSafe (); } 
    CreateStructInnerScope 
    structDeclList  DeleteStructInnerScope { sRef_clearGlobalScopeSafe (); }
    TRBRACE 
    optStructInvariant 
-   { ctype ct; ct = declareStruct ($3, $8); /* setGlobalStructInfo(ct, $12);*/ $$ = ct; } 
+   { ctype ct; ct = declareStruct ($3, $8); setGlobalStructInfo(ct, $12); $$ = ct; } 
  | NotType CUNION  newId IsType TLBRACE { sRef_setGlobalScopeSafe (); } 
    CreateStructInnerScope 
    structDeclList DeleteStructInnerScope { sRef_clearGlobalScopeSafe (); } 

diff --git a/src/constraint.c b/src/constraint.c
index cb87d1025e6e0550d5eb06a81a7f2c6e60df90bf..71c3855093eade6be2c43f29475faf9a22e661a0 100644 (file)
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -482,6 +482,7 @@ constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequenc
 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 {
   constraintExpr t1, t2;
+  constraint t3;
 
   t1 = constraintExpr_makeValueExpr (e1);
   t2 = constraintExpr_makeValueExpr (e2);
@@ -489,8 +490,11 @@ constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequ
   /*change this to e1 <= (e2 -1) */
 
   t2 = constraintExpr_makeDecConstraintExpr (t2);
-  
- return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE));
+
+  t3 =  constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE);
+
+  t3 = constraint_simplify(t3);
+  return (t3);
 }
 
 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
@@ -501,6 +505,7 @@ constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc
 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 {
   constraintExpr t1, t2;
+  constraint t3;
 
   t1 = constraintExpr_makeValueExpr (e1);
   t2 = constraintExpr_makeValueExpr (e2);
@@ -509,8 +514,11 @@ constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc s
   /* change this to e1 >= (e2 + 1) */
   t2 = constraintExpr_makeIncConstraintExpr (t2);
   
+  t3 =  constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE);
+
+  t3 = constraint_simplify(t3);
   
- return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE));
+  return t3;
 }
 
 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
@@ -983,7 +991,7 @@ constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exp
   precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
 
   precondition->fcnPre = FALSE;
-  return precondition;
+  return constraint_simplify(precondition);
 }
 
 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/

diff --git a/src/constraintResolve.c b/src/constraintResolve.c
index 9cbc788d2feed66d4cdd39d7e2cdf0a3987efddd..6f795b399bc2392354e954d5aca03d4c3b616329 100644 (file)
--- a/src/constraintResolve.c
+++ b/src/constraintResolve.c
@@ -384,12 +384,22 @@ static /*@only@*/ constraint doResolve (/*@only@*/ constraint c, constraintList
   constraint temp;
 
   llassert(constraint_isUndefined (c->or ) );
+
+  DPRINTF((message("doResolve:: call on constraint c = : %q and constraintList %q",
+                  constraint_printOr(c), constraintList_print(post1)
+                  )
+          ));
   
   if (!resolveOr (c, post1) )
     {
       
       temp = constraint_substitute (c, post1);
       
+      DPRINTF((message("doResolve:: after substitute temp is %q",
+                  constraint_printOr(temp)
+                      )
+              ));
+  
       if (!resolveOr (temp, post1) )
        {
          /* try inequality substitution */
@@ -413,11 +423,57 @@ static /*@only@*/ constraint doResolve (/*@only@*/ constraint c, constraintList
                  if (!resolveOr (temp2, post1) )
                    {
                      if (!constraint_same (temp, temp2) )
-                       temp = constraint_addOr (temp, temp2);
-                     
+                       {
+                         /* drl added 8/28/2002*/
+                         /*make sure that the information from
+                           a post condition like i = i + 1 is transfered
+                         */
+                         constraint tempSub;
+                         tempSub = constraint_substitute (temp2, post1);
+
+                         DPRINTF((
+                                  message("doResolve: adding %s ",
+                                          constraint_printOr(tempSub)
+                                          )
+                                  ));
+                         
+                         DPRINTF((
+                                  message("doResolve: not adding %s ",
+                                          constraint_printOr(temp2)
+                                          )
+                                  ));
+                         
+                         temp = constraint_addOr (temp, tempSub);
+                         constraint_free(tempSub);
+                         
+                       }
                      if (!constraint_same (temp, temp3) && !constraint_same (temp3, temp2) )
-                       temp = constraint_addOr (temp, temp3);
-                     
+                       {
+                        /* drl added 8/28/2002*/
+                         /*make sure that the information from
+                           a post condition like i = i + 1 is transfered
+                         */
+                         constraint tempSub;
+                         
+                         tempSub = constraint_substitute (temp3, post1);
+
+                         DPRINTF((
+                                  message("doResolve: adding %s ",
+                                          constraint_printOr(tempSub)
+                                          )
+                                  ));
+
+                         
+                         DPRINTF((
+                                  message("doResolve: not adding %s ",
+                                          constraint_printOr(temp3)
+                                          )
+                                  ));
+
+                         temp = constraint_addOr (temp, tempSub);
+
+                         constraint_free(tempSub);
+                       }
                      *resolved = FALSE;
                      
                      constraint_free(temp2);
@@ -1292,20 +1348,22 @@ static constraint  inequalitySubstituteUnsound  (/*@returned@*/ constraint c, co
             
             temp = constraint_adjust(temp, ret);
 
-            DPRINTF((message ("Substituting %s in the constraint %s",
-                              constraint_print (temp), constraint_print (ret)
+            DPRINTF((message ("constraint_substitute :: Substituting in %s using %s",
+                              constraint_print (ret), constraint_print (temp)
                               ) ) );
                               
          
             ret = constraint_searchandreplace (ret, temp->lexpr, temp->expr);
-            DPRINTF(( message ("The new constraint is %s", constraint_print (ret) ) ));
+            DPRINTF(( message (" constraint_substitute :: The new constraint is %s", constraint_print (ret) ) ));
             constraint_free(temp);
           }
     }
   end_constraintList_elements;
-  DPRINTF(( message ("The finial new constraint is %s", constraint_print (ret) ) ));
 
   ret = constraint_simplify(ret);
+
+  DPRINTF(( message (" constraint_substitute :: The final new constraint is %s", constraint_print (ret) ) ));
+
   return ret;
 }
 

diff --git a/src/context.c b/src/context.c
index ba5b7adaa4c967bd6d2e6c6bd2db786d2d05fa38..f2d8b97bddbd6282eb49d7d1fc3b32a6940c1016 100644 (file)
--- a/src/context.c
+++ b/src/context.c
@@ -927,7 +927,7 @@ context_resetAllFlags (void)
    */
 
   /* commenting ou until some output issues are fixed */
-  /* gc.flags[FLG_ORCONSTRAINT] = TRUE;*/
+  gc.flags[FLG_ORCONSTRAINT] = TRUE; 
   
   gc.flags[FLG_CONSTRAINTLOCATION] = TRUE;
 
@@ -4911,12 +4911,15 @@ static struct sInfo globalStructInfo;
 /*drl 1/6/2001: I didn't think these functions were solid enough to include in the
   stable  release of splint.  I coomented them out so that they won't break anything
   but didn't delete them because they will be fixed and included later
+
+
 */
 
-/*
+/*@-paramuse@*/
+
 void  setGlobalStructInfo(ctype ct, constraintList list)
 {
-  int i;
+  /* int i;
   uentryList f;
 
   f =  ctype_getFields (ct);
@@ -4928,7 +4931,7 @@ void  setGlobalStructInfo(ctype ct, constraintList list)
 
       globalStructInfo.ngetUe = 0;
       
-      / *abstraction violation fix it * /
+      /* abstraction violation fix it * /
       globalStructInfo.t   = dmalloc(f->nelements * sizeof(struct getUe) );
 
       globalStructInfo.ngetUe = f->nelements;
@@ -4947,11 +4950,12 @@ void  setGlobalStructInfo(ctype ct, constraintList list)
        }
       end_uentryList_elements;
     }
+  */
 }
 
-*/
+/*
 
-bool hasInvariants (ctype ct) /*@*/
+bool hasInvariants (ctype ct) /*@* /
 {
   if ( ctype_sameName(globalStructInfo.ct, ct) )
 
@@ -4962,3 +4966,8 @@ bool hasInvariants (ctype ct) /*@*/
     return FALSE;
   
 }
+
+
+*/
+
+/*@=paramuse@*/

diff --git a/src/usymtab.c b/src/usymtab.c
index af4dbf5b9b7293b82366256db4fcc09b1bd88f90..7d4ccd1f0e166ecf26222d71d47ef69a1556a9ba 100644 (file)
--- a/src/usymtab.c
+++ b/src/usymtab.c
@@ -2009,9 +2009,9 @@ void usymtab_load (FILE *f)
     I'm trying to do this without breaking older libraries*/
   
   /*check for "optional" start buffer constraints message*/
-  if (cstring_compareLit(s, "start_Buffer_Constraints") )
+  if (cstring_compareLit(cstring_fromChars(s), "start_Buffer_Constraints\n") == 0 )
     {
-      fgets (s, MAX_DUMP_LINE_LENGTH, f);
+      (void)fgets (s, MAX_DUMP_LINE_LENGTH, f);
     }
   
   while (s != NULL && *s != ';')