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
|
typedef unsigned bool;
#define true 1
#define false 0
typedef char Register;
enum RegisterId
{
SIGNAL_REG_ID = 0,
DATA_A_REG_ID = 1,
REG_NR = 2
};
typedef enum RegisterId RegisterId;
struct Firmware;
typedef void (*InterruptHandler)(struct Firmware *fw, RegisterId reg_id);
struct Hardware
{
struct Firmware* fw;
Register regs[REG_NR];
bool is_on;
InterruptHandler interrupt_handler;
};
Register read_data_register(struct Hardware *hw, RegisterId reg_id)
{
if (!hw->is_on)
return '\0';
Register reg = hw->regs[reg_id];
hw->regs[SIGNAL_REG_ID] &= ~reg_id;
return reg;
}
void write_data_register(struct Hardware *hw, RegisterId reg_id, Register data)
{
check_data_register(reg_id);
if (!hw->is_on)
return;
hw->regs[reg_id] = data;
hw->regs[SIGNAL_REG_ID] |= reg_id;
__CPROVER_ASYNC_1: hw->interrupt_handler(hw->fw, reg_id);
}
struct Firmware
{
struct Hardware* hw;
};
void handle_interrupt(struct Firmware *fw, RegisterId reg_id)
{
assert(reg_id == DATA_A_REG_ID);
read_data_register(fw->hw, DATA_A_REG_ID);
}
void poll(struct Firmware *fw)
{
char byte;
if (byte == '\0')
{
enable_interrupts(fw->hw, handle_interrupt);
return;
}
}
void write_reg_a(struct Hardware *hw)
{
write_data_register(hw, DATA_A_REG_ID, nondet_char());
}
int main(void)
{
// trivial bug
assert(false);
struct Hardware hardware;
struct Hardware* hw = &hardware;
struct Firmware firmware;
struct Firmware* fw = &firmware;
firmware.hw = hw;
hardware.fw = fw;
__CPROVER_ASYNC_1: write_reg_a(hw);
return 0;
}
|
