overflows in getenv

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@5864 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

regression/cbmc/getenv-overflow1/main.c

@@ -0,0 +1,8 @@
+#include <stdlib.h>
+
+int main()
+{
+  char *something;
+  // there should not be any overflow in there
+  something=getenv("HOME");
+}

regression/cbmc/getenv-overflow1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--signed-overflow-check --unsigned-overflow-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/library/stdlib.c

@@ -295,6 +295,11 @@ inline long atol(const char *nptr)
 
 #undef getenv
 
+#ifndef __CPROVER_LIMITS_H_INCLUDED
+#include <limits.h>
+#define __CPROVER_LIMITS_H_INCLUDED
+#endif
+
 inline char *getenv(const char *name)
 {
   __CPROVER_HIDE:;
@@ -311,7 +316,11 @@ inline char *getenv(const char *name)
   char *buffer;
   __CPROVER_size_t buf_size;
 
-  __CPROVER_assume(buf_size>=1);
+  // It's reasonable to assume this won't exceed the signed
+  // range in practice, but in principle, this could exceed
+  // the range.
+
+  __CPROVER_assume(1<=buf_size && buf_size<=SSIZE_MAX);
   buffer=(char *)__CPROVER_malloc(buf_size);
   buffer[buf_size-1]=0;