Merge pull request sosy-lab#1256 from Eiram/master

Avoid uninitialized variable usage in c/bitvector/s3_clnt_?.BV.c.cil-2a.c
tautschnig · Dec 3, 2020 · 5f7451b · 5f7451b
2 parents a4bf122 + 848529b
commit 5f7451b
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 15 deletions.
diff --git a/c/bitvector/s3_clnt_1.BV.c.cil-2a.c b/c/bitvector/s3_clnt_1.BV.c.cil-2a.c
@@ -20,16 +20,16 @@ int ssl3_connect(void)
   int s__wbio  = __VERIFIER_nondet_int();
   int s__hit  = __VERIFIER_nondet_int();
   int s__rwstate ;
-  int s__init_buf___0 ;
+  int s__init_buf___0  = __VERIFIER_nondet_int();
   int s__debug  = __VERIFIER_nondet_int();
   int s__shutdown ;
   int s__ctx__info_callback  = __VERIFIER_nondet_int();
-  unsigned int s__ctx__stats__sess_connect_renegotiate ;
-  unsigned int s__ctx__stats__sess_connect ;
+  unsigned int s__ctx__stats__sess_connect_renegotiate = __VERIFIER_nondet_uint();
+  unsigned int s__ctx__stats__sess_connect  = __VERIFIER_nondet_uint();
   int s__ctx__stats__sess_hit  = __VERIFIER_nondet_int();
   int s__ctx__stats__sess_connect_good  = __VERIFIER_nondet_int();
   int s__s3__change_cipher_spec ;
-  int s__s3__flags ;
+  int s__s3__flags = __VERIFIER_nondet_int();
   int s__s3__delay_buf_pop_ret ;
   int s__s3__tmp__cert_req  = __VERIFIER_nondet_int();
   int s__s3__tmp__new_compression  = __VERIFIER_nondet_int();
@@ -43,7 +43,7 @@ int ssl3_connect(void)
   int buf ;
   unsigned long tmp ;
   unsigned long l ;
-  int num1 ;
+  int num1 = __VERIFIER_nondet_int();
   int cb ;
   int ret ;
   int new_state ;

diff --git a/c/bitvector/s3_clnt_2.BV.c.cil-2a.c b/c/bitvector/s3_clnt_2.BV.c.cil-2a.c
@@ -20,16 +20,16 @@ int ssl3_connect(void)
   int s__wbio  = __VERIFIER_nondet_int();
   int s__hit  = __VERIFIER_nondet_int();
   int s__rwstate ;
-  int s__init_buf___0 ;
+  int s__init_buf___0 = __VERIFIER_nondet_int();
   int s__debug  = __VERIFIER_nondet_int();
   int s__shutdown ;
   int s__ctx__info_callback  = __VERIFIER_nondet_int();
-  unsigned int s__ctx__stats__sess_connect_renegotiate ;
-  unsigned int s__ctx__stats__sess_connect ;
+  unsigned int s__ctx__stats__sess_connect_renegotiate = __VERIFIER_nondet_uint();
+  unsigned int s__ctx__stats__sess_connect = __VERIFIER_nondet_uint();
   unsigned int s__ctx__stats__sess_hit  = __VERIFIER_nondet_uint();
   unsigned int s__ctx__stats__sess_connect_good  = __VERIFIER_nondet_uint();
   int s__s3__change_cipher_spec ;
-  int s__s3__flags ;
+  int s__s3__flags = __VERIFIER_nondet_int();
   int s__s3__delay_buf_pop_ret ;
   int s__s3__tmp__cert_req  = __VERIFIER_nondet_int();
   int s__s3__tmp__new_compression  = __VERIFIER_nondet_int();
@@ -43,7 +43,7 @@ int ssl3_connect(void)
   int buf ;
   unsigned long tmp ;
   unsigned long l ;
-  int num1 ;
+  int num1 = __VERIFIER_nondet_int();
   int cb ;
   int ret ;
   int new_state ;

diff --git a/c/bitvector/s3_clnt_3.BV.c.cil-2a.c b/c/bitvector/s3_clnt_3.BV.c.cil-2a.c
@@ -20,16 +20,16 @@ int ssl3_connect(void)
   int s__wbio  = __VERIFIER_nondet_int();
   int s__hit  = __VERIFIER_nondet_int();
   int s__rwstate ;
-  int s__init_buf___0 ;
+  int s__init_buf___0 = __VERIFIER_nondet_int();
   int s__debug  = __VERIFIER_nondet_int();
   int s__shutdown ;
   int s__ctx__info_callback  = __VERIFIER_nondet_int();
-  unsigned int s__ctx__stats__sess_connect_renegotiate ;
-  unsigned int s__ctx__stats__sess_connect ;
+  unsigned int s__ctx__stats__sess_connect_renegotiate = __VERIFIER_nondet_uint();
+  unsigned int s__ctx__stats__sess_connect = __VERIFIER_nondet_uint();
   unsigned int s__ctx__stats__sess_hit  = __VERIFIER_nondet_uint();
   unsigned int s__ctx__stats__sess_connect_good  = __VERIFIER_nondet_uint();
   int s__s3__change_cipher_spec ;
-  int s__s3__flags ;
+  int s__s3__flags = __VERIFIER_nondet_int();
   int s__s3__delay_buf_pop_ret ;
   int s__s3__tmp__cert_req  = __VERIFIER_nondet_int();
   int s__s3__tmp__new_compression  = __VERIFIER_nondet_int();
@@ -43,7 +43,7 @@ int ssl3_connect(void)
   int buf ;
   unsigned long tmp ;
   unsigned long l ;
-  int num1 ;
+  int num1 = __VERIFIER_nondet_int();
   int cb ;
   int ret ;
   int new_state ;