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.

diff --git a/src/cgrammar.c.der b/src/cgrammar.c.der
index 382fe7ef27906306f536653cf03110485015deef..65cd3e15187f5b74d48a90389500e3f3d00c67ad 100644 (file)
--- 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 cbd9e15c62c87b64c015cc839dade28c68d70194..e91de36edfd60b44f0966d3a1b504ead550c68e5 100644 (file)
--- 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 da24ba0e951a0ae9074b36240d25d68b642503e6..1131f590095f1c4545310cedbe8a8d91dead79d3 100644 (file)
--- 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 c741a99aebce38f301c457590659e4a4f607c45c..f63810ce9206a18430392b43e7ddab151820b658 100644 (file)
--- 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 26009b4059918f8a28d9feb9993e057d4d7e2e33..5b7fbce3c6f9eb496fe2afbeccbbf9ea34ac59bf 100644 (file)
--- 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) 
 {