Fix Problems with Benchmark Set #1279
Conversation
dbeyer
changed the title
|
Changed title because this applies also to SV-COMP. |
|
This PR is also interesting for the verification community. Maybe related to issue #1270. |
| 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(); |
There was a problem hiding this comment.
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?
| @@ -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(); | |||
There was a problem hiding this comment.
I was puzzled by this initialization, but info_callback is only compared to 0, so this should actually work fine.
| (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(); |
There was a problem hiding this comment.
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?
Removed property coverage-error from one property file because it is no longer appropriate and
initialize variables mainly in openssl tasks to avoid that they are used uniitialized, which causes problems with test case validation.