Skip to content

Commit 7c3239b

Browse files
author
Daniel Kroening
authored
Merge pull request diffblue#1417 from diffblue/builtin_memset
added __builtin_memset
2 parents 368bb27 + cd8d494 commit 7c3239b

File tree

1 file changed

+30
-0
lines changed

1 file changed

+30
-0
lines changed

src/ansi-c/library/string.c

+30
Original file line numberDiff line numberDiff line change
@@ -607,6 +607,36 @@ void *memset(void *s, int c, size_t n)
607607
return s;
608608
}
609609

610+
/* FUNCTION: __builtin_memset */
611+
612+
void *__builtin_memset(void *s, int c, __CPROVER_size_t n)
613+
{
614+
__CPROVER_HIDE:;
615+
#ifdef __CPROVER_STRING_ABSTRACTION
616+
__CPROVER_assert(__CPROVER_buffer_size(s)>=n, "memset buffer overflow");
617+
// for(size_t i=0; i<n ; i++) s[i]=c;
618+
if(__CPROVER_is_zero_string(s) &&
619+
n > __CPROVER_zero_string_length(s))
620+
{
621+
__CPROVER_is_zero_string(s)=1;
622+
}
623+
else if(c==0)
624+
{
625+
__CPROVER_is_zero_string(s)=1;
626+
__CPROVER_zero_string_length(s)=0;
627+
}
628+
else
629+
__CPROVER_is_zero_string(s)=0;
630+
#else
631+
//char *sp=s;
632+
//for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
633+
unsigned char s_n[n];
634+
__CPROVER_array_set(s_n, (unsigned char)c);
635+
__CPROVER_array_replace((unsigned char*)s, s_n);
636+
#endif
637+
return s;
638+
}
639+
610640
/* FUNCTION: __builtin___memset_chk */
611641

612642
void *__builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_t size)

0 commit comments

Comments
 (0)