Apparently splint does not correctly handle the case in which a #defined constant...

Modified splint to halt and print a message suggesting that the constant annotation be used.

diff --git a/lib/Makefile.am b/lib/Makefile.am
index 07f8c094a7bbdddceec80d52fe4f334a0af2f824..74d952721fd906781e64638fcc45d38b7335d217 100644 (file)
--- a/lib/Makefile.am
+++ b/lib/Makefile.am
@@ -18,6 +18,10 @@ splintlib_DATA = \
 ## Include them in the distribution
 EXTRA_DIST = $(splintlib_DATA)
 
+##get rid of lcd files if the user does a make clean
+CLEANFILES = posix.lcd standard.lcd unix.lcd \
+             posixstrict.lcd  standardstrict.lcd  unixstrict.lcd
+
 
 ## Rules to make splint & the dumps
 

diff --git a/lib/Makefile.in b/lib/Makefile.in
index 35c4a16c3f0795f53d51052cdb4cac692a430f8c..c7cb49316dcaa3785f55b097f210ac19dae667b7 100644 (file)
--- a/lib/Makefile.in
+++ b/lib/Makefile.in
@@ -101,6 +101,10 @@ splintlib_DATA = \
 
 EXTRA_DIST = $(splintlib_DATA)
 
+CLEANFILES = posix.lcd standard.lcd unix.lcd \
+             posixstrict.lcd  standardstrict.lcd  unixstrict.lcd
+
+
 SPLINT = $(top_builddir)/src/splint$(EXEEXT)
 subdir = lib
 mkinstalldirs = $(SHELL) $(top_srcdir)/config/mkinstalldirs
@@ -186,6 +190,7 @@ install-strip:
 mostlyclean-generic:
 
 clean-generic:
+       -test -z "$(CLEANFILES)" || rm -f $(CLEANFILES)
 
 distclean-generic:
        -rm -f Makefile $(CONFIG_CLEAN_FILES) stamp-h stamp-h[0-9]*

diff --git a/src/clabstract.c b/src/clabstract.c
index 5628c1577d427a0d49053274be0d42f8fd6dae57..a100791f4ec0b2313ce8e45ed2066460ebbea10a 100644 (file)
--- a/src/clabstract.c
+++ b/src/clabstract.c
@@ -2165,6 +2165,7 @@ sRef checkStateClausesId (uentry ue)
 
 sRef checkbufferConstraintClausesId (uentry ue)
 {
+  sRef sr;
   cstring s = uentry_rawName (ue);
 
   if (cstring_equalLit (s, "result"))
@@ -2179,8 +2180,14 @@ sRef checkbufferConstraintClausesId (uentry ue)
        }
     }
   
-  DPRINTF (("constrant id: %s", uentry_unparseFull (ue)));
-  return sRef_saveCopy (uentry_getSref (ue)); /*@i523 why the saveCopy? */
+  DPRINTF (("constraint id: %s", uentry_unparseFull (ue)));
+  sr = uentry_getSref (ue);
+
+  if (sRef_isInvalid (sr) )
+    {
+      llfatalerrorLoc (cstring_makeLiteral("Macro defined constants can not be used in function constraints unless they are specifed with the constant annotation.  To use a macro defined constant include an annotation of the form /*@constant <type> <name>=<value>@*/ somewhere before the function constraint.  This restriction may be removed in future releases if it is determined to be excessively burdensome." ));
+    }
+  return sRef_saveCopy (sr); /*@i523 why the saveCopy? */
 }
 
 void checkModifiesId (uentry ue)

diff --git a/test/moreBufferTests2/def.c b/test/moreBufferTests2/def.c
new file mode 100644 (file)
index 0000000..a6023ef
--- /dev/null
+++ b/test/moreBufferTests2/def.c
@@ -0,0 +1,10 @@
+#define SIZE 10
+
+static void foo()
+{
+  char str[SIZE];
+
+  str[SIZE -1 ] = 'd';
+
+  str[SIZE] = 'd';
+}