simplified buffer precondition in fgets

Since we are interested in checking if the buffer is writable and we are
assuming that str_length < size, verify __CPROVER_w_ok(str, str_length + 1)
is the same as verify __CPROVER_w_ok(str, size).

Author: mauguignard

src/ansi-c/library/stdio.c

@@ -260,9 +260,7 @@ char *fgets(char *str, int size, FILE *stream)
   {
     int str_length=__VERIFIER_nondet_int();
     __CPROVER_assume(str_length >= 0 && str_length < size);
-    // check that the memory is accessible
-    __CPROVER_precondition(
-      __CPROVER_w_ok(str, str_length + 1), "fgets buffer writeable");
+    __CPROVER_precondition(__CPROVER_w_ok(str, size), "fgets buffer writable");
     char contents_nondet[str_length];
     __CPROVER_array_replace(str, contents_nondet);
     if(!error)