CBMC: /home/runner/work/cbmc/cbmc/src/ansi-c/library/stdlib.c Source File

CBMC
Loading...
Searching...
No Matches
stdlib.c
Go to the documentation of this file.
1/* FUNCTION: abs */
2
3#ifndef __CPROVER_LIMITS_H_INCLUDED
4# include <limits.h>
5 # define __CPROVER_LIMITS_H_INCLUDED
6#endif
7
8#undef abs
9
10 int abs(int i)
11{
12 // C99 Section 7.20.6.1:
13 // "If the result cannot be represented, the behavior is undefined."
14 __CPROVER_precondition(i != INT_MIN, "argument to abs must not be INT_MIN");
15 return __CPROVER_abs(i);
16}
17
18/* FUNCTION: labs */
19
20#ifndef __CPROVER_LIMITS_H_INCLUDED
21# include <limits.h>
22# define __CPROVER_LIMITS_H_INCLUDED
23#endif
24
25#undef labs
26
27 long int labs(long int i)
28{
29 // C99 Section 7.20.6.1:
30 // "If the result cannot be represented, the behavior is undefined."
32 i != LONG_MIN, "argument to labs must not be LONG_MIN");
33 return __CPROVER_labs(i);
34}
35
36/* FUNCTION: llabs */
37
38#ifndef __CPROVER_LIMITS_H_INCLUDED
39# include <limits.h>
40# define __CPROVER_LIMITS_H_INCLUDED
41#endif
42
43#undef llabs
44
45 long long int llabs(long long int i)
46{
47 // C99 Section 7.20.6.1:
48 // "If the result cannot be represented, the behavior is undefined."
50 i != LLONG_MIN, "argument to llabs must not be LLONG_MIN");
51 return __CPROVER_llabs(i);
52}
53
54/* FUNCTION: imaxabs */
55
56#ifndef __CPROVER_INTTYPES_H_INCLUDED
57# include <inttypes.h>
58 # define __CPROVER_INTTYPES_H_INCLUDED
59#endif
60
61#ifndef __CPROVER_LIMITS_H_INCLUDED
62# include <limits.h>
63# define __CPROVER_LIMITS_H_INCLUDED
64#endif
65
66#undef imaxabs
67
68 intmax_t __CPROVER_imaxabs(intmax_t);
69
71{
73 i != INTMAX_MIN, "argument to imaxabs must not be INTMAX_MIN");
74 return __CPROVER_imaxabs(i);
75}
76
77/* FUNCTION: __builtin_abs */
78
79 int __builtin_abs(int i)
80{
81 return __CPROVER_abs(i);
82}
83
84/* FUNCTION: __builtin_labs */
85
86 long int __builtin_labs(long int i)
87{
88 return __CPROVER_labs(i);
89}
90
91/* FUNCTION: __builtin_llabs */
92
93 long long int __builtin_llabs(long long int i)
94{
95 return __CPROVER_llabs(i);
96}
97
98/* FUNCTION: exit */
99
100#undef exit
101
102 void exit(int status)
103{
104 (void)status;
106#ifdef LIBRARY_CHECK
108#endif
109}
110
111/* FUNCTION: _Exit */
112
113#undef _Exit
114
115 void _Exit(int status)
116{
117 (void)status;
119#ifdef LIBRARY_CHECK
121#endif
122}
123
124/* FUNCTION: abort */
125
126#undef abort
127
128 void abort(void)
129{
131#ifdef LIBRARY_CHECK
133#endif
134}
135
136/* FUNCTION: calloc */
137
138#undef calloc
139
140 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
141#ifndef __GNUC__
142 _Bool __builtin_mul_overflow();
143#endif
144 __CPROVER_bool __CPROVER_malloc_is_new_array;
145
147{
151 return (void *)0;
152
154 {
156 if(
159 {
160 return (void *)0;
161 }
162 }
163 else if(
166 {
168 alloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded");
170
174 "max allocation may fail");
176 }
177
178 void *malloc_res;
179 // realistically, calloc may return NULL,
180 // and __CPROVER_allocate doesn't, but no one cares
182
183 // record the object size for non-determistic bounds checking
187
188 // detect memory leaks
191
192#ifdef __CPROVER_STRING_ABSTRACTION
196#endif
197
198 return malloc_res;
199}
200
201/* FUNCTION: malloc */
202
203#undef malloc
204
205__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
206#ifndef LIBRARY_CHECK
207__CPROVER_bool __CPROVER_malloc_is_new_array;
208#endif
209
210// malloc is marked "inline" for the benefit of goto-analyzer. Really,
211// goto-analyzer should take care of inlining as needed.
213{
214// realistically, malloc may return NULL,
215// but we only do so if `--malloc-may-fail` is set
217
219 {
221 if(
224 {
225 return (void *)0;
226 }
227 }
228 else if(
231 {
233 malloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded");
235
239 "max allocation may fail");
241 }
242
243 void *malloc_res;
245
246 // record the object size for non-determistic bounds checking
250
251 // detect memory leaks
254
255#ifdef __CPROVER_STRING_ABSTRACTION
257#endif
258
259 return malloc_res;
260}
261
262/* FUNCTION: __builtin_alloca */
263
264__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
265 const void *__CPROVER_alloca_object;
266#ifndef LIBRARY_CHECK
267__CPROVER_bool __CPROVER_malloc_is_new_array;
268#endif
269
271{
273 void *res;
275
276 // record the object size for non-determistic bounds checking
279
280 // record alloca to detect invalid free
283
284#ifdef __CPROVER_STRING_ABSTRACTION
286#endif
287
288 return res;
289}
290
291/* FUNCTION: alloca */
292
293#undef alloca
294
295void *__builtin_alloca(__CPROVER_size_t alloca_size);
296
302
303/* FUNCTION: free */
304
305#undef free
306
307void __CPROVER_deallocate(void *);
308__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
309#ifndef LIBRARY_CHECK
310const void *__CPROVER_alloca_object;
311#endif
312 const void *__CPROVER_new_object;
313#ifndef LIBRARY_CHECK
314__CPROVER_bool __CPROVER_malloc_is_new_array;
315#endif
316
317 void free(void *ptr)
318{
320 // If ptr is NULL, no operation is performed.
322 ptr == 0 || __CPROVER_r_ok(ptr, 0),
323 "free argument must be NULL or valid pointer");
325 "free argument must be dynamic object");
327 "free argument has offset zero");
328
329 // catch double free
331 "double free");
332
333 // catch people who try to use free(...) for stuff
334 // allocated with new[]
337 "free called for new[] object");
338
339 // catch people who try to use free(...) with alloca
341 ptr == 0 || __CPROVER_alloca_object != ptr,
342 "free called for stack-allocated object");
343
344 if(ptr!=0)
345 {
347
348 // detect memory leaks
349 if(__CPROVER_memory_leak==ptr)
351 }
352}
353
354/* FUNCTION: strtol */
355
356#ifndef __CPROVER_ERRNO_H_INCLUDED
357#include <errno.h>
358 #define __CPROVER_ERRNO_H_INCLUDED
359#endif
360
361#ifndef __CPROVER_LIMITS_H_INCLUDED
362#include <limits.h>
363#define __CPROVER_LIMITS_H_INCLUDED
364#endif
365
366#undef strtol
367#undef isdigit
368#undef isspace
369
370int isspace(int);
371int isdigit(int);
372
373#ifndef __GNUC__
374 _Bool __builtin_add_overflow();
375_Bool __builtin_mul_overflow();
376#endif
377
378 long strtol(const char *nptr, char **endptr, int base)
379{
381 #ifdef __CPROVER_STRING_ABSTRACTION
383 "zero-termination of argument of strtol");
384 #endif
385
386 if(base==1 || base<0 || base>36)
387 {
389 return 0;
390 }
391
392 long res=0;
394 char sign=0;
395
396 // 32 chars is an arbitrarily chosen limit
397 int i=0;
398 for( ; i<31; ++i)
399 {
400 char ch=nptr[i];
401 char sub=0;
402 if(ch==0)
403 break;
404 else if((base==0 || base==16) && !in_number &&
405 ch=='0' && (nptr[i+1]=='x' || nptr[i+1]=='X'))
406 {
407 base=16;
408 in_number=1;
409 ++i;
410 continue;
411 }
412 else if(base==0 && !in_number && ch=='0')
413 {
414 base=8;
415 in_number=1;
416 continue;
417 }
418 else if(!in_number && !sign && isspace(ch))
419 continue;
420 else if(!in_number && !sign && (ch=='-' || ch=='+'))
421 {
422 sign=ch;
423 continue;
424 }
425 else if(base>10 && ch>='a' && ch-'a'<base-10)
426 sub='a'-10;
427 else if(base>10 && ch>='A' && ch-'A'<base-10)
428 sub='A'-10;
429 else if(isdigit(ch))
430 {
431 sub='0';
432 base=base==0 ? 10 : base;
433 }
434 else
435 break;
436
437 in_number=1;
439 if(overflow || __builtin_add_overflow(res, (long)(ch - sub), &res))
440 {
442 if(sign=='-')
443 return LONG_MIN;
444 else
445 return LONG_MAX;
446 }
447 }
448
449 if(endptr!=0)
450 *endptr=(char*)nptr+i;
451
452 if(sign=='-')
453 res*=-1;
454
455 return res;
456}
457
458/* FUNCTION: atoi */
459
460#undef atoi
461#undef strtol
462
463long strtol(const char *nptr, char **endptr, int base);
464
465 int atoi(const char *nptr)
466{
468 return (int)strtol(nptr, (char **)0, 10);
469}
470
471/* FUNCTION: atol */
472
473#undef atol
474#undef strtol
475
476long strtol(const char *nptr, char **endptr, int base);
477
478 long atol(const char *nptr)
479{
481 return strtol(nptr, (char **)0, 10);
482}
483
484/* FUNCTION: getenv */
485
486#undef getenv
487
488#ifndef __CPROVER_STDDEF_H_INCLUDED
489# include <stddef.h>
490 # define __CPROVER_STDDEF_H_INCLUDED
491#endif
492
493__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
494 ptrdiff_t __VERIFIER_nondet_ptrdiff_t(void);
495
496 char *getenv(const char *name)
497{
499
500 (void)*name;
501 #ifdef __CPROVER_STRING_ABSTRACTION
503 "zero-termination of argument of getenv");
504 #endif
505
506#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
507 __CPROVER_event("invalidate_pointer", "getenv_result");
508 char *getenv_result;
509 __CPROVER_set_must(getenv_result, "getenv_result");
510 return getenv_result;
511
512#else
513
515 if(!found) return 0;
516
518
519 // It's reasonable to assume this won't exceed the signed
520 // range in practice, but in principle, this could exceed
521 // the range.
522
524 char *buffer = (char *)__CPROVER_allocate(buf_size * sizeof(char), 0);
525 buffer[buf_size-1]=0;
526
527# ifdef __CPROVER_STRING_ABSTRACTION
531# endif
532
533 return buffer;
534#endif
535}
536
537/* FUNCTION: realloc */
538
539void *malloc(__CPROVER_size_t malloc_size);
540void free(void *ptr);
541
543{
545
547 "realloc argument is dynamic object");
548
549 // if ptr is NULL, this behaves like malloc
550 if(ptr==0)
551 return malloc(malloc_size);
552
553 // if malloc-size is 0, allocate new minimum sized object
554 // and free original
555 if(malloc_size==0)
556 {
557 free(ptr);
558 return malloc(0);
559 }
560
561 // this shouldn't move if the new size isn't bigger
562 void *res;
564 if(res != (void *)0)
565 {
567 free(ptr);
568 }
569
570 return res;
571}
572
573/* FUNCTION: valloc */
574
575void *malloc(__CPROVER_size_t malloc_size);
576
578{
579 // The allocated memory is aligned on a page
580 // boundary, which we don't model.
581
583 return malloc(malloc_size);
584}
585
586/* FUNCTION: posix_memalign */
587
588#ifndef __CPROVER_ERRNO_H_INCLUDED
589#include <errno.h>
590#define __CPROVER_ERRNO_H_INCLUDED
591#endif
592
593#undef posix_memalign
594
595void *malloc(__CPROVER_size_t malloc_size);
597 void **ptr,
599 __CPROVER_size_t size)
600{
602
603 __CPROVER_size_t multiplier = alignment / sizeof(void *);
604 // Modeling the posix_memalign checks on alignment.
605 if(
606 alignment % sizeof(void *) != 0 || ((multiplier) & (multiplier - 1)) != 0 ||
607 alignment == 0)
608 {
609 return EINVAL;
610 }
611 // The address of the allocated memory is supposed to be aligned with
612 // alignment. As cbmc doesn't model address alignment,
613 // assuming MALLOC_ALIGNMENT = MAX_INT_VALUE seems fair.
614 // As _mid_memalign simplifies for alignment <= MALLOC_ALIGNMENT
615 // to a malloc call, it should be sound, if we do it too.
616
617 void *tmp = malloc(size);
618 if(tmp != (void *)0)
619 {
620 *ptr = tmp;
621 return 0;
622 }
623 return ENOMEM;
624}
625
626/* FUNCTION: random */
627
628 long __VERIFIER_nondet_long(void);
629
630 long random(void)
631{
632 // We return a non-deterministic value instead of a random one.
634 long result=__VERIFIER_nondet_long();
635 __CPROVER_assume(result>=0 && result<=2147483647);
636 return result;
637}
638
639/* FUNCTION: rand */
640
641 int __VERIFIER_nondet_int(void);
642
643 int rand(void)
644{
646 // We return a non-deterministic value instead of a random one.
647 int result = __VERIFIER_nondet_int();
648 __CPROVER_assume(result >= 0);
649 return result;
650}
651
652/* FUNCTION: rand_r */
653
654int __VERIFIER_nondet_int(void);
655
656 int rand_r(unsigned int *seed)
657{
659 // We return a non-deterministic value instead of a random one.
660 (void)*seed;
661 int result = __VERIFIER_nondet_int();
662 __CPROVER_assume(result >= 0);
663 return result;
664}
665
666/* FUNCTION: __CPROVER_deallocate */
667
668__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
669
__CPROVER_thread_local __CPROVER_size_t __CPROVER_max_malloc_size
int __CPROVER_malloc_failure_mode
int __CPROVER_malloc_failure_mode_return_null
void * __CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero)
const void * __CPROVER_deallocated
const void * __CPROVER_memory_leak
__CPROVER_bool __CPROVER_malloc_may_fail
int __CPROVER_malloc_failure_mode_assert_then_assume
__CPROVER_bool __CPROVER_r_ok(const void *,...)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
__CPROVER_size_t __CPROVER_buffer_size(const void *)
void __CPROVER_assert(__CPROVER_bool assertion, const char *description)
long int __CPROVER_labs(long int x)
__CPROVER_size_t __CPROVER_POINTER_OFFSET(const void *)
__CPROVER_size_t __CPROVER_zero_string_length(const void *)
int __CPROVER_abs(int x)
void __CPROVER_precondition(__CPROVER_bool precondition, const char *description)
long long int __CPROVER_llabs(long long int x)
_Bool __CPROVER_is_zero_string(const void *)
void __CPROVER_set_must(const void *, const char *)
__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *)
void __CPROVER_assume(__CPROVER_bool assumption)
void __CPROVER_array_copy(const void *dest, const void *src)
void __builtin_unreachable(void)
mp_integer alignment(const typet &type, const namespacet &ns)
Definition padding.cpp:23
int __VERIFIER_nondet_int(void)
long random(void)
Definition stdlib.c:630
void * alloca(__CPROVER_size_t alloca_size)
Definition stdlib.c:297
long atol(const char *nptr)
Definition stdlib.c:478
_Bool __builtin_mul_overflow()
long int labs(long int i)
Definition stdlib.c:27
int posix_memalign(void **ptr, __CPROVER_size_t alignment, __CPROVER_size_t size)
Definition stdlib.c:596
long strtol(const char *nptr, char **endptr, int base)
Definition stdlib.c:378
int rand_r(unsigned int *seed)
Definition stdlib.c:656
intmax_t __CPROVER_imaxabs(intmax_t)
void * malloc(__CPROVER_size_t malloc_size)
Definition stdlib.c:212
void exit(int status)
Definition stdlib.c:102
long int __builtin_labs(long int i)
Definition stdlib.c:86
void __CPROVER_deallocate(void *)
Definition stdlib.c:670
void * valloc(__CPROVER_size_t malloc_size)
Definition stdlib.c:577
const void * __CPROVER_new_object
Definition stdlib.c:312
int isdigit(int)
Definition ctype.c:24
void _Exit(int status)
Definition stdlib.c:115
void * calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
Definition stdlib.c:146
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void)
void abort(void)
Definition stdlib.c:128
void * __builtin_alloca(__CPROVER_size_t alloca_size)
Definition stdlib.c:270
intmax_t imaxabs(intmax_t i)
Definition stdlib.c:70
int isspace(int)
Definition ctype.c:80
_Bool __builtin_add_overflow()
long long int llabs(long long int i)
Definition stdlib.c:45
int __builtin_abs(int i)
Definition stdlib.c:79
char * getenv(const char *name)
Definition stdlib.c:496
const void * __CPROVER_alloca_object
Definition stdlib.c:265
long long int __builtin_llabs(long long int i)
Definition stdlib.c:93
__CPROVER_bool __CPROVER_malloc_is_new_array
Definition stdlib.c:144
ptrdiff_t __VERIFIER_nondet_ptrdiff_t(void)
int atoi(const char *nptr)
Definition stdlib.c:465
int rand(void)
Definition stdlib.c:643
void * realloc(void *ptr, __CPROVER_size_t malloc_size)
Definition stdlib.c:542
int abs(int i)
Definition stdlib.c:10
void free(void *ptr)
Definition stdlib.c:317
long __VERIFIER_nondet_long(void)

AltStyle によって変換されたページ (->オリジナル) /