CBMC
Loading...
Searching...
No Matches
stdlib.c File Reference
#include <limits.h>
#include <inttypes.h>
#include <errno.h>
#include <stddef.h>
Include dependency graph for stdlib.c:

Go to the source code of this file.

Macros

#define __CPROVER_LIMITS_H_INCLUDED
#define __CPROVER_INTTYPES_H_INCLUDED
#define __CPROVER_ERRNO_H_INCLUDED
#define __CPROVER_STDDEF_H_INCLUDED

Functions

int abs (int i)
long int labs (long int i)
long long int llabs (long long int i)
intmax_t __CPROVER_imaxabs (intmax_t)
intmax_t imaxabs (intmax_t i)
int __builtin_abs (int i)
long int __builtin_labs (long int i)
long long int __builtin_llabs (long long int i)
void exit (int status)
void _Exit (int status)
void abort (void)
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool (void)
_Bool __builtin_mul_overflow ()
void * calloc (__CPROVER_size_t nmemb, __CPROVER_size_t size)
void * malloc (__CPROVER_size_t malloc_size)
void * __builtin_alloca (__CPROVER_size_t alloca_size)
void * alloca (__CPROVER_size_t alloca_size)
void __CPROVER_deallocate (void *)
void free (void *ptr)
int isspace (int)
int isdigit (int)
_Bool __builtin_add_overflow ()
long strtol (const char *nptr, char **endptr, int base)
int atoi (const char *nptr)
long atol (const char *nptr)
ptrdiff_t __VERIFIER_nondet_ptrdiff_t (void)
char * getenv (const char *name)
void * realloc (void *ptr, __CPROVER_size_t malloc_size)
void * valloc (__CPROVER_size_t malloc_size)
int posix_memalign (void **ptr, __CPROVER_size_t alignment, __CPROVER_size_t size)
long __VERIFIER_nondet_long (void)
long random (void)
int __VERIFIER_nondet_int (void)
int rand (void)
int rand_r (unsigned int *seed)

Variables

__CPROVER_bool __CPROVER_malloc_is_new_array
const void * __CPROVER_alloca_object
const void * __CPROVER_new_object

Macro Definition Documentation

◆ __CPROVER_ERRNO_H_INCLUDED

#define __CPROVER_ERRNO_H_INCLUDED

Definition at line 358 of file stdlib.c.

◆ __CPROVER_INTTYPES_H_INCLUDED

#define __CPROVER_INTTYPES_H_INCLUDED

Definition at line 58 of file stdlib.c.

◆ __CPROVER_LIMITS_H_INCLUDED

#define __CPROVER_LIMITS_H_INCLUDED

Definition at line 5 of file stdlib.c.

◆ __CPROVER_STDDEF_H_INCLUDED

#define __CPROVER_STDDEF_H_INCLUDED

Definition at line 490 of file stdlib.c.

Function Documentation

◆ __builtin_abs()

int __builtin_abs ( int i)

Definition at line 79 of file stdlib.c.

◆ __builtin_add_overflow()

_Bool __builtin_add_overflow ( )

◆ __builtin_alloca()

void * __builtin_alloca ( __CPROVER_size_t alloca_size)

Definition at line 270 of file stdlib.c.

◆ __builtin_labs()

long int __builtin_labs ( long int i)

Definition at line 86 of file stdlib.c.

◆ __builtin_llabs()

long long int __builtin_llabs ( long long int i)

Definition at line 93 of file stdlib.c.

◆ __builtin_mul_overflow()

_Bool __builtin_mul_overflow ( )

◆ __CPROVER_deallocate()

void __CPROVER_deallocate ( void * ptr)

Definition at line 670 of file stdlib.c.

◆ __CPROVER_imaxabs()

intmax_t __CPROVER_imaxabs ( intmax_t )

◆ __VERIFIER_nondet___CPROVER_bool()

__CPROVER_bool __VERIFIER_nondet___CPROVER_bool ( void )

◆ __VERIFIER_nondet_int()

int __VERIFIER_nondet_int ( void )

◆ __VERIFIER_nondet_long()

long __VERIFIER_nondet_long ( void )

◆ __VERIFIER_nondet_ptrdiff_t()

ptrdiff_t __VERIFIER_nondet_ptrdiff_t ( void )

◆ _Exit()

void _Exit ( int status)

Definition at line 115 of file stdlib.c.

◆ abort()

void abort ( void )

Definition at line 128 of file stdlib.c.

◆ abs()

int abs ( int i)

Definition at line 10 of file stdlib.c.

◆ alloca()

void * alloca ( __CPROVER_size_t alloca_size)

Definition at line 297 of file stdlib.c.

◆ atoi()

int atoi ( const char * nptr)

Definition at line 465 of file stdlib.c.

◆ atol()

long atol ( const char * nptr)

Definition at line 478 of file stdlib.c.

◆ calloc()

void * calloc ( __CPROVER_size_t nmemb,
__CPROVER_size_t size )

Definition at line 146 of file stdlib.c.

◆ exit()

void exit ( int status)

Definition at line 102 of file stdlib.c.

◆ free()

void free ( void * ptr)

Definition at line 317 of file stdlib.c.

◆ getenv()

char * getenv ( const char * name)

Definition at line 496 of file stdlib.c.

◆ imaxabs()

intmax_t imaxabs ( intmax_t i)

Definition at line 70 of file stdlib.c.

◆ isdigit()

int isdigit ( int c)

Definition at line 24 of file ctype.c.

◆ isspace()

int isspace ( int c)

Definition at line 80 of file ctype.c.

◆ labs()

long int labs ( long int i)

Definition at line 27 of file stdlib.c.

◆ llabs()

long long int llabs ( long long int i)

Definition at line 45 of file stdlib.c.

◆ malloc()

void * malloc ( __CPROVER_size_t malloc_size)
inline

Definition at line 212 of file stdlib.c.

◆ posix_memalign()

int posix_memalign ( void ** ptr,
__CPROVER_size_t alignment,
__CPROVER_size_t size )

Definition at line 596 of file stdlib.c.

◆ rand()

int rand ( void )

Definition at line 643 of file stdlib.c.

◆ rand_r()

int rand_r ( unsigned int * seed)

Definition at line 656 of file stdlib.c.

◆ random()

long random ( void )

Definition at line 630 of file stdlib.c.

◆ realloc()

void * realloc ( void * ptr,
__CPROVER_size_t malloc_size )

Definition at line 542 of file stdlib.c.

◆ strtol()

long strtol ( const char * nptr,
char ** endptr,
int base )

Definition at line 378 of file stdlib.c.

◆ valloc()

void * valloc ( __CPROVER_size_t malloc_size)

Definition at line 577 of file stdlib.c.

Variable Documentation

◆ __CPROVER_alloca_object

const void* __CPROVER_alloca_object

Definition at line 265 of file stdlib.c.

◆ __CPROVER_malloc_is_new_array

__CPROVER_bool __CPROVER_malloc_is_new_array

Definition at line 144 of file stdlib.c.

◆ __CPROVER_new_object

const void* __CPROVER_new_object

Definition at line 312 of file stdlib.c.