../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