Merge pull request #7903 from tautschnig/features/strftime

C library: model strftime

Author: tautschnig

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

@@ -0,0 +1,15 @@
+#include <assert.h>
+#include <time.h>
+
+#ifndef __DARWIN_ALIAS
+size_t _strftime(char *s, size_t max, const char *format, const struct tm *tm);
+#endif
+
+int main()
+{
+  char dest[3];
+  struct tm input;
+  size_t result = _strftime(dest, 3, "%y", &input);
+  assert(result < 3);
+  return 0;
+}

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

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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

@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <time.h>
+
+int main()
+{
+  char dest[3];
+  struct tm input;
+  size_t result = strftime(dest, 3, "%y", &input);
+  assert(result < 3);
+  return 0;
+}

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

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/library/time.c

@@ -218,3 +218,50 @@ char *ctime(const time_t *clock)
   return ctime_result;
   #endif
 }
+
+/* FUNCTION: strftime */
+
+#ifndef __CPROVER_TIME_H_INCLUDED
+#  include <time.h>
+#  define __CPROVER_TIME_H_INCLUDED
+#endif
+
+__CPROVER_size_t __VERIFIER_nondet_size_t(void);
+
+__CPROVER_size_t
+strftime(char *s, __CPROVER_size_t max, const char *format, const struct tm *tm)
+{
+  (void)*format;
+  (void)*tm;
+  __CPROVER_havoc_slice(s, max);
+  __CPROVER_size_t length = __VERIFIER_nondet_size_t();
+  if(length >= max)
+    return 0;
+  s[length] = '\0';
+  return length;
+}
+
+/* FUNCTION: _strftime */
+
+#ifndef __CPROVER_TIME_H_INCLUDED
+#  include <time.h>
+#  define __CPROVER_TIME_H_INCLUDED
+#endif
+
+__CPROVER_size_t __VERIFIER_nondet_size_t(void);
+
+__CPROVER_size_t _strftime(
+  char *s,
+  __CPROVER_size_t max,
+  const char *format,
+  const struct tm *tm)
+{
+  (void)*format;
+  (void)*tm;
+  __CPROVER_havoc_slice(s, max);
+  __CPROVER_size_t length = __VERIFIER_nondet_size_t();
+  if(length >= max)
+    return 0;
+  s[length] = '\0';
+  return length;
+}