Skip to content

Commit 91aef54

Browse files
committed
Do not inline functions using arrays of symbolic size
Multiple uses of the same library function might cause phi nodes merging arrays of different size, when really their objects have actually gone out of scope.
1 parent af73aec commit 91aef54

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed

src/ansi-c/library/string.c

+4-4
Original file line numberDiff line numberDiff line change
@@ -516,7 +516,7 @@ inline char *strdup(const char *str)
516516

517517
#undef memcpy
518518

519-
inline void *memcpy(void *dst, const void *src, size_t n)
519+
void *memcpy(void *dst, const void *src, size_t n)
520520
{
521521
__CPROVER_HIDE:
522522
#ifdef __CPROVER_STRING_ABSTRACTION
@@ -583,7 +583,7 @@ void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __C
583583

584584
#undef memset
585585

586-
inline void *memset(void *s, int c, size_t n)
586+
void *memset(void *s, int c, size_t n)
587587
{
588588
__CPROVER_HIDE:;
589589
#ifdef __CPROVER_STRING_ABSTRACTION
@@ -652,7 +652,7 @@ void *__builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_
652652

653653
#undef memmove
654654

655-
inline void *memmove(void *dest, const void *src, size_t n)
655+
void *memmove(void *dest, const void *src, size_t n)
656656
{
657657
__CPROVER_HIDE:;
658658
#ifdef __CPROVER_STRING_ABSTRACTION
@@ -683,7 +683,7 @@ inline void *memmove(void *dest, const void *src, size_t n)
683683

684684
#undef memmove
685685

686-
inline void *__builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_size_t size)
686+
void *__builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_size_t size)
687687
{
688688
__CPROVER_HIDE:;
689689
#ifdef __CPROVER_STRING_ABSTRACTION

0 commit comments

Comments
 (0)