clean-out ill-modeled optimization in string comparisons

Author: Daniel Kroening

src/ansi-c/library/string.c

@@ -298,12 +298,6 @@ inline char *strncat(char *dst, const char *src, size_t n)
 inline int strcmp(const char *s1, const char *s2)
 {
   __CPROVER_HIDE:;
-  #if !defined(__linux__) || defined(__GLIBC__)
-  if(s1!=0 && s1==s2) return 0;
-  #else
-  // musl guarantees non-null of s1
-  if(s1==s2) return 0;
-  #endif
   #ifdef __CPROVER_STRING_ABSTRACTION
   int retval;
   __CPROVER_assert(__CPROVER_is_zero_string(s1), "strcmp zero-termination of 1st argument");
@@ -345,12 +339,6 @@ inline int strcmp(const char *s1, const char *s2)
 inline int strcasecmp(const char *s1, const char *s2)
 {
   __CPROVER_HIDE:;
-  #if !defined(__linux__) || defined(__GLIBC__)
-  if(s1!=0 && s1==s2) return 0;
-  #else
-  // musl guarantees non-null of s1
-  if(s1==s2) return 0;
-  #endif
   #ifdef __CPROVER_STRING_ABSTRACTION
   int retval;
   __CPROVER_assert(__CPROVER_is_zero_string(s1), "strcasecmp zero-termination of 1st argument");
@@ -395,12 +383,6 @@ inline int strcasecmp(const char *s1, const char *s2)
 inline int strncmp(const char *s1, const char *s2, size_t n)
 {
   __CPROVER_HIDE:;
-  #if !defined(__linux__) || defined(__GLIBC__)
-  if(s1!=0 && s1==s2) return 0;
-  #else
-  // musl guarantees non-null of s1
-  if(s1==s2) return 0;
-  #endif
   #ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_assert(__CPROVER_is_zero_string(s1) || __CPROVER_buffer_size(s1)>=n, "strncmp zero-termination of 1st argument");
   __CPROVER_assert(__CPROVER_is_zero_string(s2) || __CPROVER_buffer_size(s2)>=n, "strncmp zero-termination of 2nd argument");
@@ -439,12 +421,6 @@ inline int strncmp(const char *s1, const char *s2, size_t n)
 inline int strncasecmp(const char *s1, const char *s2, size_t n)
 {
   __CPROVER_HIDE:;
-  #if !defined(__linux__) || defined(__GLIBC__)
-  if(s1!=0 && s1==s2) return 0;
-  #else
-  // musl guarantees non-null of s1
-  if(s1==s2) return 0;
-  #endif
   #ifdef __CPROVER_STRING_ABSTRACTION
   int retval;
   __CPROVER_assert(__CPROVER_is_zero_string(s1), "strncasecmp zero-termination of 1st argument");