From 5ca29538dc03edec2ad7043a925ceb4b12c1d950 Mon Sep 17 00:00:00 2001
From: drl7x <drl7x>
Date: Mon, 1 Jul 2002 08:59:13 +0000
Subject: [PATCH] Apparently splint does not correctly handle the case in which
 a #defined constant is used in the function constraint unless it's been
 specified with the constant annotation.

Modified splint to halt and print a message suggesting that the constant annotation be used.
---
 lib/Makefile.am             |  4 ++++
 lib/Makefile.in             |  5 +++++
 src/clabstract.c            | 11 +++++++++--
 test/moreBufferTests2/def.c | 10 ++++++++++
 4 files changed, 28 insertions(+), 2 deletions(-)
 create mode 100644 test/moreBufferTests2/def.c

diff --git a/lib/Makefile.am b/lib/Makefile.am
index 07f8c09..74d9527 100644
--- 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 35c4a16..c7cb493 100644
--- 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 5628c15..a100791 100644
--- 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
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';
+}
-- 
2.45.2