Merge pull request #4623 from mauguignard/fix-4621

bugfix: pointer check failure in fgets

Author: tautschnig

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,10 +259,8 @@ 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);
-    // check that the memory is accessible
-    (void)*(char *)str;
-    (void)*(((const char *)str) + str_length - 1);
+    __CPROVER_assume(str_length >= 0 && str_length < size);
+    __CPROVER_precondition(__CPROVER_w_ok(str, size), "fgets buffer writable");
     char contents_nondet[str_length];
     __CPROVER_array_replace(str, contents_nondet);
     if(!error)