Added support for default buffer constraint annotations

and merged with previously committed code.

diff --git a/src/Headers/functionConstraint.h b/src/Headers/functionConstraint.h
index 546e102a06256bc52502ae0fbd93a2380d76fd17..5d6b72aaa6376c52ac0d43168dd91d4a9dfc2e54 100644 (file)
--- 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 0dadfc17e18b6dc5c9a26349337ad90c156b1667..4685875c3ff054505a1f6c21be317a95ed127f6a 100644 (file)
--- 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 e889b900cbbec5d0a8b8acf3c4e06d00f37dcfdd..c7f03df49b4a5761b2e3621ab35b05e1c85e6b09 100644 (file)
--- 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 8c3a3e22e4ba47a67b2cce0ab5c607c16b7068eb..c79a2ee763107c67b040e00fa3c14c94e49d09d5 100644 (file)
--- 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 3134c11af2e6e3d0142c6da3cc1f1f40c0806c2c..7294805ecfac2f9861398df1a4a532284ba0b7ec 100644 (file)
--- 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 304d0edc97c209f6251a17f953928b755506cf24..3798ba6d945727617d53527f26506d45fc4607cb 100644 (file)
--- 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 d919f0154e7c6ac63e3907be9ff5a5d03718784d..0a48a9070c8d729fc745fefd5f3e4be27dc839fd 100644 (file)
--- 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 f35d6a544607a2eb5c379ba422c00bdb17eb2332..825c2149826698bac42827ed3d828b0c58caac1a 100644 (file)
--- 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 5a30602f881c0a95c52e6d5731874054b3c1d6d0..785e2f37903443a5db14289f09f222bcc7da43d3 100644 (file)
--- 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 851c622819faa34d89aa4a2ac9bea090aa881c7e..76ba025d9b143ed5ceb44eb2493f9ad2ecbb2016 100644 (file)
--- 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 e5b7ad88018874175b36de5483fda62ee6b8ca82..9e34fc2d1f0a0267c2ca3dcbd0726a563441ea0e 100644 (file)
--- 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.