pre-conditions for strings

diffblue · Feb 14, 2018 · 9ea0cc6 · 9ea0cc6
1 parent c94548c
commit 9ea0cc6
Show file tree

Hide file tree

Showing 5 changed files with 149 additions and 78 deletions.
diff --git a/regression/cbmc/strcat1/test.desc b/regression/cbmc/strcat1/test.desc
@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 \[main.assertion.6\] assertion strlen\(A3\) == 4: FAILURE
-\*\* 1 of 8 failed
+\*\* 1 of 9 failed
 --
 ^warning: ignoring
diff --git a/src/ansi-c/library/inet.c b/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;

diff --git a/src/ansi-c/library/netdb.c b/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;