From cd8d49480afe13b2f2eeb7fa30705cd5be119080 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 24 Sep 2017 12:27:05 +0100 Subject: [PATCH] added __builtin_memset --- src/ansi-c/library/string.c | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c index 0dabca6ebc5..9145059ff0f 100644 --- a/src/ansi-c/library/string.c +++ b/src/ansi-c/library/string.c @@ -607,6 +607,36 @@ void *memset(void *s, int c, size_t n) return s; } +/* FUNCTION: __builtin_memset */ + +void *__builtin_memset(void *s, int c, __CPROVER_size_t n) +{ + __CPROVER_HIDE:; + #ifdef __CPROVER_STRING_ABSTRACTION + __CPROVER_assert(__CPROVER_buffer_size(s)>=n, "memset buffer overflow"); + // for(size_t i=0; i __CPROVER_zero_string_length(s)) + { + __CPROVER_is_zero_string(s)=1; + } + else if(c==0) + { + __CPROVER_is_zero_string(s)=1; + __CPROVER_zero_string_length(s)=0; + } + else + __CPROVER_is_zero_string(s)=0; + #else + //char *sp=s; + //for(__CPROVER_size_t i=0; i