Merge pull request #7824 from tautschnig/bugfixes/sysconf

Avoid conversion check failure sysconf library model

Author: feliperodri

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

@@ -1,12 +1,12 @@
 CORE unix
 main.c
-
+--pointer-check --bounds-check --conversion-check
 ^\[main.assertion.\d+\] line \d+ ARG\_MAX is not supported: FAILURE$
 ^\[main.assertion.\d+\] line \d+ sysconf\(\) error: FAILURE$
 ^\[main.assertion.\d+\] line \d+ ARG\_MAX is supported: FAILURE$
-^\*\* 3 of 3 failed .*$
+^\*\* 3 of \d+ failed .*$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
-^WARNING: no body for function sysconf
+^\*\*\*\* WARNING: no body for function sysconf

src/ansi-c/library/unistd.c

@@ -328,7 +328,7 @@ ret_type _read(int fildes, void *buf, size_type nbyte)
 #endif
 
 long __VERIFIER_nondet_long(void);
-unsigned int __VERIFIER_nondet_unsigned_int(void);
+int __VERIFIER_nondet_int(void);
 
 long sysconf(int name);
 
@@ -340,13 +340,13 @@ __CPROVER_HIDE:;
   (void)name;
   long retval = __VERIFIER_nondet_long();
 
-  // We should keep errno as non-determinist as possible, since this model
-  // nver takes into account the name input.
-  errno = __VERIFIER_nondet_unsigned_int();
+  // We should keep errno as non-deterministic as possible, since this model
+  // never takes into account the name input.
+  errno = __VERIFIER_nondet_int();
 
   // Spec states "some returned values may be huge; they are not suitable
   // for allocating memory". There aren't also guarantees about return
-  // values being strickly equal or greater to -1.
+  // values being strictly equal or greater to -1.
   // Thus, modelling it as non-deterministic.
   return retval;
 }