Import getopt{,_long} and vasprintf models from SV-COMP/busybox

Licensing: I had contributed these myself to the SV-COMP benchmarks.

Author: tautschnig

src/ansi-c/library/getopt.c

@@ -3,22 +3,67 @@
 extern char *optarg;
 extern int optind;
 
+#ifndef __CPROVER_STRING_H_INCLUDED
+#include <string.h>
+#define __CPROVER_STRING_H_INCLUDED
+#endif
+
 inline int getopt(int argc, char * const argv[],
                   const char *optstring)
 {
   __CPROVER_HIDE:;
-  int result_index;
-  __CPROVER_assume(result_index>=0);
-  (void)*optstring;
-  if(optind>=argc)
+  int result=-1;
+
+  if(optind==0)
+    optind=1;
+
+  if(optind>=argc || argv[optind][0]!='-')
     return -1;
-  __CPROVER_assume(result_index<argc && result_index>=optind);
+
+  size_t result_index;
+  __CPROVER_assume(
+    result_index<strlen(optstring) && optstring[result_index]!=':');
   #ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_assert(__CPROVER_is_zero_string(optstring),
     "getopt zero-termination of 3rd argument");
   #endif
-  optarg = argv[result_index];
-  optind = result_index+1;
-  int retval;
-  return retval;
+
+  _Bool found;
+  if(found)
+  {
+    result=optstring[result_index];
+    if(skipped)
+      ++optind;
+  }
+
+  if(result!=-1 && optind<argc && optstring[result_index+1]==':')
+  {
+    _Bool has_no_arg;
+    if(has_no_arg)
+    {
+      optarg=argv[optind];
+      ++optind;
+    }
+    else
+      optarg=NULL;
+  }
+
+  return result;
+}
+
+/* FUNCTION: getopt_long */
+
+int getopt(int argc, char * const argv[], const char *optstring);
+
+inline int getopt_long(int argc, char * const argv[], const char *optstring,
+                const struct option *longopts, int *longindex)
+{
+  // trigger valid-pointer checks (if enabled), even though we don't
+  // use the parameter in this model
+  (void)*longopts;
+  // avoid unused-parameter warnings when compiling using GCC (for
+  // internal library syntax checks)
+  (void)longindex;
+
+  return getopt(argc, argv, optstring);
 }

src/ansi-c/library/stdio.c

@@ -794,3 +794,43 @@ inline int vfprintf(FILE *stream, const char *restrict format, va_list arg)
 
   return result;
 }
+
+/* FUNCTION: vasprintf */
+
+#ifndef __CPROVER_STDIO_H_INCLUDED
+#include <stdio.h>
+#define __CPROVER_STDIO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDARG_H_INCLUDED
+#include <stdarg.h>
+#define __CPROVER_STDARG_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDLIB_H_INCLUDED
+#include <stdlib.h>
+#define __CPROVER_STDLIB_H_INCLUDED
+#endif
+
+inline int vasprintf(char **ptr, const char *fmt, va_list ap)
+{
+  (void)*fmt;
+  (void)ap;
+
+  int result_buffer_size;
+  if(result_buffer_size<=0)
+    return -1;
+
+  *ptr=malloc(result_buffer_size);
+  for(int i=0; i<result_buffer_size; ++i)
+  {
+    char c;
+    (*ptr)[i]=c;
+    if(c=='\0')
+      break;
+  }
+
+  __CPROVER_assume(i<result_buffer_size);
+
+  return i;
+}