stdlib.c

Go to the documentation of this file.

/* FUNCTION: abs */
 
#ifndef __CPROVER_LIMITS_H_INCLUDED
#  include <limits.h>
#  define __CPROVER_LIMITS_H_INCLUDED
#endif
 
#undef abs
 
int abs(int i)
{
  // C99 Section 7.20.6.1:
  // "If the result cannot be represented, the behavior is undefined."
  __CPROVER_precondition(i != INT_MIN, "argument to abs must not be INT_MIN");
  return __CPROVER_abs(i);
}
 
/* FUNCTION: labs */
 
#ifndef __CPROVER_LIMITS_H_INCLUDED
#  include <limits.h>
#  define __CPROVER_LIMITS_H_INCLUDED
#endif
 
#undef labs
 
long int labs(long int i)
{
  // C99 Section 7.20.6.1:
  // "If the result cannot be represented, the behavior is undefined."
  __CPROVER_precondition(
    i != LONG_MIN, "argument to labs must not be LONG_MIN");
  return __CPROVER_labs(i);
}
 
/* FUNCTION: llabs */
 
#ifndef __CPROVER_LIMITS_H_INCLUDED
#  include <limits.h>
#  define __CPROVER_LIMITS_H_INCLUDED
#endif
 
#undef llabs
 
long long int llabs(long long int i)
{
  // C99 Section 7.20.6.1:
  // "If the result cannot be represented, the behavior is undefined."
  __CPROVER_precondition(
    i != LLONG_MIN, "argument to llabs must not be LLONG_MIN");
  return __CPROVER_llabs(i);
}
 
/* FUNCTION: imaxabs */
 
#ifndef __CPROVER_INTTYPES_H_INCLUDED
#  include <inttypes.h>
#  define __CPROVER_INTTYPES_H_INCLUDED
#endif
 
#ifndef __CPROVER_LIMITS_H_INCLUDED
#  include <limits.h>
#  define __CPROVER_LIMITS_H_INCLUDED
#endif
 
#undef imaxabs
 
intmax_t __CPROVER_imaxabs(intmax_t);
 
intmax_t imaxabs(intmax_t i)
{
  __CPROVER_precondition(
    i != INTMAX_MIN, "argument to imaxabs must not be INTMAX_MIN");
  return __CPROVER_imaxabs(i);
}
 
/* FUNCTION: __builtin_abs */
 
int __builtin_abs(int i)
{
  return __CPROVER_abs(i);
}
 
/* FUNCTION: __builtin_labs */
 
long int __builtin_labs(long int i)
{
  return __CPROVER_labs(i);
}
 
/* FUNCTION: __builtin_llabs */
 
long long int __builtin_llabs(long long int i)
{
  return __CPROVER_llabs(i);
}
 
/* FUNCTION: exit */
 
#undef exit
 
void exit(int status)
{
  (void)status;
  __CPROVER_assume(0);
#ifdef LIBRARY_CHECK
  __builtin_unreachable();
#endif
}
 
/* FUNCTION: _Exit */
 
#undef _Exit
 
void _Exit(int status)
{
  (void)status;
  __CPROVER_assume(0);
#ifdef LIBRARY_CHECK
  __builtin_unreachable();
#endif
}
 
/* FUNCTION: abort */
 
#undef abort
 
void abort(void)
{
  __CPROVER_assume(0);
#ifdef LIBRARY_CHECK
  __builtin_unreachable();
#endif
}
 
/* FUNCTION: calloc */
 
#undef calloc
 
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
#ifndef __GNUC__
_Bool __builtin_mul_overflow();
#endif
__CPROVER_bool __CPROVER_malloc_is_new_array = 0;
 
void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
{
__CPROVER_HIDE:;
  __CPROVER_size_t alloc_size;
  if(__builtin_mul_overflow(nmemb, size, &alloc_size))
    return (void *)0;
 
  if(__CPROVER_malloc_failure_mode == __CPROVER_malloc_failure_mode_return_null)
  {
    __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
    if(
      alloc_size > __CPROVER_max_malloc_size ||
      (__CPROVER_malloc_may_fail && should_malloc_fail))
    {
      return (void *)0;
    }
  }
  else if(
    __CPROVER_malloc_failure_mode ==
    __CPROVER_malloc_failure_mode_assert_then_assume)
  {
    __CPROVER_assert(
      alloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded");
    __CPROVER_assume(alloc_size <= __CPROVER_max_malloc_size);
 
    __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
    __CPROVER_assert(
      !__CPROVER_malloc_may_fail || !should_malloc_fail,
      "max allocation may fail");
    __CPROVER_assume(!__CPROVER_malloc_may_fail || !should_malloc_fail);
  }
 
  void *malloc_res;
  // realistically, calloc may return NULL,
  // and __CPROVER_allocate doesn't, but no one cares
  malloc_res = __CPROVER_allocate(alloc_size, 1);
 
  // record the object size for non-determistic bounds checking
  __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
  __CPROVER_malloc_is_new_array =
    record_malloc ? 0 : __CPROVER_malloc_is_new_array;
 
  // detect memory leaks
  __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
  __CPROVER_memory_leak = record_may_leak ? malloc_res : __CPROVER_memory_leak;
 
#ifdef __CPROVER_STRING_ABSTRACTION
  __CPROVER_assume(__CPROVER_buffer_size(malloc_res) == alloc_size);
  __CPROVER_is_zero_string(malloc_res) = 1;
  __CPROVER_zero_string_length(malloc_res) = 0;
#endif
 
  return malloc_res;
}
 
/* FUNCTION: malloc */
 
#undef malloc
 
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
#ifndef LIBRARY_CHECK
__CPROVER_bool __CPROVER_malloc_is_new_array = 0;
#endif
 
// malloc is marked "inline" for the benefit of goto-analyzer. Really,
// goto-analyzer should take care of inlining as needed.
inline void *malloc(__CPROVER_size_t malloc_size)
{
// realistically, malloc may return NULL,
// but we only do so if `--malloc-may-fail` is set
__CPROVER_HIDE:;
 
  if(__CPROVER_malloc_failure_mode == __CPROVER_malloc_failure_mode_return_null)
  {
    __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
    if(
      malloc_size > __CPROVER_max_malloc_size ||
      (__CPROVER_malloc_may_fail && should_malloc_fail))
    {
      return (void *)0;
    }
  }
  else if(
    __CPROVER_malloc_failure_mode ==
    __CPROVER_malloc_failure_mode_assert_then_assume)
  {
    __CPROVER_assert(
      malloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded");
    __CPROVER_assume(malloc_size <= __CPROVER_max_malloc_size);
 
    __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
    __CPROVER_assert(
      !__CPROVER_malloc_may_fail || !should_malloc_fail,
      "max allocation may fail");
    __CPROVER_assume(!__CPROVER_malloc_may_fail || !should_malloc_fail);
  }
 
  void *malloc_res;
  malloc_res = __CPROVER_allocate(malloc_size, 0);
 
  // record the object size for non-determistic bounds checking
  __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
  __CPROVER_malloc_is_new_array =
    record_malloc ? 0 : __CPROVER_malloc_is_new_array;
 
  // detect memory leaks
  __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
  __CPROVER_memory_leak = record_may_leak ? malloc_res : __CPROVER_memory_leak;
 
#ifdef __CPROVER_STRING_ABSTRACTION
  __CPROVER_assume(__CPROVER_buffer_size(malloc_res) == malloc_size);
#endif
 
  return malloc_res;
}
 
/* FUNCTION: __builtin_alloca */
 
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
const void *__CPROVER_alloca_object = 0;
#ifndef LIBRARY_CHECK
__CPROVER_bool __CPROVER_malloc_is_new_array = 0;
#endif
 
void *__builtin_alloca(__CPROVER_size_t alloca_size)
{
  __CPROVER_HIDE:;
  void *res;
  res = __CPROVER_allocate(alloca_size, 0);
 
  // record the object size for non-determistic bounds checking
  __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
  __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
 
  // record alloca to detect invalid free
  __CPROVER_bool record_alloca = __VERIFIER_nondet___CPROVER_bool();
  __CPROVER_alloca_object = record_alloca ? res : __CPROVER_alloca_object;
 
#ifdef __CPROVER_STRING_ABSTRACTION
  __CPROVER_assume(__CPROVER_buffer_size(res) == alloca_size);
#endif
 
  return res;
}
 
/* FUNCTION: alloca */
 
#undef alloca
 
void *__builtin_alloca(__CPROVER_size_t alloca_size);
 
void *alloca(__CPROVER_size_t alloca_size)
{
__CPROVER_HIDE:;
  return __builtin_alloca(alloca_size);
}
 
/* FUNCTION: free */
 
#undef free
 
void __CPROVER_deallocate(void *);
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
#ifndef LIBRARY_CHECK
const void *__CPROVER_alloca_object = 0;
#endif
const void *__CPROVER_new_object = 0;
#ifndef LIBRARY_CHECK
__CPROVER_bool __CPROVER_malloc_is_new_array = 0;
#endif
 
void free(void *ptr)
{
  __CPROVER_HIDE:;
  // If ptr is NULL, no operation is performed.
  __CPROVER_precondition(
    ptr == 0 || __CPROVER_r_ok(ptr, 0),
    "free argument must be NULL or valid pointer");
  __CPROVER_precondition(ptr==0 || __CPROVER_DYNAMIC_OBJECT(ptr),
                         "free argument must be dynamic object");
  __CPROVER_precondition(ptr==0 || __CPROVER_POINTER_OFFSET(ptr)==0,
                         "free argument has offset zero");
 
  // catch double free
  __CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr,
                         "double free");
 
  // catch people who try to use free(...) for stuff
  // allocated with new[]
  __CPROVER_precondition(
    ptr == 0 || __CPROVER_new_object != ptr || !__CPROVER_malloc_is_new_array,
    "free called for new[] object");
 
  // catch people who try to use free(...) with alloca
  __CPROVER_precondition(
    ptr == 0 || __CPROVER_alloca_object != ptr,
    "free called for stack-allocated object");
 
  if(ptr!=0)
  {
    __CPROVER_deallocate(ptr);
 
    // detect memory leaks
    if(__CPROVER_memory_leak==ptr)
      __CPROVER_memory_leak=0;
  }
}
 
/* FUNCTION: strtol */
 
#ifndef __CPROVER_ERRNO_H_INCLUDED
#include <errno.h>
#define __CPROVER_ERRNO_H_INCLUDED
#endif
 
#ifndef __CPROVER_LIMITS_H_INCLUDED
#include <limits.h>
#define __CPROVER_LIMITS_H_INCLUDED
#endif
 
#undef strtol
#undef isdigit
#undef isspace
 
int isspace(int);
int isdigit(int);
 
#ifndef __GNUC__
_Bool __builtin_add_overflow();
_Bool __builtin_mul_overflow();
#endif
 
long strtol(const char *nptr, char **endptr, int base)
{
  __CPROVER_HIDE:;
  #ifdef __CPROVER_STRING_ABSTRACTION
  __CPROVER_precondition(__CPROVER_is_zero_string(nptr),
    "zero-termination of argument of strtol");
  #endif
 
  if(base==1 || base<0 || base>36)
  {
    errno=EINVAL;
    return 0;
  }
 
  long res=0;
  _Bool in_number=0;
  char sign=0;
 
  // 32 chars is an arbitrarily chosen limit
  int i=0;
  for( ; i<31; ++i)
  {
    char ch=nptr[i];
    char sub=0;
    if(ch==0)
      break;
    else if((base==0 || base==16) && !in_number &&
            ch=='0' && (nptr[i+1]=='x' || nptr[i+1]=='X'))
    {
      base=16;
      in_number=1;
      ++i;
      continue;
    }
    else if(base==0 && !in_number && ch=='0')
    {
      base=8;
      in_number=1;
      continue;
    }
    else if(!in_number && !sign && isspace(ch))
      continue;
    else if(!in_number && !sign && (ch=='-' || ch=='+'))
    {
      sign=ch;
      continue;
    }
    else if(base>10 && ch>='a' && ch-'a'<base-10)
      sub='a'-10;
    else if(base>10 && ch>='A' && ch-'A'<base-10)
      sub='A'-10;
    else if(isdigit(ch))
    {
      sub='0';
      base=base==0 ? 10 : base;
    }
    else
      break;
 
    in_number=1;
    _Bool overflow = __builtin_mul_overflow(res, (long)base, &res);
    if(overflow || __builtin_add_overflow(res, (long)(ch - sub), &res))
    {
      errno=ERANGE;
      if(sign=='-')
        return LONG_MIN;
      else
        return LONG_MAX;
    }
  }
 
  if(endptr!=0)
    *endptr=(char*)nptr+i;
 
  if(sign=='-')
    res*=-1;
 
  return res;
}
 
/* FUNCTION: atoi */
 
#undef atoi
#undef strtol
 
long strtol(const char *nptr, char **endptr, int base);
 
int atoi(const char *nptr)
{
  __CPROVER_HIDE:;
  return (int)strtol(nptr, (char **)0, 10);
}
 
/* FUNCTION: atol */
 
#undef atol
#undef strtol
 
long strtol(const char *nptr, char **endptr, int base);
 
long atol(const char *nptr)
{
  __CPROVER_HIDE:;
  return strtol(nptr, (char **)0, 10);
}
 
/* FUNCTION: getenv */
 
#undef getenv
 
#ifndef __CPROVER_STDDEF_H_INCLUDED
#  include <stddef.h>
#  define __CPROVER_STDDEF_H_INCLUDED
#endif
 
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
ptrdiff_t __VERIFIER_nondet_ptrdiff_t(void);
 
char *getenv(const char *name)
{
  __CPROVER_HIDE:;
 
  (void)*name;
  #ifdef __CPROVER_STRING_ABSTRACTION
  __CPROVER_precondition(__CPROVER_is_zero_string(name),
    "zero-termination of argument of getenv");
  #endif
 
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
  __CPROVER_event("invalidate_pointer", "getenv_result");
  char *getenv_result;
  __CPROVER_set_must(getenv_result, "getenv_result");
  return getenv_result;
 
#else
 
  __CPROVER_bool found=__VERIFIER_nondet___CPROVER_bool();
  if(!found) return 0;
 
  ptrdiff_t buf_size = __VERIFIER_nondet_ptrdiff_t();
 
  // It's reasonable to assume this won't exceed the signed
  // range in practice, but in principle, this could exceed
  // the range.
 
  __CPROVER_assume(buf_size >= 1);
  char *buffer = (char *)__CPROVER_allocate(buf_size * sizeof(char), 0);
  buffer[buf_size-1]=0;
 
#  ifdef __CPROVER_STRING_ABSTRACTION
  __CPROVER_assume(__CPROVER_buffer_size(buffer) == buf_size);
  __CPROVER_is_zero_string(buffer) = 1;
  __CPROVER_zero_string_length(buffer) = buf_size - 1;
#  endif
 
  return buffer;
#endif
}
 
/* FUNCTION: realloc */
 
void *malloc(__CPROVER_size_t malloc_size);
void free(void *ptr);
 
void *realloc(void *ptr, __CPROVER_size_t malloc_size)
{
  __CPROVER_HIDE:;
 
  __CPROVER_precondition(ptr==0 || __CPROVER_DYNAMIC_OBJECT(ptr),
                         "realloc argument is dynamic object");
 
  // if ptr is NULL, this behaves like malloc
  if(ptr==0)
    return malloc(malloc_size);
 
  // if malloc-size is 0, allocate new minimum sized object
  // and free original
  if(malloc_size==0)
  {
    free(ptr);
    return malloc(0);
  }
 
  // this shouldn't move if the new size isn't bigger
  void *res;
  res=malloc(malloc_size);
  if(res != (void *)0)
  {
    __CPROVER_array_copy(res, ptr);
    free(ptr);
  }
 
  return res;
}
 
/* FUNCTION: valloc */
 
void *malloc(__CPROVER_size_t malloc_size);
 
void *valloc(__CPROVER_size_t malloc_size)
{
  // The allocated memory is aligned on a page
  // boundary, which we don't model.
 
  __CPROVER_HIDE:;
  return malloc(malloc_size);
}
 
/* FUNCTION: posix_memalign */
 
#ifndef __CPROVER_ERRNO_H_INCLUDED
#include <errno.h>
#define __CPROVER_ERRNO_H_INCLUDED
#endif
 
#undef posix_memalign
 
void *malloc(__CPROVER_size_t malloc_size);
int posix_memalign(
  void **ptr,
  __CPROVER_size_t alignment,
  __CPROVER_size_t size)
{
__CPROVER_HIDE:;
 
  __CPROVER_size_t multiplier = alignment / sizeof(void *);
  // Modeling the posix_memalign checks on alignment.
  if(
    alignment % sizeof(void *) != 0 || ((multiplier) & (multiplier - 1)) != 0 ||
    alignment == 0)
  {
    return EINVAL;
  }
  // The address of the allocated memory is supposed to be aligned with
  // alignment. As cbmc doesn't model address alignment,
  // assuming MALLOC_ALIGNMENT = MAX_INT_VALUE seems fair.
  // As _mid_memalign simplifies for alignment <= MALLOC_ALIGNMENT
  // to a malloc call, it should be sound, if we do it too.
 
  void *tmp = malloc(size);
  if(tmp != (void *)0)
  {
    *ptr = tmp;
    return 0;
  }
  return ENOMEM;
}
 
/* FUNCTION: random */
 
long __VERIFIER_nondet_long(void);
 
long random(void)
{
  // We return a non-deterministic value instead of a random one.
  __CPROVER_HIDE:;
  long result=__VERIFIER_nondet_long();
  __CPROVER_assume(result>=0 && result<=2147483647);
  return result;
}
 
/* FUNCTION: rand */
 
int __VERIFIER_nondet_int(void);
 
int rand(void)
{
__CPROVER_HIDE:;
  // We return a non-deterministic value instead of a random one.
  int result = __VERIFIER_nondet_int();
  __CPROVER_assume(result >= 0);
  return result;
}
 
/* FUNCTION: rand_r */
 
int __VERIFIER_nondet_int(void);
 
int rand_r(unsigned int *seed)
{
__CPROVER_HIDE:;
  // We return a non-deterministic value instead of a random one.
  (void)*seed;
  int result = __VERIFIER_nondet_int();
  __CPROVER_assume(result >= 0);
  return result;
}
 
/* FUNCTION: __CPROVER_deallocate */
 
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
void __CPROVER_deallocate(void *ptr)
{
  if(__VERIFIER_nondet___CPROVER_bool())
    __CPROVER_deallocated = ptr;
}