Merge pull request #1279 from Eiram/master

Fix Problems with Benchmark Set

c/ldv-regression/rule57_ebda_blast.yml

@@ -12,7 +12,6 @@ properties:
   - property_file: ../properties/coverage-branches.prp
   - property_file: ../properties/coverage-conditions.prp
   - property_file: ../properties/coverage-statements.prp
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

c/ldv-regression/test28-1.c

@@ -16,6 +16,7 @@ int main()
   struct dummy *pd = n ? &d1 : &d2;
   if (pd == &d2) {
     pd->a = 0;
+    pd->b = __VERIFIER_nondet_int();
   } else {
     pd->b = 0;
   }

c/loops/s3.i

@@ -8,6 +8,7 @@ extern void *malloc(unsigned int sz);
 
 extern int __VERIFIER_nondet_int(void);
 extern unsigned long __VERIFIER_nondet_ulong(void);
+extern  long __VERIFIER_nondet_long(void);
 
 typedef unsigned int size_t;
 typedef long __time_t;
@@ -1067,9 +1068,19 @@ int main(void)
   {
   s = malloc (sizeof (SSL));
   s->s3 = malloc(sizeof(struct ssl3_state_st));
+  s->s3->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  s->s3->tmp.next_state = __VERIFIER_nondet_int();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
   s->ctx = malloc(sizeof(SSL_CTX));
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong();
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->info_callback = (void (*)()) __VERIFIER_nondet_ulong();
   ssl3_connect(s);
   }
   return (0);

c/openssl/s3_clnt.blast.01.i.cil-1.c

@@ -1073,6 +1073,18 @@ int main(void)
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+
+	s->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
+  (s->s3)->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.next_state = __VERIFIER_nondet_int();
+
   ssl3_connect(s);
   }
   return (0);

c/openssl/s3_clnt.blast.01.i.cil-2.c

@@ -1073,6 +1073,18 @@ int main(void)
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+
+	s->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
+  (s->s3)->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.next_state = __VERIFIER_nondet_int();
+
   ssl3_connect(s);
   }
   return (0);

c/openssl/s3_clnt.blast.02.i.cil-1.c

@@ -1073,6 +1073,18 @@ int main(void)
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+
+	s->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
+  (s->s3)->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.next_state = __VERIFIER_nondet_int();
+
   ssl3_connect(s);
   }
   return (0);

c/openssl/s3_clnt.blast.02.i.cil-2.c

@@ -1074,6 +1074,18 @@ int main(void)
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+
+	s->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
+  (s->s3)->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.next_state = __VERIFIER_nondet_int();
+
   ssl3_connect(s);
   }
   return (0);

c/openssl/s3_clnt.blast.03.i.cil-1.c

@@ -1073,6 +1073,18 @@ int main(void)
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+
+	s->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
+  (s->s3)->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.next_state = __VERIFIER_nondet_int();
+
   ssl3_connect(s);
   }
   return (0);

c/openssl/s3_clnt.blast.03.i.cil-2.c

@@ -1073,6 +1073,18 @@ int main(void)
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+
+	s->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
+  (s->s3)->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.next_state = __VERIFIER_nondet_int();
+
   ssl3_connect(s);
   }
   return (0);

c/openssl/s3_clnt.blast.04.i.cil-1.c

@@ -1073,6 +1073,18 @@ int main(void)
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+
+	s->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
+  (s->s3)->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.next_state = __VERIFIER_nondet_int();
+
   ssl3_connect(s);
   }
   return (0);

c/openssl/s3_clnt.blast.04.i.cil-2.c

@@ -1073,6 +1073,18 @@ int main(void)
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+
+	s->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
+  (s->s3)->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.next_state = __VERIFIER_nondet_int();
+
   ssl3_connect(s);
   }
   return (0);

c/openssl/s3_srvr.blast.01.i.cil-1.c

@@ -1074,6 +1074,25 @@ int main(void)
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 8464;
+
+	s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);

c/openssl/s3_srvr.blast.01.i.cil-2.c

@@ -1074,6 +1074,25 @@ int main(void)
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 8464;
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);

c/openssl/s3_srvr.blast.02.i.cil-1.c

@@ -1074,6 +1074,25 @@ int main(void)
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 8464;
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);

c/openssl/s3_srvr.blast.02.i.cil-2.c

@@ -1074,6 +1074,25 @@ int main(void)
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 8464;
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);

c/openssl/s3_srvr.blast.03.i.cil.c

@@ -1074,6 +1074,25 @@ int main(void)
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 8464;
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);

c/openssl/s3_srvr.blast.04.i.cil.c

@@ -1074,6 +1074,25 @@ int main(void)
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 8464;
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);

c/openssl/s3_srvr.blast.06.i.cil-1.c

@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);