../svcomp15/ssh-simplified/s3_clnt_1_false-unreach-call.cil.c path false false false false C true int s ; 758 36978 s = 12292; 763 37007 s == (12292); main ssl3_connect(12292); 765 37030 ssl3_connect int s__info_callback = __VERIFIER_nondet_int() ; 13 403 int s__in_handshake = __VERIFIER_nondet_int() ; 14 454 s__info_callback == (0); ssl3_connect int s__in_handshake = __VERIFIER_nondet_int() ; 14 476 s__in_handshake == (9); ssl3_connect int s__state ; 15 504 int s__new_session ; 16 521 int s__server ; 17 544 int s__version = __VERIFIER_nondet_int() ; 18 562 int s__type ; 19 607 s__version == (66048); ssl3_connect int s__init_num ; 20 623 int s__bbio = __VERIFIER_nondet_int() ; 21 643 int s__bbio = __VERIFIER_nondet_int() ; 21 657 s__bbio == (11); ssl3_connect int s__wbio = __VERIFIER_nondet_int() ; 22 685 int s__wbio = __VERIFIER_nondet_int() ; 22 697 s__wbio == (12); ssl3_connect int s__hit = __VERIFIER_nondet_int() ; 23 727 int s__hit = __VERIFIER_nondet_int() ; 23 740 s__hit == (0); ssl3_connect int s__rwstate ; 24 768 int s__init_buf___0 ; 25 787 s__init_buf___0 == (0); ssl3_connect int s__debug = __VERIFIER_nondet_int() ; 26 811 int s__debug = __VERIFIER_nondet_int() ; 26 824 s__debug == (13); ssl3_connect int s__shutdown ; 27 854 int s__ctx__info_callback = __VERIFIER_nondet_int() ; 28 874 int s__ctx__info_callback = __VERIFIER_nondet_int() ; 28 902 s__ctx__info_callback == (1); ssl3_connect int s__ctx__stats__sess_connect_renegotiate = __VERIFIER_nondet_int() ; 29 930 int s__ctx__stats__sess_connect_renegotiate = __VERIFIER_nondet_int() ; 29 976 s__ctx__stats__sess_connect_renegotiate == (7); ssl3_connect int s__ctx__stats__sess_connect = __VERIFIER_nondet_int() ; 30 1004 int s__ctx__stats__sess_connect = __VERIFIER_nondet_int() ; 30 1038 s__ctx__stats__sess_connect == (5); ssl3_connect int s__ctx__stats__sess_hit = __VERIFIER_nondet_int() ; 31 1066 int s__ctx__stats__sess_hit = __VERIFIER_nondet_int() ; 31 1094 s__ctx__stats__sess_hit == (14); ssl3_connect int s__ctx__stats__sess_connect_good = __VERIFIER_nondet_int() ; 32 1124 int s__ctx__stats__sess_connect_good = __VERIFIER_nondet_int() ; 32 1163 s__ctx__stats__sess_connect_good == (15); ssl3_connect int s__s3__change_cipher_spec ; 33 1191 int s__s3__flags ; 34 1225 int s__s3__delay_buf_pop_ret ; 35 1246 int s__s3__tmp__cert_req = __VERIFIER_nondet_int() ; 36 1279 int s__s3__tmp__cert_req = __VERIFIER_nondet_int() ; 36 1306 s__s3__tmp__cert_req == (16); ssl3_connect int s__s3__tmp__new_compression = __VERIFIER_nondet_int() ; 37 1334 int s__s3__tmp__new_compression = __VERIFIER_nondet_int() ; 37 1368 s__s3__tmp__new_compression == (17); ssl3_connect int s__s3__tmp__reuse_message = __VERIFIER_nondet_int() ; 38 1396 int s__s3__tmp__new_cipher = __VERIFIER_nondet_int() ; 39 1456 s__s3__tmp__reuse_message == (1); ssl3_connect int s__s3__tmp__new_cipher = __VERIFIER_nondet_int() ; 39 1483 s__s3__tmp__new_cipher == (18); ssl3_connect int s__s3__tmp__new_cipher__algorithms = __VERIFIER_nondet_int() ; 40 1513 int s__s3__tmp__new_cipher__algorithms = __VERIFIER_nondet_int() ; 40 1552 s__s3__tmp__new_cipher__algorithms == (256); ssl3_connect int s__s3__tmp__next_state___0 ; 41 1582 int s__s3__tmp__new_compression__id = __VERIFIER_nondet_int() ; 42 1617 int s__session__cipher ; 43 1683 s__s3__tmp__new_compression__id == (19); ssl3_connect int s__session__compress_meth ; 44 1710 int buf ; 45 1744 unsigned long tmp ; 46 1756 unsigned long l ; 47 1778 int num1 ; 48 1798 int cb ; 49 1811 int ret ; 50 1822 int new_state ; 51 1834 int state ; 52 1852 int skip ; 53 1866 int tmp___0 ; 54 1879 int tmp___1 = __VERIFIER_nondet_int() ; 55 1895 int tmp___2 = __VERIFIER_nondet_int() ; 56 1937 tmp___1 == (12288); ssl3_connect int tmp___2 = __VERIFIER_nondet_int() ; 56 1949 tmp___2 == (20); ssl3_connect int tmp___3 = __VERIFIER_nondet_int() ; 57 1979 int tmp___3 = __VERIFIER_nondet_int() ; 57 1993 tmp___3 == (-1); ssl3_connect int tmp___4 = __VERIFIER_nondet_int() ; 58 2021 int tmp___4 = __VERIFIER_nondet_int() ; 58 2035 tmp___4 == (1); ssl3_connect int tmp___5 = __VERIFIER_nondet_int() ; 59 2063 int tmp___5 = __VERIFIER_nondet_int() ; 59 2077 tmp___5 == (1); ssl3_connect int tmp___6 = __VERIFIER_nondet_int() ; 60 2105 int tmp___6 = __VERIFIER_nondet_int() ; 60 2119 tmp___6 == (1); ssl3_connect int tmp___7 = __VERIFIER_nondet_int() ; 61 2147 int tmp___7 = __VERIFIER_nondet_int() ; 61 2159 tmp___7 == (21); ssl3_connect int tmp___8 = __VERIFIER_nondet_int() ; 62 2189 int tmp___8 = __VERIFIER_nondet_int() ; 62 2203 tmp___8 == (22); ssl3_connect int tmp___9 = __VERIFIER_nondet_int() ; 63 2231 int blastFlag ; 64 2273 tmp___9 == (23); ssl3_connect int __cil_tmp55 ; 65 2291 long __cil_tmp56 ; 66 2311 long __cil_tmp57 ; 67 2332 long __cil_tmp58 ; 68 2353 long __cil_tmp59 ; 69 2374 long __cil_tmp60 ; 70 2395 long __cil_tmp61 ; 71 2416 long __cil_tmp62 ; 72 2437 long __cil_tmp63 ; 73 2458 long __cil_tmp64 ; 74 2479 s__state = initial_state; 79 2516 s__state == (12292); ssl3_connect blastFlag = 0; 81 2553 blastFlag == (0); ssl3_connect tmp = __VERIFIER_nondet_int(); 83 2585 tmp == (24UL); ssl3_connect cb = 0; 85 2621 cb == (0); ssl3_connect ret = -1; 87 2640 ret == (-1); ssl3_connect skip = 0; 89 2668 skip == (0); ssl3_connect tmp___0 = 0; 91 2682 tmp___0 == (0); ssl3_connect [!(s__info_callback != 0)] 93 2730 condition-false true [s__info_callback != 0] 93 2730 condition-true [s__ctx__info_callback != 0] 98 2824 condition-true [!(s__ctx__info_callback != 0)] 98 2824 condition-false cb = s__ctx__info_callback; 100 2844 cb == (1); ssl3_connect s__in_handshake ++; 104 2893 s__in_handshake == (10); ssl3_connect [!(((tmp___1 - 12288) == 0) == 0)] 106 2938 condition-false [((tmp___1 - 12288) == 0) == 0] 106 2938 condition-true state = s__state; 117 3074 state == (12292); ssl3_connect [s__state == 12292] 119 3109 condition-true [!(s__state == 12292)] 119 3109 condition-false s__new_session = 1; 255 9150 s__new_session == (1); ssl3_connect s__state = 4096; 257 9252 s__state == (4096); ssl3_connect s__ctx__stats__sess_connect_renegotiate ++; 259 9351 s__ctx__stats__sess_connect_renegotiate == (8); ssl3_connect s__server = 0; 265 9834 s__server == (0); ssl3_connect [cb != 0] 267 9935 condition-true [!(cb != 0)] 267 9935 condition-false __cil_tmp55 = s__version - 65280; 272 10191 __cil_tmp55 == (768); ssl3_connect [!(__cil_tmp55 != 768)] 274 10297 condition-false [__cil_tmp55 != 768] 274 10297 condition-true s__type = 4096; 281 10727 s__type == (4096); ssl3_connect [s__init_buf___0 == 0] 283 10829 condition-true [!(s__init_buf___0 == 0)] 283 10829 condition-false buf = __VERIFIER_nondet_int(); 285 10937 buf == (1); ssl3_connect [!(buf == 0)] 287 11063 condition-false [buf == 0] 287 11063 condition-true [!(tmp___3 == 0)] 293 11416 condition-false [tmp___3 == 0] 293 11416 condition-true s__init_buf___0 = buf; 299 11787 s__init_buf___0 == (1); ssl3_connect [!(tmp___4 == 0)] 302 11954 condition-false [tmp___4 == 0] 302 11954 condition-true [!(tmp___5 == 0)] 308 12305 condition-false [tmp___5 == 0] 308 12305 condition-true s__state = 4368; 314 12650 s__state == (4368); ssl3_connect s__ctx__stats__sess_connect ++; 316 12749 s__ctx__stats__sess_connect == (6); ssl3_connect s__init_num = 0; 318 12877 s__init_num == (0); ssl3_connect [!(s__s3__tmp__reuse_message == 0)] 710 36238 condition-false [s__s3__tmp__reuse_message == 0] 710 36238 condition-true skip = 0; 737 36718 skip == (0); ssl3_connect state = s__state; 117 3074 state == (4368); ssl3_connect [!(s__state == 12292)] 119 3109 condition-false [s__state == 12292] 119 3109 condition-true [!(s__state == 16384)] 123 3189 condition-false [s__state == 16384] 123 3189 condition-true [!(s__state == 4096)] 127 3275 condition-false [s__state == 4096] 127 3275 condition-true [!(s__state == 20480)] 131 3365 condition-false [s__state == 20480] 131 3365 condition-true [!(s__state == 4099)] 135 3476 condition-false [s__state == 4099] 135 3476 condition-true [s__state == 4368] 139 3579 condition-true [!(s__state == 4368)] 139 3579 condition-false s__shutdown = 0; 323 13246 s__shutdown == (0); ssl3_connect ret = __VERIFIER_nondet_int(); 325 13331 ret == (1); ssl3_connect [blastFlag == 0] 327 13448 condition-true [!(blastFlag == 0)] 327 13448 condition-false blastFlag = 1; 329 13550 blastFlag == (1); ssl3_connect [!(ret <= 0)] 332 13725 condition-false [ret <= 0] 332 13725 condition-true s__state = 4384; 336 13977 s__state == (4384); ssl3_connect s__init_num = 0; 338 14076 s__init_num == (0); ssl3_connect [s__bbio != s__wbio] 340 14179 condition-true [!(s__bbio != s__wbio)] 340 14179 condition-false [!(s__s3__tmp__reuse_message == 0)] 710 36238 condition-false [s__s3__tmp__reuse_message == 0] 710 36238 condition-true skip = 0; 737 36718 skip == (0); ssl3_connect state = s__state; 117 3074 state == (4384); ssl3_connect [!(s__state == 12292)] 119 3109 condition-false [s__state == 12292] 119 3109 condition-true [!(s__state == 16384)] 123 3189 condition-false [s__state == 16384] 123 3189 condition-true [!(s__state == 4096)] 127 3275 condition-false [s__state == 4096] 127 3275 condition-true [!(s__state == 20480)] 131 3365 condition-false [s__state == 20480] 131 3365 condition-true [!(s__state == 4099)] 135 3476 condition-false [s__state == 4099] 135 3476 condition-true [!(s__state == 4368)] 139 3579 condition-false [s__state == 4368] 139 3579 condition-true [!(s__state == 4369)] 143 3676 condition-false [s__state == 4369] 143 3676 condition-true [s__state == 4384] 147 3791 condition-true [!(s__state == 4384)] 147 3791 condition-false ret = __VERIFIER_nondet_int(); 347 14628 ret == (1); ssl3_connect [blastFlag == 1] 349 14758 condition-true [!(blastFlag == 1)] 349 14758 condition-false blastFlag = 2; 351 14859 blastFlag == (2); ssl3_connect [!(ret <= 0)] 354 15022 condition-false [ret <= 0] 354 15022 condition-true [!((s__hit == 0) == 0)] 358 15278 condition-false [(s__hit == 0) == 0] 358 15278 condition-true s__state = 4400; 363 15554 s__state == (4400); ssl3_connect s__init_num = 0; 366 15727 s__init_num == (0); ssl3_connect [!(s__s3__tmp__reuse_message == 0)] 710 36238 condition-false [s__s3__tmp__reuse_message == 0] 710 36238 condition-true skip = 0; 737 36718 skip == (0); ssl3_connect state = s__state; 117 3074 state == (4400); ssl3_connect [!(s__state == 12292)] 119 3109 condition-false [s__state == 12292] 119 3109 condition-true [!(s__state == 16384)] 123 3189 condition-false [s__state == 16384] 123 3189 condition-true [!(s__state == 4096)] 127 3275 condition-false [s__state == 4096] 127 3275 condition-true [!(s__state == 20480)] 131 3365 condition-false [s__state == 20480] 131 3365 condition-true [!(s__state == 4099)] 135 3476 condition-false [s__state == 4099] 135 3476 condition-true [!(s__state == 4368)] 139 3579 condition-false [s__state == 4368] 139 3579 condition-true [!(s__state == 4369)] 143 3676 condition-false [s__state == 4369] 143 3676 condition-true [!(s__state == 4384)] 147 3791 condition-false [s__state == 4384] 147 3791 condition-true [!(s__state == 4385)] 151 3912 condition-false [s__state == 4385] 151 3912 condition-true [s__state == 4400] 155 4051 condition-true [!(s__state == 4400)] 155 4051 condition-false [!(((s__s3__tmp__new_cipher__algorithms - 256) == 0) == 0)] 371 16101 condition-false [((s__s3__tmp__new_cipher__algorithms - 256) == 0) == 0] 371 16101 condition-true ret = __VERIFIER_nondet_int(); 376 16404 ret == (1); ssl3_connect [blastFlag == 2] 378 16523 condition-true [!(blastFlag == 2)] 378 16523 condition-false blastFlag = 3; 380 16639 blastFlag == (3); ssl3_connect [!(ret <= 0)] 383 16806 condition-false [ret <= 0] 383 16806 condition-true s__state = 4416; 388 17147 s__state == (4416); ssl3_connect s__init_num = 0; 390 17235 s__init_num == (0); ssl3_connect [!(s__s3__tmp__reuse_message == 0)] 710 36238 condition-false [s__s3__tmp__reuse_message == 0] 710 36238 condition-true skip = 0; 737 36718 skip == (0); ssl3_connect state = s__state; 117 3074 state == (4416); ssl3_connect [!(s__state == 12292)] 119 3109 condition-false [s__state == 12292] 119 3109 condition-true [!(s__state == 16384)] 123 3189 condition-false [s__state == 16384] 123 3189 condition-true [!(s__state == 4096)] 127 3275 condition-false [s__state == 4096] 127 3275 condition-true [!(s__state == 20480)] 131 3365 condition-false [s__state == 20480] 131 3365 condition-true [!(s__state == 4099)] 135 3476 condition-false [s__state == 4099] 135 3476 condition-true [!(s__state == 4368)] 139 3579 condition-false [s__state == 4368] 139 3579 condition-true [!(s__state == 4369)] 143 3676 condition-false [s__state == 4369] 143 3676 condition-true [!(s__state == 4384)] 147 3791 condition-false [s__state == 4384] 147 3791 condition-true [!(s__state == 4385)] 151 3912 condition-false [s__state == 4385] 151 3912 condition-true [!(s__state == 4400)] 155 4051 condition-false [s__state == 4400] 155 4051 condition-true [!(s__state == 4401)] 159 4184 condition-false [s__state == 4401] 159 4184 condition-true [s__state == 4416] 163 4311 condition-true [!(s__state == 4416)] 163 4311 condition-false ret = __VERIFIER_nondet_int(); 395 17604 ret == (1); ssl3_connect [blastFlag == 3] 397 17721 condition-true [!(blastFlag == 3)] 397 17721 condition-false blastFlag = 4; 399 17823 blastFlag == (4); ssl3_connect [!(ret <= 0)] 402 18005 condition-false [ret <= 0] 402 18005 condition-true s__state = 4432; 406 18261 s__state == (4432); ssl3_connect s__init_num = 0; 408 18363 s__init_num == (0); ssl3_connect [!(tmp___6 == 0)] 410 18454 condition-false [tmp___6 == 0] 410 18454 condition-true [!(s__s3__tmp__reuse_message == 0)] 710 36238 condition-false [s__s3__tmp__reuse_message == 0] 710 36238 condition-true skip = 0; 737 36718 skip == (0); ssl3_connect state = s__state; 117 3074 state == (4432); ssl3_connect [!(s__state == 12292)] 119 3109 condition-false [s__state == 12292] 119 3109 condition-true [!(s__state == 16384)] 123 3189 condition-false [s__state == 16384] 123 3189 condition-true [!(s__state == 4096)] 127 3275 condition-false [s__state == 4096] 127 3275 condition-true [!(s__state == 20480)] 131 3365 condition-false [s__state == 20480] 131 3365 condition-true [!(s__state == 4099)] 135 3476 condition-false [s__state == 4099] 135 3476 condition-true [!(s__state == 4368)] 139 3579 condition-false [s__state == 4368] 139 3579 condition-true [!(s__state == 4369)] 143 3676 condition-false [s__state == 4369] 143 3676 condition-true [!(s__state == 4384)] 147 3791 condition-false [s__state == 4384] 147 3791 condition-true [!(s__state == 4385)] 151 3912 condition-false [s__state == 4385] 151 3912 condition-true [!(s__state == 4400)] 155 4051 condition-false [s__state == 4400] 155 4051 condition-true [!(s__state == 4401)] 159 4184 condition-false [s__state == 4401] 159 4184 condition-true [!(s__state == 4416)] 163 4311 condition-false [s__state == 4416] 163 4311 condition-true [!(s__state == 4417)] 167 4456 condition-false [s__state == 4417] 167 4456 condition-true [s__state == 4432] 171 4607 condition-true [!(s__state == 4432)] 171 4607 condition-false ret = __VERIFIER_nondet_int(); 419 19069 ret == (25); ssl3_connect [blastFlag == 4] 421 19186 condition-true [!(blastFlag == 4)] 421 19186 condition-false true __VERIFIER_error(); 751 36879