Adds an over-approximation model for sysconf

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

regression/cbmc-library/sysconf-01/main.c

@@ -0,0 +1,8 @@
+#include <unistd.h>
+#include <errno.h>
+
+int main() {
+  errno = 0;
+  long result = sysconf(_SC_ARG_MAX);
+  __CPROVER_assert(!(errno == EINVAL) || (result == -1), "Non-deterministically set errno to EINVAL");
+}

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

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.\d+\] .* Non-deterministically set errno to EINVAL: SUCCESS$
+^\*\* 0 of 1 failed
+--
+^WARNING: no body for function sysconf

src/ansi-c/library/unistd.c

@@ -319,3 +319,27 @@ ret_type _read(int fildes, void *buf, size_type nbyte)
   __CPROVER_HIDE:;
   return read(fildes, buf, nbyte);
 }
+
+/* FUNCTION: sysconf */
+
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#include <errno.h>
+#define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
+long __VERIFIER_nondet_long(void);
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+
+long sysconf(int name);
+
+// This overapproximation is based on this specification
+// https://man7.org/linux/man-pages/man3/sysconf.3.html.
+long sysconf(int name)
+{
+  __CPROVER_HIDE:;
+  (void)name;
+  long retval = __VERIFIER_nondet_long();
+  if(retval == -1 && __VERIFIER_nondet___CPROVER_bool())
+    errno = EINVAL;
+  return retval;
+}