1void __blast_assert(void) {
2ERROR: goto ERROR;
3}
4
5
6
7int ldv_mutex = 1;
8
9int open_called = 0;
10int __VERIFIER_nondet_int(void) { int x; return x; }
11
12void mutex_lock(void)
13{
14 ((ldv_mutex == 1) ? 0 : __blast_assert());
15 ldv_mutex = 2;
16}
17
18void mutex_unlock(void)
19{
20 ((ldv_mutex == 2) ? 0 : __blast_assert());
21 ldv_mutex = 1;
22}
23
24void check_final_state(void)
25{
26 ((ldv_mutex == 1) ? 0 : __blast_assert());
27}
28
29static int misc_release() {
30
31
32 if(open_called) {
33
34 mutex_lock();
35 mutex_unlock();
36 open_called = 0;
37 } else {
38
39 mutex_lock();
40 mutex_lock();
41 }
42 return 0;
43}
44
45static int misc_llseek() {
46 return 0;
47}
48
49static int misc_read() {
50 return 0;
51}
52
53static int misc_open()
54{
55 if(__VERIFIER_nondet_int()) {
56
57 return 1;
58 } else {
59 open_called = 1;
60 return 0;
61 }
62}
63
64static int my_init(void)
65{
66
67 open_called = 0;
68 return 0;
69}
70
71void main(void) {
72 int ldv_s_misc_fops_file_operations = 0;
73 my_init();
74 while(__VERIFIER_nondet_int()) {
75
76 switch(__VERIFIER_nondet_int()) {
77
78 case 0: {
79 if(ldv_s_misc_fops_file_operations==0) {
80 misc_open();
81 ldv_s_misc_fops_file_operations++;
82 }
83 }
84 break;
85
86 case 1: {
87 if(ldv_s_misc_fops_file_operations==1) {
88 misc_read();
89 ldv_s_misc_fops_file_operations++;
90 }
91 }
92 break;
93
94 case 2: {
95 if(ldv_s_misc_fops_file_operations==2) {
96 misc_llseek();
97 ldv_s_misc_fops_file_operations++;
98 }
99 }
100 break;
101
102 case 3: {
103 if(ldv_s_misc_fops_file_operations==3) {
104 misc_release();
105 ldv_s_misc_fops_file_operations=0;
106 }
107 }
108 break;
109
110 default: break;
111 }
112 }
113 check_final_state();
114 return;
115}