From 4287634ef9d99c9ab7476b2937c35fabc299aca8 Mon Sep 17 00:00:00 2001 From: drl7x Date: Wed, 18 Dec 2002 23:54:36 +0000 Subject: [PATCH] Added support for default buffer constraint annotations and merged with previously committed code. --- src/Headers/functionConstraint.h | 4 +- src/Makefile.am | 15 ++- src/Makefile.in | 30 ++++-- src/cgrammar.c.der | 174 ++++++++++++++++++------------- src/cgrammar.y | 36 ++++++- src/clabstract.c | 58 +++++++---- src/constraintGeneration.c | 21 ++-- src/functionClauseList.c | 44 +++++++- src/functionConstraint.c | 35 ++++++- src/idDecl.c | 11 +- test/Makefile.in | 15 +-- 11 files changed, 309 insertions(+), 134 deletions(-) diff --git a/src/Headers/functionConstraint.h b/src/Headers/functionConstraint.h index 546e102..5d6b72a 100644 --- a/src/Headers/functionConstraint.h +++ b/src/Headers/functionConstraint.h @@ -32,8 +32,8 @@ extern /*@falsewhennull@*/ bool functionConstraint_isDefined (functionConstraint extern /*@falsewhennull@*/ bool functionConstraint_isBufferConstraint (/*@sef@*/ functionConstraint) /*@*/ ; # define functionConstraint_isBufferConstraint(p_con) (((p_con) != NULL) && ((p_con)->kind == FCT_BUFFER)) -extern void functionConstraint_addBufferConstraints (functionConstraint p_fc, /*@only@*/ constraintList) - /*@modifies p_fc@*/ ; +extern void functionConstraint_addBufferConstraints (functionConstraint p_node, /*@only@*/ constraintList) + /*@modifies p_node@*/ ; extern /*@nullwhentrue@*/ bool functionConstraint_isUndefined (functionConstraint) /*@*/ ; # define functionConstraint_isUndefined(p_info) ((p_info) == NULL) diff --git a/src/Makefile.am b/src/Makefile.am index 0dadfc1..4685875 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -282,6 +282,19 @@ BUILT_SOURCES = Headers/signature_gen.h Headers/cgrammar_tokens.h \ ## Grammars +signature.c.der: + @if test x$(BISON) = xno; then \ + echo "Cannot make signature.c.der because bison is not here" \ + else \ + echo '* Making signature.c'; \ + $(BISON) $(YFLAGS) -p lsl signature.y; \ + $(CAT) bison.head signature.tab.c bison.reset >signature.c; \ + $(CP) signature.c signature.c.der; \ + $(MV) Headers/signature_gen.h Headers/signature_gen.bak || true; \ + $(CAT) bison.head signature.tab.h bison.reset >Headers/signature_gen.h; \ + $(RM) signature.tab.c signature.tab.h; \ + fi + Headers/signature_gen.h signature.c: signature.c.der signature.y @if test x$(BISON) = xno; then \ $(CP) signature.c.der signature.c; \ @@ -307,7 +320,7 @@ Headers/cgrammar_tokens.h cgrammar.c: cgrammar.c.der cgrammar.y bison.head bison $(BISON) $(YFLAGS) cgrammar.y; \ $(CAT) bison.head cgrammar.tab.c bison.reset | $(SED) 's/YYSTYPE/cgrammar_YYSTYPE/g' | $(SED) 's/lsllex/cgrammar_lsllex/g' > cgrammar.c; \ $(CP) cgrammar.c cgrammar.c.der; \ - $(MV) Headers/cgrammar_tokens.h Headers/cgrammar_tokens.bak; \ + $(MV) Headers/cgrammar_tokens.h Headers/cgrammar_tokens.bak || true; \ $(CAT) bison.head cgrammar.tab.h bison.reset | $(SED) 's/YYSTYPE/cgrammar_YYSTYPE/g' | $(SED) 's/lsllex/cgrammar_lsllex/g' > Headers/cgrammar_tokens.h; \ $(RM) cgrammar.tab.c cgrammar.tab.h; \ fi diff --git a/src/Makefile.in b/src/Makefile.in index e889b90..c7f03df 100644 --- a/src/Makefile.in +++ b/src/Makefile.in @@ -132,7 +132,7 @@ CSRC = context.c uentry.c cprim.c macrocache.c qual.c qtype.c stateClause.c \ globalsClause.c modifiesClause.c warnClause.c functionClause.c \ functionClauseList.c metaStateConstraint.c metaStateConstraintList.c \ metaStateExpression.c metaStateSpecifier.c functionConstraint.c \ - pointers.c cscannerHelp.c + pointers.c cscannerHelp.c SPLINTSRC = exprNode.c exprChecks.c llmain.c help.c rcfiles.c @@ -350,8 +350,8 @@ ALLSRC = $(GRAMSRC) $(COMMONSRC) $(SPLINTSRC) $(OVERFLOWCHSRC) $(DER_FILES) $(HE #files to run Splint on LINTSRC = $(COMMONSRC) $(SPLINTSRC) -## cscanner.c cgrammar.c +# cscanner.c cgrammar.c #ALLSRC = $(COMMONSRC) $(SPLINTSRC) $(DER_FILES) $(HEADERSRC) LCLSRC = $(LCLSETSRC) $(LCLLISTSRC) $(LSLSRC) $(CMNSRC) $(LCLONLYSRC) @@ -427,7 +427,8 @@ am__objects_9 = context.$(OBJEXT) uentry.$(OBJEXT) cprim.$(OBJEXT) \ functionClause.$(OBJEXT) functionClauseList.$(OBJEXT) \ metaStateConstraint.$(OBJEXT) metaStateConstraintList.$(OBJEXT) \ metaStateExpression.$(OBJEXT) metaStateSpecifier.$(OBJEXT) \ - functionConstraint.$(OBJEXT) pointers.$(OBJEXT) + functionConstraint.$(OBJEXT) pointers.$(OBJEXT) \ + cscannerHelp.$(OBJEXT) am__objects_10 = structNames.$(OBJEXT) transferChecks.$(OBJEXT) \ varKinds.$(OBJEXT) nameChecks.$(OBJEXT) am__objects_11 = exprData.$(OBJEXT) cstring.$(OBJEXT) fileloc.$(OBJEXT) \ @@ -509,7 +510,8 @@ am__depfiles_maybe = depfiles @AMDEP_TRUE@ ./$(DEPDIR)/cppexp.Po ./$(DEPDIR)/cpphash.Po \ @AMDEP_TRUE@ ./$(DEPDIR)/cpplib.Po ./$(DEPDIR)/cppmain.Po \ @AMDEP_TRUE@ ./$(DEPDIR)/cprim.Po ./$(DEPDIR)/cscanner.Po \ -@AMDEP_TRUE@ ./$(DEPDIR)/cstring.Po ./$(DEPDIR)/cstringList.Po \ +@AMDEP_TRUE@ ./$(DEPDIR)/cscannerHelp.Po ./$(DEPDIR)/cstring.Po \ +@AMDEP_TRUE@ ./$(DEPDIR)/cstringList.Po \ @AMDEP_TRUE@ ./$(DEPDIR)/cstringSList.Po \ @AMDEP_TRUE@ ./$(DEPDIR)/cstringTable.Po ./$(DEPDIR)/ctype.Po \ @AMDEP_TRUE@ ./$(DEPDIR)/ctypeList.Po ./$(DEPDIR)/cvar.Po \ @@ -701,6 +703,7 @@ distclean-compile: @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/cppmain.Po@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/cprim.Po@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/cscanner.Po@am__quote@ +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/cscannerHelp.Po@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/cstring.Po@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/cstringList.Po@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/cstringSList.Po@am__quote@ @@ -1023,6 +1026,19 @@ lcl$(EXEEXT): @echo "This is a fake target"; \ echo "Use configure's --with-lcl option to enable lcl" +signature.c.der: + @if test x$(BISON) = xno; then \ + echo "Cannot make signature.c.der because bison is not here" \ + else \ + echo '* Making signature.c'; \ + $(BISON) $(YFLAGS) -p lsl signature.y; \ + $(CAT) bison.head signature.tab.c bison.reset >signature.c; \ + $(CP) signature.c signature.c.der; \ + $(MV) Headers/signature_gen.h Headers/signature_gen.bak || true; \ + $(CAT) bison.head signature.tab.h bison.reset >Headers/signature_gen.h; \ + $(RM) signature.tab.c signature.tab.h; \ + fi + Headers/signature_gen.h signature.c: signature.c.der signature.y @if test x$(BISON) = xno; then \ $(CP) signature.c.der signature.c; \ @@ -1041,12 +1057,12 @@ Headers/cgrammar_tokens.h cgrammar.c: cgrammar.c.der cgrammar.y bison.head bison $(CP) cgrammar.c.der cgrammar.c; \ else \ echo '* Making cgrammar.c'; \ - echo '* Expect 154 shift/reduce conflicts and 116 reduce/reduce conflicts.'; \ + echo '* Expect 157 shift/reduce conflicts and 117 reduce/reduce conflicts.'; \ echo '* (see cgrammar.y for explanation)'; \ $(BISON) $(YFLAGS) cgrammar.y; \ $(CAT) bison.head cgrammar.tab.c bison.reset | $(SED) 's/YYSTYPE/cgrammar_YYSTYPE/g' | $(SED) 's/lsllex/cgrammar_lsllex/g' > cgrammar.c; \ $(CP) cgrammar.c cgrammar.c.der; \ - $(MV) Headers/cgrammar_tokens.h Headers/cgrammar_tokens.bak; \ + $(MV) Headers/cgrammar_tokens.h Headers/cgrammar_tokens.bak || true; \ $(CAT) bison.head cgrammar.tab.h bison.reset | $(SED) 's/YYSTYPE/cgrammar_YYSTYPE/g' | $(SED) 's/lsllex/cgrammar_lsllex/g' > Headers/cgrammar_tokens.h; \ $(RM) cgrammar.tab.c cgrammar.tab.h; \ fi @@ -1106,7 +1122,7 @@ etags: lintnew: splintme splintme: - ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude cscannerHelp.c $(LINTSRC) $(OVERFLOWCHSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw + ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(LINTSRC) $(OVERFLOWCHSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw valsplint: valgrind -v --leak-resolution=high --num-callers=20 --show-reachable=no --leak-check=yes ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(LINTSRC) $(OVERFLOWCHSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw diff --git a/src/cgrammar.c.der b/src/cgrammar.c.der index 8c3a3e2..c79a2ee 100644 --- a/src/cgrammar.c.der +++ b/src/cgrammar.c.der @@ -731,75 +731,75 @@ static const short yyrline[] = { 0, 325, 326, 330, 331, 335, 336, 337, 338, 339, 340, 341, 342, 346, 348, 353, 353, 362, 368, 373, - 374, 379, 380, 382, 384, 401, 401, 419, 419, 434, - 435, 437, 441, 458, 458, 470, 470, 484, 484, 484, - 493, 494, 495, 496, 500, 504, 509, 509, 514, 514, - 522, 523, 527, 533, 534, 538, 539, 543, 549, 550, - 554, 555, 556, 560, 561, 562, 568, 569, 573, 575, - 577, 579, 588, 590, 592, 594, 611, 615, 616, 623, - 624, 633, 635, 640, 641, 642, 643, 644, 645, 649, - 650, 651, 652, 653, 654, 658, 662, 662, 671, 675, - 679, 679, 694, 696, 701, 705, 706, 710, 714, 720, - 725, 726, 730, 734, 735, 739, 740, 741, 745, 746, - 747, 748, 749, 753, 754, 755, 756, 757, 761, 762, - 766, 773, 778, 778, 784, 784, 784, 795, 806, 807, - 811, 812, 813, 814, 815, 816, 817, 818, 819, 823, - 824, 829, 830, 834, 836, 838, 839, 840, 841, 842, - 844, 849, 850, 854, 858, 871, 872, 873, 874, 875, - 876, 877, 877, 883, 884, 885, 886, 887, 888, 889, - 890, 891, 892, 897, 898, 902, 903, 904, 905, 906, - 907, 908, 909, 910, 911, 912, 916, 917, 919, 923, - 929, 929, 934, 935, 936, 937, 941, 942, 947, 948, - 949, 950, 954, 955, 956, 960, 961, 962, 966, 967, - 968, 969, 970, 974, 975, 976, 980, 981, 985, 986, - 990, 991, 995, 996, 996, 1008, 1009, 1009, 1022, 1023, - 1023, 1023, 1029, 1030, 1031, 1032, 1033, 1034, 1035, 1036, - 1037, 1038, 1039, 1040, 1044, 1045, 1049, 1050, 1054, 1060, - 1061, 1062, 1066, 1080, 1080, 1091, 1091, 1100, 1101, 1105, - 1110, 1110, 1115, 1115, 1118, 1119, 1123, 1127, 1131, 1135, - 1136, 1140, 1144, 1145, 1149, 1150, 1154, 1155, 1156, 1157, - 1165, 1166, 1171, 1172, 1176, 1177, 1181, 1183, 1193, 1194, - 1195, 1196, 1197, 1201, 1205, 1205, 1221, 1225, 1229, 1229, - 1243, 1243, 1275, 1276, 1280, 1281, 1282, 1283, 1284, 1288, - 1289, 1290, 1291, 1295, 1296, 1297, 1298, 1299, 1300, 1301, - 1302, 1303, 1304, 1305, 1306, 1307, 1308, 1309, 1310, 1311, - 1315, 1316, 1320, 1321, 1325, 1326, 1330, 1331, 1332, 1333, - 1334, 1338, 1339, 1340, 1341, 1342, 1343, 1347, 1348, 1349, - 1350, 1354, 1355, 1356, 1357, 1361, 1362, 1363, 1364, 1365, - 1366, 1367, 1368, 1369, 1370, 1371, 1372, 1380, 1381, 1382, - 1383, 1384, 1385, 1386, 1387, 1388, 1389, 1390, 1391, 1392, - 1393, 1397, 1402, 1403, 1408, 1409, 1414, 1415, 1416, 1420, - 1421, 1425, 1432, 1432, 1432, 1438, 1438, 1438, 1443, 1445, - 1447, 1447, 1447, 1452, 1452, 1452, 1457, 1459, 1461, 1462, - 1466, 1470, 1471, 1472, 1476, 1478, 1483, 1485, 1490, 1491, - 1492, 1497, 1499, 1499, 1501, 1505, 1507, 1509, 1513, 1518, - 1526, 1527, 1528, 1534, 1539, 1540, 1545, 1546, 1550, 1551, - 1552, 1556, 1557, 1561, 1562, 1563, 1564, 1568, 1569, 1573, - 1574, 1578, 1579, 1580, 1584, 1584, 1585, 1585, 1590, 1602, - 1619, 1620, 1624, 1625, 1626, 1630, 1631, 1635, 1637, 1638, - 1640, 1641, 1643, 1645, 1647, 1649, 1656, 1657, 1658, 1659, - 1660, 1661, 1662, 1663, 1664, 1669, 1673, 1677, 1678, 1683, - 1685, 1687, 1689, 1694, 1694, 1694, 1702, 1702, 1706, 1710, - 1711, 1712, 1713, 1714, 1715, 1716, 1717, 1718, 1719, 1720, - 1721, 1722, 1726, 1726, 1733, 1737, 1741, 1742, 1746, 1747, - 1748, 1749, 1750, 1751, 1752, 1753, 1754, 1755, 1756, 1760, - 1761, 1769, 1770, 1777, 1777, 1779, 1779, 1784, 1784, 1786, - 1786, 1791, 1792, 1797, 1801, 1805, 1809, 1813, 1817, 1821, - 1822, 1823, 1824, 1826, 1827, 1829, 1831, 1838, 1843, 1845, - 1847, 1849, 1854, 1855, 1859, 1860, 1864, 1865, 1869, 1870, - 1874, 1875, 1879, 1880, 1884, 1885, 1886, 1890, 1904, 1909, - 1909, 1914, 1914, 1919, 1925, 1929, 1929, 1929, 1940, 1941, - 1941, 1946, 1947, 1948, 1959, 1967, 1968, 1972, 1973, 1977, - 1978, 1979, 1980, 1981, 1983, 1984, 1985, 1986, 1990, 1991, - 1992, 1993, 1994, 1995, 1996, 1997, 1998, 1999, 2003, 2004, - 2008, 2009, 2010, 2011, 2015, 2016, 2017, 2021, 2022, 2023, - 2027, 2028, 2029, 2030, 2031, 2035, 2036, 2037, 2041, 2042, - 2046, 2047, 2051, 2052, 2056, 2057, 2061, 2062, 2066, 2067, - 2067, 2067, 2073, 2074, 2075, 2076, 2077, 2078, 2079, 2080, - 2081, 2082, 2083, 2084, 2088, 2089, 2093, 2097, 2099, 2101, - 2106, 2107, 2109, 2111, 2115, 2116, 2117, 2119, 2120, 2121, - 2122, 2123, 2124, 2125, 2129, 2130, 2134, 2135, 2139, 2143, - 2144, 2145, 2146, 2147, 2151, 2152, 2153, 2154 + 374, 379, 380, 382, 384, 401, 401, 432, 432, 462, + 463, 465, 469, 486, 486, 498, 498, 512, 512, 512, + 521, 522, 523, 524, 528, 532, 537, 537, 542, 542, + 550, 551, 555, 561, 562, 566, 567, 571, 577, 578, + 582, 583, 584, 588, 589, 590, 596, 597, 601, 603, + 605, 607, 616, 618, 620, 622, 639, 643, 644, 651, + 652, 661, 663, 668, 669, 670, 671, 672, 673, 677, + 678, 679, 680, 681, 682, 686, 690, 690, 699, 703, + 707, 707, 722, 724, 729, 733, 734, 738, 742, 748, + 753, 754, 758, 762, 763, 767, 768, 769, 773, 774, + 775, 776, 777, 781, 782, 783, 784, 785, 789, 790, + 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, 962, 963, 964, 965, 969, 970, 975, 976, + 977, 978, 982, 983, 984, 988, 989, 990, 994, 995, + 996, 997, 998, 1002, 1003, 1004, 1008, 1009, 1013, 1014, + 1018, 1019, 1023, 1024, 1024, 1036, 1037, 1037, 1050, 1051, + 1051, 1051, 1057, 1058, 1059, 1060, 1061, 1062, 1063, 1064, + 1065, 1066, 1067, 1068, 1072, 1073, 1077, 1078, 1082, 1088, + 1089, 1090, 1094, 1108, 1108, 1119, 1119, 1128, 1129, 1133, + 1138, 1138, 1143, 1143, 1146, 1147, 1151, 1155, 1159, 1163, + 1164, 1168, 1172, 1173, 1177, 1178, 1182, 1183, 1184, 1185, + 1193, 1194, 1199, 1200, 1204, 1205, 1209, 1211, 1221, 1222, + 1223, 1224, 1225, 1229, 1233, 1233, 1249, 1253, 1257, 1257, + 1271, 1271, 1303, 1304, 1308, 1309, 1310, 1311, 1312, 1316, + 1317, 1318, 1319, 1323, 1324, 1325, 1326, 1327, 1328, 1329, + 1330, 1331, 1332, 1333, 1334, 1335, 1336, 1337, 1338, 1339, + 1343, 1344, 1348, 1349, 1353, 1354, 1358, 1359, 1360, 1361, + 1362, 1366, 1367, 1368, 1369, 1370, 1371, 1375, 1376, 1377, + 1378, 1382, 1383, 1384, 1385, 1389, 1390, 1391, 1392, 1393, + 1394, 1395, 1396, 1397, 1398, 1399, 1400, 1408, 1409, 1410, + 1411, 1412, 1413, 1414, 1415, 1416, 1417, 1418, 1419, 1420, + 1421, 1425, 1430, 1431, 1436, 1437, 1442, 1443, 1444, 1448, + 1449, 1453, 1460, 1460, 1460, 1466, 1466, 1466, 1471, 1473, + 1475, 1475, 1475, 1480, 1480, 1480, 1485, 1487, 1489, 1490, + 1494, 1498, 1499, 1500, 1504, 1506, 1511, 1513, 1518, 1519, + 1520, 1525, 1527, 1527, 1529, 1533, 1535, 1537, 1541, 1546, + 1554, 1555, 1556, 1562, 1567, 1568, 1573, 1574, 1578, 1579, + 1580, 1584, 1585, 1589, 1590, 1591, 1592, 1596, 1597, 1601, + 1602, 1606, 1607, 1608, 1612, 1612, 1613, 1613, 1618, 1630, + 1647, 1648, 1652, 1653, 1654, 1658, 1659, 1663, 1665, 1666, + 1668, 1669, 1671, 1673, 1675, 1677, 1684, 1685, 1686, 1687, + 1688, 1689, 1690, 1691, 1692, 1697, 1701, 1705, 1706, 1711, + 1713, 1715, 1717, 1722, 1722, 1722, 1730, 1730, 1734, 1738, + 1739, 1740, 1741, 1742, 1743, 1744, 1745, 1746, 1747, 1748, + 1749, 1750, 1754, 1754, 1761, 1765, 1769, 1770, 1774, 1775, + 1776, 1777, 1778, 1779, 1780, 1781, 1782, 1783, 1784, 1788, + 1789, 1797, 1798, 1805, 1805, 1807, 1807, 1812, 1812, 1814, + 1814, 1819, 1820, 1825, 1829, 1833, 1837, 1841, 1845, 1849, + 1850, 1851, 1852, 1854, 1855, 1857, 1859, 1866, 1871, 1873, + 1875, 1877, 1882, 1883, 1887, 1888, 1892, 1893, 1897, 1898, + 1902, 1903, 1907, 1908, 1912, 1913, 1914, 1918, 1932, 1937, + 1937, 1942, 1942, 1947, 1953, 1957, 1957, 1957, 1968, 1969, + 1969, 1974, 1975, 1976, 1987, 1995, 1996, 2000, 2001, 2005, + 2006, 2007, 2008, 2009, 2011, 2012, 2013, 2014, 2018, 2019, + 2020, 2021, 2022, 2023, 2024, 2025, 2026, 2027, 2031, 2032, + 2036, 2037, 2038, 2039, 2043, 2044, 2045, 2049, 2050, 2051, + 2055, 2056, 2057, 2058, 2059, 2063, 2064, 2065, 2069, 2070, + 2074, 2075, 2079, 2080, 2084, 2085, 2089, 2090, 2094, 2095, + 2095, 2095, 2101, 2102, 2103, 2104, 2105, 2106, 2107, 2108, + 2109, 2110, 2111, 2112, 2116, 2117, 2121, 2125, 2127, 2129, + 2134, 2135, 2137, 2139, 2143, 2144, 2145, 2147, 2148, 2149, + 2150, 2151, 2152, 2153, 2157, 2158, 2162, 2163, 2167, 2171, + 2172, 2173, 2174, 2175, 2179, 2180, 2181, 2182 }; #endif @@ -3584,6 +3584,7 @@ case 25: break;} case 26: { /* need to support globals and modifies here! */ + functionClauseList fcl; ctype ct = ctype_makeFunction (idDecl_getCtype (yyvsp[-5].ntyp), uentryList_makeMissingParams ()); @@ -3592,9 +3593,21 @@ case 26: /*drl 7/25/01 added*/ setImplictfcnConstraints(); - /* functionClauseList_ImplictConstraints($6); */ + DPRINTF((message("namedDeclBase PushType TLPAREN TRPAREN...:\n adding implict constraints to functionClause List: %s", + functionClauseList_unparse(yyvsp[0].funcclauselist) + ) + )); + + fcl = functionClauseList_setImplictConstraints(yyvsp[0].funcclauselist); - idDecl_addClauses (yyval.ntyp, yyvsp[0].funcclauselist); + idDecl_addClauses (yyval.ntyp, fcl); + + DPRINTF((message("1 added fuctionClause List: %s to the Id", + functionClauseList_unparse(fcl) + ) + )); + + context_popLoc (); lltok_free2 (yyvsp[-3].tok, yyvsp[-2].tok); ; @@ -3604,11 +3617,26 @@ case 27: break;} case 28: { + functionClauseList fcl; setImplictfcnConstraints (); - /* functionClauseList_ImplictConstraints($7);*/ clearCurrentParams (); yyval.ntyp = idDecl_replaceCtype (yyvsp[-6].ntyp, ctype_makeFunction (idDecl_getCtype (yyvsp[-6].ntyp), yyvsp[-3].entrylist)); - idDecl_addClauses (yyval.ntyp, yyvsp[0].funcclauselist); + + DPRINTF((message("namedDeclBase PushType TLPAREN genericParamList TRPAREN...:\n adding implict constraints to functionClause List: %s", + functionClauseList_unparse(yyvsp[0].funcclauselist) + ) + )) ; + + fcl = functionClauseList_setImplictConstraints(yyvsp[0].funcclauselist); + + idDecl_addClauses (yyval.ntyp, fcl); + + DPRINTF((message("added fuctionClause List: %s to the Id", + functionClauseList_unparse(fcl) + ) + )); + + context_popLoc (); lltok_free2 (yyvsp[-4].tok, yyvsp[-2].tok); ; diff --git a/src/cgrammar.y b/src/cgrammar.y index 3134c11..7294805 100644 --- a/src/cgrammar.y +++ b/src/cgrammar.y @@ -402,6 +402,7 @@ namedDeclBase { setCurrentParams (uentryList_missingParams); } functionClauses { /* need to support globals and modifies here! */ + functionClauseList fcl; ctype ct = ctype_makeFunction (idDecl_getCtype ($1), uentryList_makeMissingParams ()); @@ -410,9 +411,21 @@ namedDeclBase /*drl 7/25/01 added*/ setImplictfcnConstraints(); - /* functionClauseList_ImplictConstraints($6); */ + DPRINTF((message("namedDeclBase PushType TLPAREN TRPAREN...:\n adding implict constraints to functionClause List: %s", + functionClauseList_unparse($6) + ) + )); + + fcl = functionClauseList_setImplictConstraints($6); - idDecl_addClauses ($$, $6); + idDecl_addClauses ($$, fcl); + + DPRINTF((message("1 added fuctionClause List: %s to the Id", + functionClauseList_unparse(fcl) + ) + )); + + context_popLoc (); lltok_free2 ($3, $4); } @@ -420,11 +433,26 @@ namedDeclBase { setCurrentParams ($4); } functionClauses { + functionClauseList fcl; setImplictfcnConstraints (); - /* functionClauseList_ImplictConstraints($7);*/ clearCurrentParams (); $$ = idDecl_replaceCtype ($1, ctype_makeFunction (idDecl_getCtype ($1), $4)); - idDecl_addClauses ($$, $7); + + DPRINTF((message("namedDeclBase PushType TLPAREN genericParamList TRPAREN...:\n adding implict constraints to functionClause List: %s", + functionClauseList_unparse($7) + ) + )) ; + + fcl = functionClauseList_setImplictConstraints($7); + + idDecl_addClauses ($$, fcl); + + DPRINTF((message("added fuctionClause List: %s to the Id", + functionClauseList_unparse(fcl) + ) + )); + + context_popLoc (); lltok_free2 ($3, $5); } diff --git a/src/clabstract.c b/src/clabstract.c index 304d0ed..3798ba6 100644 --- a/src/clabstract.c +++ b/src/clabstract.c @@ -512,41 +512,61 @@ void setImplictfcnConstraints (void) if (constraintList_isDefined(implicitFcnConstraints) ) constraintList_free(implicitFcnConstraints); - + implicitFcnConstraints = constraintList_makeNew(); uentryList_elements (params, el) { DPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) )); - s = uentry_getSref(el); - if (sRef_isReference (s) ) + if ( uentry_isVariable (el) ) { - DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) )); - } - else + s = uentry_getSref(el); + if (sRef_isReference (s) ) + { + + DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) )); + /*drl 4/26/01 + chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0 */ + c = constraint_makeSRefWriteSafeInt (s, 0); + + implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c); + + /*drl 10/23/2002 added support for out*/ + + if (!uentry_isOut(el) ) + { + c = constraint_makeSRefReadSafeInt (s, 0); + + implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c); + } + } + else + { + DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) )); + } + } /*end uentry_isVariable*/ + + else if (uentry_isElipsisMarker (el) ) { - DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) )); + /*just ignore these*/ + ; } - /*drl 4/26/01 - chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0 */ - c = constraint_makeSRefWriteSafeInt (s, 0); - implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c); - - /*drl 10/23/2002 added support for out*/ - if (!uentry_isOut(el) ) + else { - c = constraint_makeSRefReadSafeInt (s, 0); - - implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c); + /*just ignore this + I'm not sure if this is possible though + */ + /*@warning take this out befor@*/ + llassert(FALSE); } - - } + end_uentryList_elements; DPRINTF((message("implicitFcnConstraints has been set to %s\n", constraintList_print(implicitFcnConstraints) ) )); + } diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c index d919f01..0a48a90 100644 --- a/src/constraintGeneration.c +++ b/src/constraintGeneration.c @@ -2242,23 +2242,23 @@ constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist) preconditions = constraintList_makeNew(); } - /*@i523@ drl remember to remove this code before you make a splint release. */ - /* if (context_getFlag (FLG_IMPLICTCONSTRAINT) ) { - - uentryList_elements (params, el) + + /* + uentryList_elements (arglist, el) { - DPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) )); + sRef s; + TPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) )); s = uentry_getSref(el); if (sRef_isReference (s) ) { - DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) )); + TPRINTF((message ("%s is a pointer", sRef_unparse(s) ) )); } else { - DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) )); + TPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) )); } //drl 4/26/01 //chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0 @@ -2270,15 +2270,14 @@ constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist) if (!uentry_isOut(el) ) { c = constraint_makeSRefReadSafeInt (s, 0); - implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c); } - + } - + */ } - */ + DPRINTF ((message("Done checkCall\n"))); DPRINTF ((message("Returning list %q ", constraintList_printDetailed(preconditions)))); diff --git a/src/functionClauseList.c b/src/functionClauseList.c index f35d6a5..825c214 100644 --- a/src/functionClauseList.c +++ b/src/functionClauseList.c @@ -172,9 +172,25 @@ functionClauseList_free (functionClauseList s) } } -void -functionClauseList_getImplictConstraints (functionClauseList s) +functionClauseList +functionClauseList_setImplictConstraints (/*@returned@*/ functionClauseList s) { + bool addedConstraints; + + constraintList c; + + DPRINTF ((message ("functionClauseList_setImplictConstraints called ") )); + + addedConstraints = FALSE; + + + c = getImplicitFcnConstraints (); + + if (constraintList_isEmpty(c) ) + { + return s; + } + functionClauseList_elements(s, el) { if (functionClause_isRequires(el)) @@ -188,12 +204,15 @@ functionClauseList_getImplictConstraints (functionClauseList s) constraintList implCons = getImplicitFcnConstraints (); DPRINTF ((message ("functionClauseList_ImplictConstraints adding the implict constraints: %s to %s", - constraintList_print(implCons), constraintList_print (con->constraint.buffer)))); + constraintList_print(implCons), constraintList_print (con->constraint.buffer)))); - functionConstraint_addBufferConstraints (con, constraintList_copy (implCons)); + functionConstraint_addBufferConstraints (con, constraintList_copy (implCons) ); + + addedConstraints = TRUE; DPRINTF ((message ("functionClauseList_ImplictConstraints the new constraint is %s", functionConstraint_unparse (con)))); + } else { @@ -204,5 +223,20 @@ functionClauseList_getImplictConstraints (functionClauseList s) } } - end_functionClauseList_elements + end_functionClauseList_elements; + + if (!addedConstraints) + { + functionConstraint fCon; + functionClause fClause; + + constraintList implCons = getImplicitFcnConstraints (); + + fCon = functionConstraint_createBufferConstraint(constraintList_copy (implCons) ); + fClause = functionClause_createRequires(fCon); + s = functionClauseList_add(s, fClause); + + + } + return s; } diff --git a/src/functionConstraint.c b/src/functionConstraint.c index 5a30602..785e2f3 100644 --- a/src/functionConstraint.c +++ b/src/functionConstraint.c @@ -219,9 +219,36 @@ extern void functionConstraint_free (/*@only@*/ functionConstraint node) } } -void functionConstraint_addBufferConstraints (functionConstraint fc, constraintList clist) +/*drl modified */ +void functionConstraint_addBufferConstraints (functionConstraint node, constraintList clist) { - llassert (functionConstraint_isBufferConstraint (fc)); - fc->constraint.buffer = constraintList_addList (fc->constraint.buffer, clist); -} + constraintList temp; + temp = constraintList_copy (clist); + + if (functionConstraint_isDefined (node)) + { + if (node->kind == FCT_CONJUNCT) + { + functionConstraint_addBufferConstraints (node->constraint.conjunct.op1, constraintList_copy(temp) ); + functionConstraint_addBufferConstraints (node->constraint.conjunct.op2,temp); + } + else + { + if (node->kind == FCT_BUFFER) + { + node->constraint.buffer = constraintList_addList(node->constraint.buffer, temp); + } + else + { + constraintList_free (temp); + return; + } + } + } + else + { + constraintList_free (temp); + return; + } +} diff --git a/src/idDecl.c b/src/idDecl.c index 851c622..76ba025 100644 --- a/src/idDecl.c +++ b/src/idDecl.c @@ -247,6 +247,15 @@ void idDecl_addClauses (idDecl d, functionClauseList clauses) { llassert (idDecl_isDefined (d)); - llassert (functionClauseList_isUndefined (d->clauses)); + /*@i222*/ + /* + This breaks on sometypes of functionPointers. + I.e. + void (*signal (int sig ) @requires g >= 0 @ ) (int) @requires g >= 0 @ ; + + llassert (functionClauseList_isUndefined (d->clauses)); + + */ + d->clauses = clauses; } diff --git a/test/Makefile.in b/test/Makefile.in index e5b7ad8..9e34fc2 100644 --- a/test/Makefile.in +++ b/test/Makefile.in @@ -1392,13 +1392,6 @@ mystrncat: noeffect: ${SPLINTP} noeffect.c +allmacros +checks -expect 3 - -.PHONY: numabstract -numabstract: - -$(SPLINTR) numabstract.c -expect 11 - -$(SPLINTR) numabstract.c +numabstractlit -expect 9 - -$(SPLINTR) numabstract.c -numabstractcast -expect 10 - ### ### 2002-01-01: null1.c: expect increased to 15 because out must be defined ### checking detects one new error @@ -1429,6 +1422,14 @@ nullassign: -$(SPLINTR) nullassign.c -expect 2 -$(SPLINTR) -nullassign nullassign.c -expect 1 +### Added for 3.1 - evans 2002-12-14 + +.PHONY: numabstract +numabstract: + -$(SPLINTR) numabstract.c -expect 11 + -$(SPLINTR) numabstract.c +numabstractlit -expect 9 + -$(SPLINTR) numabstract.c -numabstractcast -expect 10 + # # Before 2.4, expected one more because error was reported both as # dependent and observer. -- 2.45.1