From: drl7x Date: Thu, 5 Sep 2002 16:33:20 +0000 (+0000) Subject: Fixed bug cause spurious bounds errors. X-Git-Tag: splint-3_1_0~98 X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/commitdiff_plain/d9daf826a5062af3f227a98f0525e5a38f350539 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 3beeb1d..38450a1 100644 --- 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 d299af7..70349f6 100644 --- 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 4be8618..8d84bff 100644 --- 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 4a08b45..da66257 100644 --- 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 cb87d10..71c3855 100644 --- 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 9cbc788..6f795b3 100644 --- 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 ba5b7ad..f2d8b97 100644 --- 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 af4dbf5..7d4ccd1 100644 --- 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 != ';')