bugfix: pointer check failure in fgets

Now we assume str_length greater than 0, since no dereference should take place when str_length equals 0.
Updated cbmc-library/fgets-01 regression test.

Fixes: #4621

Author: mauguignard

regression/cbmc-library/fgets-01/test.desc

@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 \[main.assertion.3\] line 16 assertion p\[1\] == 'b': FAILURE
-\*\* 2 of \d+ failed
+\*\* 1 of \d+ failed
 --
 ^warning: ignoring

src/ansi-c/library/stdio.c

@@ -259,7 +259,7 @@ char *fgets(char *str, int size, FILE *stream)
   if(size>0)
   {
     int str_length=__VERIFIER_nondet_int();
-    __CPROVER_assume(str_length>=0 && str_length<size);
+    __CPROVER_assume(str_length>0 && str_length<size);
     // check that the memory is accessible
     (void)*(char *)str;
     (void)*(((const char *)str) + str_length - 1);