ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
stdlib.c File Reference
#include <stdlib.h>
#include <string.h>
#include <ctype.h>
#include <limits.h>
#include <errno.h>
#include <stdint.h>
#include <math.h>
#include <stdbool.h>
#include <assert.h>
Include dependency graph for stdlib.c:

Classes

struct  atexit_key

Macros

#define DIV_DEF(name, result_type, type)
#define STRTOL_DEF(name, type, TYPE)
#define STRTOUL_DEF(name, type, TYPE)
#define STRTOF_DEF(name, type, mant_dig, max_exact_pow10)
#define ATOI_DEF(name, type, TYPE)

Typedefs

typedef struct atexit_key __ESBMC_atexit_key

Functions

static void __ESBMC_set_errno (int value)
 __attribute__ ((annotate("__ESBMC_inf_size")))
int atexit (void(*func)(void))
void exit (int status)
_Bool __ESBMC_no_abnormal_memory_leak (void)
void abort (void)
void _Exit (int status)
_Bool __ESBMC_sv_comp (void)
void * calloc (size_t nmemb, size_t size)
static const char * __ESBMC_strto_prefix (const char *str, int *base, int *negative)
static int __ESBMC_strto_digit (char c)
static double __ESBMC_exact_pow10 (int n)
double atof (const char *nptr)
static const unsigned char get_atoi_map (unsigned char pos)
char * getenv (const char *name)
void * ldv_malloc (size_t size)
void * ldv_zalloc (size_t size)
size_t strlcat (char *dst, const char *src, size_t siz)
int posix_memalign (void **memptr, size_t align, size_t size)
void * aligned_alloc (size_t align, size_t size)
static void __ESBMC_swap_elements (char *x, char *y, size_t size)
void qsort (void *base, size_t nmemb, size_t size, int(*compar)(const void *, const void *))
void * bsearch (const void *key, const void *base, size_t nmemb, size_t size, int(*compar)(const void *, const void *))
int rand (void)
long random (void)
void rev (char *p)
char * itoa (int value, char *str, int base)
void _exit (int status)

Variables

_Thread_local int errno

Macro Definition Documentation

◆ ATOI_DEF

#define ATOI_DEF ( name,
type,
TYPE )
Value:
type name(const char *s) \
{ \
__ESBMC_HIDE:; \
while (isspace(*s)) \
s++; \
int neg = 0; \
if (*s == '-') \
{ \
neg = 1; \
s++; \
} \
else if (*s == '+') \
s++; \
unsigned type r = 0; \
for (unsigned char c; (c = get_atoi_map((unsigned char)*s)); s++) \
{ \
c--; \
if (r > (TYPE##_MAX - c) / 10) \
return neg ? TYPE##_MIN : TYPE##_MAX; \
r *= 10; \
r += c; \
} \
return neg ? -r : r; \
}
isspace
int isspace(int c)
Definition ctype.c:79
TYPE
#define TYPE(pre)
Definition frexp.c:51
neg
literalt neg(literalt a)
Definition literal.h:126
get_atoi_map
static const unsigned char get_atoi_map(unsigned char pos)
Definition stdlib.c:390

◆ DIV_DEF

#define DIV_DEF ( name,
result_type,
type )
Value:
result_type name(type numerator, type denominator) \
{ \
__ESBMC_HIDE:; \
result_type result; \
result.quot = numerator / denominator; \
result.rem = numerator % denominator; \
return result; \
}

◆ STRTOF_DEF

#define STRTOF_DEF ( name,
type,
mant_dig,
max_exact_pow10 )

◆ STRTOL_DEF

#define STRTOL_DEF ( name,
type,
TYPE )

◆ STRTOUL_DEF

#define STRTOUL_DEF ( name,
type,
TYPE )
Value:
type name(const char *nptr, char **endptr, int base) \
{ \
__ESBMC_HIDE:; \
int negative; \
const char *str = __ESBMC_strto_prefix(nptr, &base, &negative); \
if (str == NULL) \
return 0; \
type result = 0; \
const char *digits = str; \
int out_of_range = 0; \
\
for (int digit; (digit = __ESBMC_strto_digit(*str)) < base; str++) \
{ \
if (result > (TYPE##_MAX - digit) / base) \
out_of_range = 1; \
else \
result = result * base + digit; \
} \
\
if (endptr != NULL) \
*endptr = (char *)(str == digits ? nptr : str); \
\
if (out_of_range) \
{ \
__ESBMC_set_errno(ERANGE); \
return TYPE##_MAX; \
} \
return negative ? (type)0 - result : result; \
}
base
static const twodig_t base
Definition bigint.cpp:28
transform.type
type
Definition transform.py:9
NULL
#define NULL
Definition pthread.h:32
__ESBMC_strto_prefix
static const char * __ESBMC_strto_prefix(const char *str, int *base, int *negative)
Definition stdlib.c:154
__ESBMC_strto_digit
static int __ESBMC_strto_digit(char c)
Definition stdlib.c:185

Typedef Documentation

◆ __ESBMC_atexit_key

typedef struct atexit_key __ESBMC_atexit_key

Function Documentation

◆ __attribute__()

__attribute__ ( (annotate( "__ESBMC_inf_size")) )

◆ __ESBMC_exact_pow10()

double __ESBMC_exact_pow10 ( int n)
static

◆ __ESBMC_no_abnormal_memory_leak()

_Bool __ESBMC_no_abnormal_memory_leak ( void )

◆ __ESBMC_set_errno()

void __ESBMC_set_errno ( int value)
static

◆ __ESBMC_strto_digit()

int __ESBMC_strto_digit ( char c)
static

◆ __ESBMC_strto_prefix()

const char * __ESBMC_strto_prefix ( const char * str,
int * base,
int * negative )
static

◆ __ESBMC_sv_comp()

_Bool __ESBMC_sv_comp ( void )

◆ __ESBMC_swap_elements()

void __ESBMC_swap_elements ( char * x,
char * y,
size_t size )
static

◆ _Exit()

void _Exit ( int status)

◆ _exit()

void _exit ( int status)

◆ abort()

void abort ( void )

◆ aligned_alloc()

void * aligned_alloc ( size_t align,
size_t size )

◆ atexit()

int atexit ( void(* func )(void))

◆ atof()

double atof ( const char * nptr)

◆ bsearch()

void * bsearch ( const void * key,
const void * base,
size_t nmemb,
size_t size,
int(* compar )(const void *, const void *) )

◆ calloc()

void * calloc ( size_t nmemb,
size_t size )

◆ exit()

void exit ( int status)

◆ get_atoi_map()

const unsigned char get_atoi_map ( unsigned char pos)
static

◆ getenv()

char * getenv ( const char * name)

◆ itoa()

char * itoa ( int value,
char * str,
int base )

◆ ldv_malloc()

void * ldv_malloc ( size_t size)

◆ ldv_zalloc()

void * ldv_zalloc ( size_t size)

◆ posix_memalign()

int posix_memalign ( void ** memptr,
size_t align,
size_t size )

◆ qsort()

void qsort ( void * base,
size_t nmemb,
size_t size,
int(* compar )(const void *, const void *) )

◆ rand()

int rand ( void )

◆ random()

long random ( void )

◆ rev()

void rev ( char * p)

◆ strlcat()

size_t strlcat ( char * dst,
const char * src,
size_t siz )

Variable Documentation

◆ errno

_Thread_local int errno
extern