Skip to content
This repository has been archived by the owner on Oct 3, 2021. It is now read-only.

Fix Problems with Benchmark Set #1279

Merged
merged 4 commits into from
Dec 19, 2020
Merged

Fix Problems with Benchmark Set #1279

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e24e405
adapt property file coverage-error-call not appropriate when verdict …
Eiram Dec 14, 2020
b46a294
fixed uninitailized variable usage
Eiram Dec 14, 2020
380f939
fixed uninitialized variable usages in OpenSSL tasks
Eiram Dec 14, 2020
a5ecd87
uninitialized some variables to avoid that they are used uninitialized
Eiram Dec 14, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion c/ldv-regression/rule57_ebda_blast.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions c/ldv-regression/test28-1.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down
11 changes: 11 additions & 0 deletions c/loops/s3.i
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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);
Expand Down
12 changes: 12 additions & 0 deletions c/openssl/s3_clnt.blast.01.i.cil-1.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here wbio and bbio are used to be compared against themselves on line 1303 but no action is taken based on the result (the body of if-else is empty). Wouldn't it be easier just to remove the whole comparison on line 1303?

(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);
Expand Down
12 changes: 12 additions & 0 deletions c/openssl/s3_clnt.blast.01.i.cil-2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
12 changes: 12 additions & 0 deletions c/openssl/s3_clnt.blast.02.i.cil-1.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
12 changes: 12 additions & 0 deletions c/openssl/s3_clnt.blast.02.i.cil-2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
12 changes: 12 additions & 0 deletions c/openssl/s3_clnt.blast.03.i.cil-1.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
12 changes: 12 additions & 0 deletions c/openssl/s3_clnt.blast.03.i.cil-2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
12 changes: 12 additions & 0 deletions c/openssl/s3_clnt.blast.04.i.cil-1.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
12 changes: 12 additions & 0 deletions c/openssl/s3_clnt.blast.04.i.cil-2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
19 changes: 19 additions & 0 deletions c/openssl/s3_srvr.blast.01.i.cil-1.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was puzzled by this initialization, but info_callback is only compared to 0, so this should actually work fine.

s->options = __VERIFIER_nondet_ulong();
s->verify_mode = __VERIFIER_nondet_int();
(s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The same here, peer is agian used only in comparisions to 0. I wonder whether it wouldn't be better just to replace the comparisions with __VERIFIER_nondet_bool?

(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);
Expand Down
19 changes: 19 additions & 0 deletions c/openssl/s3_srvr.blast.01.i.cil-2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
19 changes: 19 additions & 0 deletions c/openssl/s3_srvr.blast.02.i.cil-1.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
19 changes: 19 additions & 0 deletions c/openssl/s3_srvr.blast.02.i.cil-2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
19 changes: 19 additions & 0 deletions c/openssl/s3_srvr.blast.03.i.cil.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
19 changes: 19 additions & 0 deletions c/openssl/s3_srvr.blast.04.i.cil.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
19 changes: 19 additions & 0 deletions c/openssl/s3_srvr.blast.06.i.cil-1.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
Loading