Added files for test case.

diff --git a/test/simplebufferConstraintTests/m.c b/test/simplebufferConstraintTests/m.c
new file mode 100644 (file)
index 0000000..129144d
--- /dev/null
+++ b/test/simplebufferConstraintTests/m.c
@@ -0,0 +1,11 @@
+extern /*@null@*/ /*@out@*/ /*@only@*/ void *mymalloc (size_t size) /*@*/
+     /*@ensuresConstraint MaxSet(result) == (size - 1); @*/ ;
+  
+void t()
+{
+char *f;
+
+f = mymalloc (3);
+f[2] = '2';
+free (f);
+}

diff --git a/test/simplebufferConstraintTests/sizeof.c b/test/simplebufferConstraintTests/sizeof.c
new file mode 100644 (file)
index 0000000..d95b92b
--- /dev/null
+++ b/test/simplebufferConstraintTests/sizeof.c
@@ -0,0 +1,20 @@
+
+extern void /*@alt char * @*/
+  mystrncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2,
+size_t n) 
+  /*@modifies *s1@*/      /*@bufferConstraint MaxSet(s1) >= ( n - 1
+); MaxRead (s2) >= ( n - 1 ); @*/ /*@ensuresConstraint MaxRead (s1) ==
+MaxRead (s2); MaxRead (s1) <= n; @*/; 
+
+ void f(char *z) /*@bufferConstraint MaxRead(z) >= 2; @*/
+{
+char x[3];
+char y[3];
+
+mystrncpy (x, z, 3);
+mystrncpy (y, z, 3);
+
+x[(sizeof x)] = 'i';
+y[((sizeof y) - 1)] = '0';
+
+}

diff --git a/test/simplebufferConstraintTests/test3.c b/test/simplebufferConstraintTests/test3.c
new file mode 100644 (file)
index 0000000..f3967c4
--- /dev/null
+++ b/test/simplebufferConstraintTests/test3.c
@@ -0,0 +1,11 @@
+
+void t()
+{
+  char g [100];
+  char j [23];
+  j[22] = 'd';  /*safe */
+  g[0] = 'd';  /*   safe */
+  g[67] = 'f;'; /*     safe */
+  g[101] = 'g'; /*    unsafe */
+  g[100] = 'f'; /*    unsafe */
+}

diff --git a/test/simplebufferConstraintTests/test7.c b/test/simplebufferConstraintTests/test7.c
new file mode 100644 (file)
index 0000000..75676c4
--- /dev/null
+++ b/test/simplebufferConstraintTests/test7.c
@@ -0,0 +1,11 @@
+
+void t(char *g, char *j )
+{
+  g++;
+  g++;
+  g[2] = 'l';
+  g[0] = g[2];
+  j[0] = 'l';
+  j++;
+  j++;
+}