This repository has been archived by the owner on Oct 3, 2021. It is now read-only.
/
stateful_check_false-unreach-call_false-termination.i
117 lines (91 loc) · 2.52 KB
/
stateful_check_false-unreach-call_false-termination.i
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
void __blast_assert(void) {
ERROR: __VERIFIER_error();
}
int ldv_mutex = 1;
int open_called = 0;
extern int __VERIFIER_nondet_int(void);
void mutex_lock(void)
{
((ldv_mutex == 1) ? 0 : __blast_assert());
ldv_mutex = 2;
}
void mutex_unlock(void)
{
((ldv_mutex == 2) ? 0 : __blast_assert());
ldv_mutex = 1;
}
void check_final_state(void)
{
((ldv_mutex == 1) ? 0 : __blast_assert());
}
static int misc_release() {
if(open_called) {
mutex_lock();
mutex_unlock();
open_called = 0;
} else {
mutex_lock();
mutex_lock();
}
return 0;
}
static int misc_llseek() {
return 0;
}
static int misc_read() {
return 0;
}
static int misc_open()
{
if(__VERIFIER_nondet_int()) {
return 1;
} else {
open_called = 1;
return 0;
}
}
static int my_init(void)
{
open_called = 0;
return 0;
}
int main(void) {
int ldv_s_misc_fops_file_operations = 0;
my_init();
while(__VERIFIER_nondet_int()) {
switch(__VERIFIER_nondet_int()) {
case 0: {
if(ldv_s_misc_fops_file_operations==0) {
misc_open();
ldv_s_misc_fops_file_operations++;
}
}
break;
case 1: {
if(ldv_s_misc_fops_file_operations==1) {
misc_read();
ldv_s_misc_fops_file_operations++;
}
}
break;
case 2: {
if(ldv_s_misc_fops_file_operations==2) {
misc_llseek();
ldv_s_misc_fops_file_operations++;
}
}
break;
case 3: {
if(ldv_s_misc_fops_file_operations==3) {
misc_release();
ldv_s_misc_fops_file_operations=0;
}
}
break;
default: break;
}
}
check_final_state();
return 0;
}