Added test cases from the buffer checking chapter of the manual.

diff --git a/test/manual.expect b/test/manual.expect
index 99f9ad24b5a005fba3b99dd9f03652eb53829079..1c0a98608b796a658d95e5c27e03e54a57269cf4 100644 (file)
--- a/test/manual.expect
+++ b/test/manual.expect
@@ -198,3 +198,36 @@ Finished checking --- 1 code warning, as expected
 ignore.c:10: Return value (type bool) ignored: fb()
 
 Finished checking --- 1 code warning, as expected
+
+setChar.c:5: Possible out-of-bounds store:
+    buf[10]
+    Unable to resolve constraint:
+    requires 9 >= 10
+     needed to satisfy precondition:
+    requires maxSet(buf @ setChar.c:5) >= 10
+
+Finished checking --- 1 code warning, as expected
+
+multiError.c:4: Possible out-of-bounds store:
+    buf[2]
+    Unable to resolve constraint:
+    requires maxSet(buf @ multiError.c:4) >= 2
+     needed to satisfy precondition:
+    requires maxSet(buf @ multiError.c:4) >= 2
+
+Finished checking --- 1 code warning, as expected
+
+updateMyEnv.c:16: Possible out-of-bounds store:
+    strcpy(str, tmp)
+    Unable to resolve constraint:
+    requires maxSet(str @ updateMyEnv.c:16) >=
+    maxRead(getenv("MYENV") @ updateMyEnv.c:14)
+     needed to satisfy precondition:
+    requires maxSet(str @ updateMyEnv.c:16) >=
+    maxRead(tmp @ updateMyEnv.c:16)
+     derived from strcpy precondition: requires
+    maxSet(<parameter 1>) >= maxRead(<parameter 2>)
+
+Finished checking --- 1 code warning, as expected
+
+Finished checking --- no warnings

diff --git a/test/manual/Makefile b/test/manual/Makefile
index 255b2b1db0f13f03a55e31d38c3bd36f0c2ec195..89b225df08e40fd11e925bbe14a8c7a91fa82cea 100755 (executable)
--- a/test/manual/Makefile
+++ b/test/manual/Makefile
@@ -21,7 +21,7 @@ DIFF = diff
 
 all: sample null mstring usedef bool palindrome only stack rstring unique \
      exposure modify globals annotglobs clauses order loop switch noeffect \
-     ignore
+     ignore setChar multiError updateMyEnv updateMyEnvGood
 
 ### In line example
 .PHONY: sample
@@ -138,10 +138,31 @@ ignore: ignore.c
        $(SPLINT) $(SPLINTFLAGS) bool.h ignore.c -retvalint -expect 1
 
 ### Figure 23:
-.PHONY: names
+.PHONY: Anames
 names: names.c
        $(SPLINT) $(SPLINTFLAGS) names.c +distinctinternalnames +internalnamelookalike +isoreserved -expect 3
 
+### Figure ???:
+
+.PHONY: setChar
+setChar: setChar.c
+       $(SPLINT) $(SPLINTFLAGS) setChar.c +arraybounds +arrayboundsread -exportlocal +constraintlocation -expect 1
+
+
+.PHONY: multiError
+multiError: multiError.c
+       $(SPLINT) $(SPLINTFLAGS) multiError.c +arraybounds +arrayboundsread -exportlocal +constraintlocation -expect 1
+
+
+.PHONY: updateMyEnv
+updateMyEnv: updateMyEnv.c
+       $(SPLINT) $(SPLINTFLAGS) updateMyEnv.c +arraybounds +arrayboundsread -exportlocal +constraintlocation -expect 1
+
+
+.PHONY: updateMyEnvGood
+updateMyEnvGood: updateMyEnvGood.c
+       $(SPLINT) $(SPLINTFLAGS) updateMyEnvGood.c +arraybounds +arrayboundsread -exportlocal +constraintlocation -expect 0
+
 clean: 
        -rm -f core a.out *.*~
 

diff --git a/test/manual/multiError.c b/test/manual/multiError.c
new file mode 100644 (file)
index 0000000..4522e73
--- /dev/null
+++ b/test/manual/multiError.c
@@ -0,0 +1,7 @@
+void multiError(char * buf)
+{
+       buf[0] = 's';
+       buf[2] =  's';
+       buf[1] =  's';
+}
+

diff --git a/test/manual/setChar.c b/test/manual/setChar.c
new file mode 100644 (file)
index 0000000..4b29fe3
--- /dev/null
+++ b/test/manual/setChar.c
@@ -0,0 +1,8 @@
+char buf[10];
+
+void setChar()
+{
+   buf[10] = 'x';
+}
+
+

diff --git a/test/manual/updateMyEnv.c b/test/manual/updateMyEnv.c
new file mode 100644 (file)
index 0000000..f2dafca
--- /dev/null
+++ b/test/manual/updateMyEnv.c
@@ -0,0 +1,19 @@
+#include<string.h>
+#include<stdlib.h>
+
+
+
+
+
+
+
+
+void updateMyEnv(char * str)
+{
+  char * tmp;
+  tmp = getenv("MYENV");
+  if (tmp != NULL)
+    strcpy (str, tmp);
+
+}
+

diff --git a/test/manual/updateMyEnvGood.c b/test/manual/updateMyEnvGood.c
new file mode 100644 (file)
index 0000000..29c0516
--- /dev/null
+++ b/test/manual/updateMyEnvGood.c
@@ -0,0 +1,25 @@
+#include<string.h>
+#include<stdlib.h>
+
+
+void updateMyEnv2(char * str) /*@requires maxSet(str) >= 1000@*/
+{
+  char * tmp;
+  tmp = getenv("MYENV");
+  if (tmp != NULL)
+    {
+      strncpy (str, tmp, 999);
+      str[999] = '/0';
+    }
+}
+
+void updateMyEnv3(char * str, size_t strSize) /*@requires maxSet(str) >= (strSize -1)@*/
+{
+  char * tmp;
+  tmp = getenv("MYENV");
+  if (tmp != NULL)
+    {
+      strncpy (str, tmp, strSize -1);
+      str[strSize -1] = '/0';
+    }
+}