pre-conditions for strings

Author: Daniel Kroening

src/ansi-c/library/inet.c

@@ -12,10 +12,11 @@ in_addr_t __VERIFIER_nondet_in_addr_t();
 in_addr_t inet_addr(const char *cp)
 {
   __CPROVER_HIDE:;
-  (void)*cp;
   #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_addr zero-termination of argument");
+  __CPROVER_precondition(__CPROVER_is_zero_string(cp),
+                         "inet_addr zero-termination of argument");
   #endif
+  (void)*cp;
 
   in_addr_t result=__VERIFIER_nondet_in_addr_t();
   return result;
@@ -37,11 +38,12 @@ int __VERIFIER_nondet_int();
 int inet_aton(const char *cp, struct in_addr *pin)
 {
   __CPROVER_HIDE:;
-  (void)*cp;
-  (void)*pin;
   #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_aton zero-termination of name argument");
+  __CPROVER_precondition(__CPROVER_is_zero_string(cp),
+                         "inet_aton zero-termination of name argument");
   #endif
+  (void)*cp;
+  (void)*pin;
 
   int result=__VERIFIER_nondet_int();
   return result;
@@ -63,10 +65,11 @@ in_addr_t __VERIFIER_nondet_in_addr_t();
 in_addr_t inet_network(const char *cp)
 {
   __CPROVER_HIDE:;
-  (void)*cp;
   #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_network zero-termination of name argument");
+  __CPROVER_precondition(__CPROVER_is_zero_string(cp),
+                         "inet_network zero-termination of name argument");
   #endif
+  (void)*cp;
 
   in_addr_t result=__VERIFIER_nondet_in_addr_t();
   return result;

src/ansi-c/library/netdb.c

@@ -7,10 +7,11 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 struct hostent *gethostbyname(const char *name)
 {
   __CPROVER_HIDE:;
-  (void)*name;
   #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_assert(__CPROVER_is_zero_string(name), "gethostbyname zero-termination of name argument");
+  __CPROVER_precondition(__CPROVER_is_zero_string(name),
+                         "gethostbyname zero-termination of name argument");
   #endif
+  (void)*name;
 
   __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
   if(error) return 0;