From a07995d9a461db88f826d7b4061524ee413ff0e8 Mon Sep 17 00:00:00 2001 From: drl7x Date: Fri, 7 Mar 2003 07:16:11 +0000 Subject: [PATCH] Fixed bug #697722 Assert error / global I had to fish around a lot but Splint now handles thing cleanly if a global is used in a /*@requires isnull ..@*/ or similar clause. Basically, we just ignore the variable as was the old behavior. The bug was that llassert were failing. I think things likely became broken after the code implementing the overloading of the requires keyword was added. --- src/cgrammar.c.der | 116 ++++++++++++++++++++++--------------------- src/cgrammar.y | 7 ++- src/clabstract.c | 4 +- src/functionClause.c | 17 +++++-- src/stateClause.c | 18 +++++++ 5 files changed, 98 insertions(+), 64 deletions(-) diff --git a/src/cgrammar.c.der b/src/cgrammar.c.der index 382fe7e..65cd3e1 100644 --- a/src/cgrammar.c.der +++ b/src/cgrammar.c.der @@ -745,61 +745,61 @@ static const short yyrline[] = 794, 801, 806, 806, 812, 812, 812, 823, 834, 835, 839, 840, 841, 842, 843, 844, 845, 846, 847, 851, 852, 857, 858, 862, 864, 866, 867, 868, 869, 870, - 872, 877, 878, 882, 886, 899, 900, 901, 902, 903, - 904, 905, 905, 911, 912, 913, 914, 915, 916, 917, - 918, 919, 920, 925, 926, 930, 931, 932, 933, 934, - 935, 936, 937, 938, 939, 940, 944, 945, 947, 951, - 957, 957, 960, 963, 967, 968, 969, 970, 976, 977, - 982, 983, 984, 985, 989, 990, 991, 995, 996, 997, - 1001, 1002, 1003, 1004, 1005, 1009, 1010, 1011, 1015, 1016, - 1020, 1021, 1025, 1026, 1030, 1031, 1031, 1043, 1044, 1044, - 1057, 1058, 1058, 1058, 1064, 1065, 1066, 1067, 1068, 1069, - 1070, 1071, 1072, 1073, 1074, 1075, 1079, 1080, 1084, 1085, - 1089, 1095, 1096, 1097, 1101, 1115, 1115, 1126, 1126, 1135, - 1136, 1140, 1145, 1145, 1150, 1150, 1153, 1154, 1158, 1162, - 1166, 1170, 1171, 1175, 1179, 1180, 1184, 1185, 1189, 1190, - 1191, 1192, 1200, 1201, 1206, 1207, 1211, 1212, 1216, 1218, - 1228, 1229, 1230, 1231, 1232, 1236, 1240, 1240, 1256, 1260, - 1264, 1264, 1278, 1278, 1310, 1311, 1315, 1316, 1317, 1318, - 1319, 1323, 1324, 1325, 1326, 1330, 1331, 1332, 1333, 1334, - 1335, 1336, 1337, 1338, 1339, 1340, 1341, 1342, 1343, 1344, - 1345, 1346, 1350, 1351, 1355, 1356, 1360, 1361, 1365, 1366, - 1367, 1368, 1369, 1373, 1374, 1375, 1376, 1377, 1378, 1382, - 1383, 1384, 1385, 1389, 1390, 1391, 1392, 1396, 1397, 1398, - 1399, 1400, 1401, 1402, 1403, 1404, 1405, 1406, 1407, 1415, - 1416, 1417, 1418, 1419, 1420, 1421, 1422, 1423, 1424, 1425, - 1426, 1427, 1428, 1432, 1437, 1438, 1443, 1444, 1449, 1450, - 1451, 1455, 1456, 1460, 1467, 1467, 1467, 1473, 1473, 1473, - 1478, 1480, 1482, 1482, 1482, 1487, 1487, 1487, 1492, 1494, - 1496, 1497, 1501, 1505, 1506, 1507, 1511, 1513, 1518, 1520, - 1525, 1526, 1527, 1532, 1534, 1534, 1536, 1540, 1542, 1544, - 1548, 1553, 1561, 1562, 1563, 1569, 1574, 1575, 1580, 1581, - 1585, 1586, 1587, 1591, 1592, 1596, 1597, 1598, 1599, 1603, - 1604, 1608, 1609, 1613, 1614, 1615, 1619, 1619, 1620, 1620, - 1625, 1637, 1654, 1655, 1659, 1660, 1661, 1665, 1666, 1670, - 1672, 1673, 1675, 1676, 1678, 1680, 1682, 1684, 1691, 1692, - 1693, 1694, 1695, 1696, 1697, 1698, 1699, 1704, 1708, 1712, - 1713, 1718, 1720, 1722, 1724, 1729, 1729, 1729, 1737, 1737, - 1741, 1745, 1746, 1747, 1748, 1749, 1750, 1751, 1752, 1753, - 1754, 1755, 1756, 1757, 1761, 1761, 1768, 1772, 1776, 1777, - 1781, 1782, 1783, 1784, 1785, 1786, 1787, 1788, 1789, 1790, - 1791, 1795, 1796, 1804, 1805, 1812, 1812, 1814, 1814, 1819, - 1819, 1821, 1821, 1826, 1827, 1832, 1836, 1840, 1844, 1848, - 1852, 1856, 1857, 1858, 1859, 1861, 1862, 1864, 1866, 1873, - 1878, 1880, 1882, 1884, 1889, 1890, 1894, 1895, 1899, 1900, - 1904, 1905, 1909, 1910, 1914, 1915, 1919, 1920, 1921, 1925, - 1939, 1944, 1944, 1949, 1949, 1954, 1960, 1964, 1964, 1964, - 1975, 1976, 1976, 1981, 1982, 1983, 1994, 2002, 2003, 2007, - 2008, 2012, 2013, 2014, 2015, 2016, 2018, 2019, 2020, 2021, - 2025, 2026, 2027, 2028, 2029, 2030, 2031, 2032, 2033, 2034, - 2038, 2039, 2043, 2044, 2045, 2046, 2050, 2051, 2052, 2056, - 2057, 2058, 2062, 2063, 2064, 2065, 2066, 2070, 2071, 2072, - 2076, 2077, 2081, 2082, 2086, 2087, 2091, 2092, 2096, 2097, - 2101, 2102, 2102, 2102, 2108, 2109, 2110, 2111, 2112, 2113, - 2114, 2115, 2116, 2117, 2118, 2119, 2123, 2124, 2128, 2132, - 2134, 2136, 2141, 2142, 2144, 2146, 2150, 2151, 2152, 2154, - 2155, 2156, 2157, 2158, 2159, 2160, 2164, 2165, 2169, 2170, - 2174, 2178, 2179, 2180, 2181, 2182, 2186, 2187, 2188, 2189 + 872, 877, 878, 882, 888, 901, 902, 903, 904, 905, + 906, 907, 907, 913, 914, 915, 916, 917, 918, 919, + 920, 921, 922, 927, 928, 932, 933, 934, 935, 936, + 937, 938, 939, 940, 941, 942, 946, 947, 949, 953, + 959, 959, 962, 965, 969, 970, 971, 972, 978, 979, + 984, 985, 986, 987, 991, 992, 993, 997, 998, 999, + 1003, 1004, 1005, 1006, 1007, 1011, 1012, 1013, 1017, 1018, + 1022, 1023, 1027, 1028, 1032, 1033, 1033, 1045, 1046, 1046, + 1059, 1060, 1060, 1060, 1066, 1067, 1068, 1069, 1070, 1071, + 1072, 1073, 1074, 1075, 1076, 1077, 1081, 1082, 1086, 1087, + 1091, 1097, 1098, 1099, 1103, 1117, 1117, 1128, 1128, 1137, + 1138, 1142, 1147, 1147, 1152, 1152, 1155, 1156, 1160, 1164, + 1168, 1172, 1173, 1177, 1181, 1182, 1186, 1187, 1191, 1192, + 1193, 1194, 1202, 1203, 1208, 1209, 1213, 1214, 1218, 1220, + 1230, 1231, 1232, 1233, 1234, 1238, 1242, 1242, 1258, 1262, + 1266, 1266, 1280, 1280, 1312, 1313, 1317, 1318, 1319, 1320, + 1321, 1325, 1326, 1327, 1328, 1332, 1333, 1334, 1335, 1336, + 1337, 1338, 1339, 1340, 1341, 1342, 1343, 1344, 1345, 1346, + 1347, 1348, 1352, 1353, 1357, 1358, 1362, 1363, 1367, 1368, + 1369, 1370, 1371, 1375, 1376, 1377, 1378, 1379, 1380, 1384, + 1385, 1386, 1387, 1391, 1392, 1393, 1394, 1398, 1399, 1400, + 1401, 1402, 1403, 1404, 1405, 1406, 1407, 1408, 1409, 1417, + 1418, 1419, 1420, 1421, 1422, 1423, 1424, 1425, 1426, 1427, + 1428, 1429, 1430, 1434, 1439, 1440, 1445, 1446, 1451, 1452, + 1453, 1457, 1458, 1462, 1469, 1469, 1469, 1475, 1475, 1475, + 1480, 1482, 1484, 1484, 1484, 1489, 1489, 1489, 1494, 1496, + 1498, 1499, 1503, 1507, 1508, 1509, 1513, 1515, 1520, 1522, + 1527, 1528, 1529, 1534, 1536, 1536, 1538, 1542, 1544, 1546, + 1550, 1555, 1563, 1564, 1565, 1571, 1576, 1577, 1582, 1583, + 1587, 1588, 1589, 1593, 1594, 1598, 1599, 1600, 1601, 1605, + 1606, 1610, 1611, 1615, 1616, 1617, 1621, 1621, 1622, 1622, + 1627, 1639, 1656, 1657, 1661, 1662, 1663, 1667, 1668, 1672, + 1674, 1675, 1677, 1678, 1680, 1682, 1684, 1686, 1693, 1694, + 1695, 1696, 1697, 1698, 1699, 1700, 1701, 1706, 1710, 1714, + 1715, 1720, 1722, 1724, 1726, 1731, 1731, 1731, 1739, 1739, + 1743, 1747, 1748, 1749, 1750, 1751, 1752, 1753, 1754, 1755, + 1756, 1757, 1758, 1759, 1763, 1763, 1770, 1774, 1778, 1779, + 1783, 1784, 1785, 1786, 1787, 1788, 1789, 1790, 1791, 1792, + 1793, 1797, 1798, 1806, 1807, 1814, 1814, 1816, 1816, 1821, + 1821, 1823, 1823, 1828, 1829, 1834, 1838, 1842, 1846, 1850, + 1854, 1858, 1859, 1860, 1861, 1863, 1864, 1866, 1868, 1875, + 1880, 1882, 1884, 1886, 1891, 1892, 1896, 1897, 1901, 1902, + 1906, 1907, 1911, 1912, 1916, 1917, 1921, 1922, 1923, 1927, + 1941, 1946, 1946, 1951, 1951, 1956, 1962, 1966, 1966, 1966, + 1977, 1978, 1978, 1983, 1984, 1985, 1996, 2004, 2005, 2009, + 2010, 2014, 2015, 2016, 2017, 2018, 2020, 2021, 2022, 2023, + 2027, 2028, 2029, 2030, 2031, 2032, 2033, 2034, 2035, 2036, + 2040, 2041, 2045, 2046, 2047, 2048, 2052, 2053, 2054, 2058, + 2059, 2060, 2064, 2065, 2066, 2067, 2068, 2072, 2073, 2074, + 2078, 2079, 2083, 2084, 2088, 2089, 2093, 2094, 2098, 2099, + 2103, 2104, 2104, 2104, 2110, 2111, 2112, 2113, 2114, 2115, + 2116, 2117, 2118, 2119, 2120, 2121, 2125, 2126, 2130, 2134, + 2136, 2138, 2143, 2144, 2146, 2148, 2152, 2153, 2154, 2156, + 2157, 2158, 2159, 2160, 2161, 2162, 2166, 2167, 2171, 2172, + 2176, 2180, 2181, 2182, 2183, 2184, 2188, 2189, 2190, 2191 }; #endif @@ -4052,11 +4052,13 @@ case 160: yyval.sr = sRef_makeArrow (yyvsp[-2].sr, yyvsp[0].cname); ; break;} case 161: -{ yyval.srset = sRefSet_undefined ; +{ DPRINTF ((message("Empty optSpecClauseList") )); yyval.srset = sRefSet_undefined ; break;} case 163: { if (sRef_isValid (yyvsp[0].sr)) { yyval.srset = sRefSet_single (yyvsp[0].sr); } - else { yyval.srset = sRefSet_undefined; } + else { + DPRINTF((message("returning sRefSEt_undefined ") )); + yyval.srset = sRefSet_undefined; } ; break;} case 164: diff --git a/src/cgrammar.y b/src/cgrammar.y index cbd9e15..e91de36 100644 --- a/src/cgrammar.y +++ b/src/cgrammar.y @@ -874,14 +874,16 @@ specClauseListExpr ; optSpecClauseList - : /* empty */ { $$ = sRefSet_undefined } + : /* empty */ { DPRINTF ((message("Empty optSpecClauseList") )); $$ = sRefSet_undefined } | specClauseList ; specClauseList : specClauseListExpr { if (sRef_isValid ($1)) { $$ = sRefSet_single ($1); } - else { $$ = sRefSet_undefined; } + else { + DPRINTF((message("returning sRefSEt_undefined ") )); + $$ = sRefSet_undefined; } } | specClauseList TCOMMA specClauseListExpr { if (sRef_isValid ($3)) @@ -956,6 +958,7 @@ offsetofExpr sizeofExpr : IsType { context_setProtectVars (); } sizeofExprAux { context_sizeofReleaseVars (); $$ = $3; } +; processSizeof: {context_enterSizeof()}; diff --git a/src/clabstract.c b/src/clabstract.c index da24ba0..1131f59 100644 --- a/src/clabstract.c +++ b/src/clabstract.c @@ -2163,7 +2163,9 @@ sRef checkStateClausesId (uentry ue) voptgenerror (FLG_COMMENTERROR, message ("Global variable %s used state clause. (Global variables " - "are not recognized in state clauses. If there is " + "are not recognized in state clauses. If they are present " + "they are ignored. " + " If there is " "sufficient interest in support for this, it may be " "added to a future release. Send mail to " "info@splint.org.)", diff --git a/src/functionClause.c b/src/functionClause.c index c741a99..f63810c 100644 --- a/src/functionClause.c +++ b/src/functionClause.c @@ -52,10 +52,19 @@ extern functionClause functionClause_createModifies (modifiesClause node) /*@*/ } extern functionClause functionClause_createState (stateClause node) /*@*/ -{ - functionClause res = functionClause_alloc (FCK_STATE); - res->val.state = node; - return res; +{ + if (stateClause_hasEmptyReferences (node) && + (!stateClause_isMetaState (node) ) ) + { + DPRINTF((message("functionClause_createState:: Returning functionClause_undefined" ) )); + return functionClause_undefined; + } + else + { + functionClause res = functionClause_alloc (FCK_STATE); + res->val.state = node; + return res; + } } extern functionClause functionClause_createEnsures (functionConstraint node) /*@*/ diff --git a/src/stateClause.c b/src/stateClause.c index 26009b4..5b7fbce 100644 --- a/src/stateClause.c +++ b/src/stateClause.c @@ -43,6 +43,24 @@ stateClause_createRaw (stateConstraint st, stateClauseKind sk, /*@only@*/ sRefSe return ret; } +/*drl added 3/7/2003*/ +bool stateClause_hasEmptyReferences (stateClause s) +{ + if (sRefSet_isUndefined(s->refs) ) + return TRUE; + else + return FALSE; +} + +bool stateClause_isMetaState (stateClause s) +{ + + if (qual_isMetaState (s->squal) ) + return TRUE; + else + return FALSE; +} + stateClause stateClause_create (lltok tok, qual q, sRefSet s) { -- 2.45.1