Project

General

Profile

Download (69 KB)

Bug #9820 » environment_model1.c

The first model - Pavel Andrianov, 09/16/2019 01:00 PM

 
#include <linux/ldv/common.h>
2 #include <linux/ldv/err.h>
3 #include <verifier/common.h>
4 #include <verifier/gcc.h>
5 #include <verifier/nondet.h>
6 #include <verifier/memory.h>
7 #include <verifier/thread.h>
8 #include <linux/interrupt.h>
9 #include <linux/platform_device.h>
10 #include <linux/netdevice.h>
11 #include <linux/pm.h>
12
13 struct ldv_struct_free_irq_3 {
14 int arg0;
15 int signal_pending;
16 };
17
18 struct ldv_struct_interrupt_scenario_13 {
19 enum irqreturn (*arg2)(int, void *);
20 enum irqreturn (*arg1)(int, void *);
21 void *arg3;
22 int arg0;
23 int signal_pending;
24 };
25
26 struct ldv_struct_platform_instance_12 {
27 struct platform_driver *arg0;
28 int signal_pending;
29 };
30
31 struct ldv_struct_random_allocationless_scenario_11 {
32 struct net_device *arg0;
33 int signal_pending;
34 };
35
36
37 /* EMG aliases */
38 extern int (*ldv_emg_alias_eth_validate_addr_8)(struct net_device *);
39 extern int ldv_emg_wrapper_dnet_ioctl_6(struct net_device *, struct ifreq *, int);
40 extern int (*ldv_emg_alias_ethtool_op_get_ts_info_4)(struct net_device *, struct ethtool_ts_info *);
41 extern int ldv_emg_wrapper_dnet_close_2(struct net_device *);
42 extern int ldv_emg_wrapper_dnet_remove_3(struct platform_device *);
43 extern int (*ldv_emg_alias_phy_ethtool_set_link_ksettings_7)(struct net_device *, struct ethtool_link_ksettings *);
44 extern int ldv_emg_wrapper_dnet_open_2(struct net_device *);
45 extern int ldv_emg_dnet_driver_init(void);
46 extern void ldv_emg_wrapper_dnet_get_drvinfo_2(struct net_device *, struct ethtool_drvinfo *);
47 extern void ldv_emg_dnet_driver_exit(void);
48 extern unsigned int (*ldv_emg_alias_ethtool_op_get_link_3)(struct net_device *);
49 extern struct net_device_stats *ldv_emg_wrapper_dnet_get_stats_9(struct net_device *);
50 extern enum irqreturn ldv_emg_wrapper_dnet_interrupt_2(int, void *);
51 extern int (*ldv_emg_alias_eth_mac_addr_10)(struct net_device *, void *);
52 extern struct platform_driver *ldv_emg_alias_dnet_driver_2;
53 extern int (*ldv_emg_alias_phy_ethtool_get_link_ksettings_5)(struct net_device *, struct ethtool_link_ksettings *);
54 extern int ldv_emg_wrapper_dnet_probe_2(struct platform_device *);
55 extern enum netdev_tx ldv_emg_wrapper_dnet_start_xmit_11(struct sk_buff *, struct net_device *);
56
57 /* EMG Function declarations */
58 int main(void);
59 void *ldv_pm_ops_scenario_10(void *);
60 void ldv_emg_platform_driver_unregister(struct platform_driver *);
61 void ldv_dispatch_irq_deregister_3_1(int);
62 struct net_device *ldv_emg_alloc_etherdev_mqs(int, unsigned int, unsigned int);
63 void ldv_dispatch_pm_deregister_12_12(void);
64 void ldv_dispatch_register_7_3(struct platform_driver *);
65 int ldv_emg_request_irq(unsigned int, enum irqreturn (*)(int, void *), long unsigned int, char *, void *);
66 void *ldv_platform_instance_12(void *);
67 void *ldv_random_allocationless_scenario_11(void *);
68 void *ldv_initialization_1(void *);
69 void ldv_dispatch_irq_register_9_3(int, enum irqreturn (*)(int, void *), enum irqreturn (*)(int, void *), void *);
70 void *ldv_interrupt_scenario_13(void *);
71 void ldv_dispatch_deregister_4_1(struct platform_driver *);
72 void ldv_dispatch_register_8_4(struct net_device *);
73 void ldv_dispatch_pm_register_12_13(void);
74 void ldv_emg_unregister_netdev(struct net_device *);
75 void *ldv_emg_free_irq(unsigned int, void *);
76 void ldv_dispatch_deregister_6_1(struct net_device *);
77 void ldv_emg_free_netdev(struct net_device *);
78 int ldv_emg___platform_driver_register(struct platform_driver *, struct module *);
79 int ldv_emg_register_netdev(struct net_device *);
80
81 /* EMG variable declarations */
82 pthread_t ldv_thread_10;
83 pthread_t ldv_thread_12;
84 pthread_t ldv_thread_13;
85 pthread_t ldv_thread_11;
86
87 /* EMG function definitions */
88 /* AUX_FUNC main */
89 int main(void) {
90 /* LDV {"thread": 1, "type": "CONTROL_FUNCTION_BEGIN", "comment": "Entry point 'main'", "function": "main"} */
91 /* LDV {"action": "INIT", "type": "CALL_BEGIN", "callback": true, "comment": "Initialize requirement models."} */
92 ldv_initialize();
93 /* LDV {"action": "INIT", "type": "CALL_END"} */
94 /* LDV {"action": "SCENARIOS", "type": "CONDITION_BEGIN", "comment": "Begin Environment model scenarios."} */
95 ldv_initialization_1(0);
96 /* LDV {"action": "SCENARIOS", "type": "CONDITION_END"} */
97 return 0;
98 /* LDV {"comment": "Exit entry point 'main'", "type": "CONTROL_FUNCTION_END", "function": "main"} */
99 }
100
101 /* AUX_FUNC ldv_pm_ops_scenario_10 */
102 void *ldv_pm_ops_scenario_10(void *arg0) {
103 /* LDV {"thread": 11, "type": "CONTROL_FUNCTION_BEGIN", "comment": "Invoke power management callbacks.", "function": "ldv_pm_ops_scenario_10"} */
104 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
105 struct dev_pm_ops *ldv_10_pm_ops;
106 struct device *ldv_10_device;
107 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
108 /* LDV {"action": "PM_REGISTER", "type": "RECEIVE_BEGIN", "comment": "Ready for a power management scenarios."} */
109 ldv_free(arg0);
110 /* LDV {"action": "PM_REGISTER", "type": "RECEIVE_END"} */
111
112 /* LDV {"action": "DO", "type": "SUBPROCESS_BEGIN", "comment": "Begin a power management scenario."} */
113 /* LDV {"action": "DO", "type": "SUBPROCESS_END"} */
114
115 /* Jump to a subprocess 'do' initial state */
116 goto ldv_do_10;
117 /* End of the process */
118 return 0;
119
120 /* Sbprocess do */
121 ldv_do_10:
122 /* LDV {"action": null, "type": "ARTIFICIAL", "comment": "Artificial state in scenario"} */
123
124 switch (ldv_undef_int()) {
125 case 1: {
126 /* LDV {"action": "RUNTIME_IDLE_15", "type": "CALL_BEGIN", "callback": true, "comment": "Device appears to be inactive and it might be put into a low-power state if all of the necessary conditions are satisfied. Invoke callback runtime_idle from PLATFORM."} */
127 if (ldv_10_pm_ops->runtime_idle) {
128 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->runtime_idle(ldv_10_device);", "comment": "runtime_idle"} */
129 ldv_10_pm_ops->runtime_idle(ldv_10_device);
130 }
131 /* LDV {"action": "RUNTIME_IDLE_15", "type": "CALL_END"} */
132
133 /* LDV {"action": "DO", "type": "SUBPROCESS_BEGIN", "comment": "Begin a power management scenario."} */
134 /* LDV {"action": "DO", "type": "SUBPROCESS_END"} */
135
136 /* Jump to a subprocess 'do' initial state */
137 goto ldv_do_10;
138 break;
139 }
140 case 2: {
141 /* LDV {"action": "RUNTIME_SUSPEND_22", "type": "CALL_BEGIN", "callback": true, "comment": "The device should be put into a low-power state to prevent communication of the device with the CPU(s) and RAM. Invoke callback runtime_suspend from PLATFORM."} */
142 if (ldv_10_pm_ops->runtime_suspend) {
143 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->runtime_suspend(ldv_10_device);", "comment": "runtime_suspend"} */
144 ldv_10_pm_ops->runtime_suspend(ldv_10_device);
145 }
146 /* LDV {"action": "RUNTIME_SUSPEND_22", "type": "CALL_END"} */
147
148 /* LDV {"action": "RUNTIME_RESUME_7", "type": "CALL_BEGIN", "callback": true, "comment": "Put the device into the fully active state in response to a wakeup event generated by hardware or at the request of software. Invoke callback runtime_resume from PLATFORM."} */
149 if (ldv_10_pm_ops->runtime_resume) {
150 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->runtime_resume(ldv_10_device);", "comment": "runtime_resume"} */
151 ldv_10_pm_ops->runtime_resume(ldv_10_device);
152 }
153 /* LDV {"action": "RUNTIME_RESUME_7", "type": "CALL_END"} */
154
155 /* LDV {"action": "DO", "type": "SUBPROCESS_BEGIN", "comment": "Begin a power management scenario."} */
156 /* LDV {"action": "DO", "type": "SUBPROCESS_END"} */
157
158 /* Jump to a subprocess 'do' initial state */
159 goto ldv_do_10;
160 break;
161 }
162 case 3: {
163 /* LDV {"action": "PREPARE_20", "type": "CALL_BEGIN", "callback": true, "comment": "Prevent new children of the device from being registered. Invoke callback prepare from PLATFORM."} */
164 if (ldv_10_pm_ops->prepare) {
165 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->prepare(ldv_10_device);", "comment": "prepare"} */
166 ldv_10_pm_ops->prepare(ldv_10_device);
167 }
168 /* LDV {"action": "PREPARE_20", "type": "CALL_END"} */
169
170 switch (ldv_undef_int()) {
171 case 1: {
172 /* LDV {"action": "SUSPEND_3", "type": "CALL_BEGIN", "callback": true, "comment": "Quiesce subsystem-level device before suspend. Invoke callback suspend from PLATFORM."} */
173 if (ldv_10_pm_ops->suspend) {
174 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->suspend(ldv_10_device);", "comment": "suspend"} */
175 ldv_10_pm_ops->suspend(ldv_10_device);
176 }
177 /* LDV {"action": "SUSPEND_3", "type": "CALL_END"} */
178
179 if (ldv_undef_int()) {
180 /* LDV {"action": "SUSPEND_NOIRQ_19", "type": "CALL_BEGIN", "callback": true, "comment": "Expect that the device will be in a low-power state. Invoke callback suspend_noirq from PLATFORM."} */
181 if (ldv_10_pm_ops->suspend_noirq) {
182 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->suspend_noirq(ldv_10_device);", "comment": "suspend_noirq"} */
183 ldv_10_pm_ops->suspend_noirq(ldv_10_device);
184 }
185 /* LDV {"action": "SUSPEND_NOIRQ_19", "type": "CALL_END"} */
186
187 /* LDV {"action": "RESUME_NOIRQ_21", "type": "CALL_BEGIN", "callback": true, "comment": "Prepare for the @resume() performing actions that might be racing with device's interrupt handler. Invoke callback resume_noirq from PLATFORM."} */
188 if (ldv_10_pm_ops->resume_noirq) {
189 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->resume_noirq(ldv_10_device);", "comment": "resume_noirq"} */
190 ldv_10_pm_ops->resume_noirq(ldv_10_device);
191 }
192 /* LDV {"action": "RESUME_NOIRQ_21", "type": "CALL_END"} */
193
194 }
195 else {
196 /* LDV {"action": "SUSPEND_LATE_10", "type": "CALL_BEGIN", "callback": true, "comment": "Continue operations started by @suspend(). Invoke callback suspend_late from PLATFORM."} */
197 if (ldv_10_pm_ops->suspend_late) {
198 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->suspend_late(ldv_10_device);", "comment": "suspend_late"} */
199 ldv_10_pm_ops->suspend_late(ldv_10_device);
200 }
201 /* LDV {"action": "SUSPEND_LATE_10", "type": "CALL_END"} */
202
203 /* LDV {"action": "RESUME_EARLY_16", "type": "CALL_BEGIN", "callback": true, "comment": "Prepare to execute @resume(). Invoke callback resume_early from PLATFORM."} */
204 if (ldv_10_pm_ops->resume_early) {
205 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->resume_early(ldv_10_device);", "comment": "resume_early"} */
206 ldv_10_pm_ops->resume_early(ldv_10_device);
207 }
208 /* LDV {"action": "RESUME_EARLY_16", "type": "CALL_END"} */
209
210 }
211 /* LDV {"action": "RESUME_17", "type": "CALL_BEGIN", "callback": true, "comment": "Make the device start working again after resume. Invoke callback resume from PLATFORM."} */
212 if (ldv_10_pm_ops->resume) {
213 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->resume(ldv_10_device);", "comment": "resume"} */
214 ldv_10_pm_ops->resume(ldv_10_device);
215 }
216 /* LDV {"action": "RESUME_17", "type": "CALL_END"} */
217
218 break;
219 }
220 case 2: {
221 /* LDV {"action": "FREEZE_2", "type": "CALL_BEGIN", "callback": true, "comment": "Prepare for creating a hibernation image. Invoke callback freeze from PLATFORM."} */
222 if (ldv_10_pm_ops->freeze) {
223 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->freeze(ldv_10_device);", "comment": "freeze"} */
224 ldv_10_pm_ops->freeze(ldv_10_device);
225 }
226 /* LDV {"action": "FREEZE_2", "type": "CALL_END"} */
227
228 if (ldv_undef_int()) {
229 /* LDV {"action": "FREEZE_LATE_5", "type": "CALL_BEGIN", "callback": true, "comment": "Continue operations started by @freeze(). Invoke callback freeze_late from PLATFORM."} */
230 if (ldv_10_pm_ops->freeze_late) {
231 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->freeze_late(ldv_10_device);", "comment": "freeze_late"} */
232 ldv_10_pm_ops->freeze_late(ldv_10_device);
233 }
234 /* LDV {"action": "FREEZE_LATE_5", "type": "CALL_END"} */
235
236 /* LDV {"action": "THAW_EARLY_13", "type": "CALL_BEGIN", "callback": true, "comment": "Prepare to execute @thaw(). Invoke callback thaw_early from PLATFORM."} */
237 if (ldv_10_pm_ops->thaw_early) {
238 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->thaw_early(ldv_10_device);", "comment": "thaw_early"} */
239 ldv_10_pm_ops->thaw_early(ldv_10_device);
240 }
241 /* LDV {"action": "THAW_EARLY_13", "type": "CALL_END"} */
242
243 }
244 else {
245 /* LDV {"action": "FREEZE_NOIRQ_9", "type": "CALL_BEGIN", "callback": true, "comment": "Complete the actions started by @freeze() that might be racing with device's interrupt handler. Invoke callback freeze_noirq from PLATFORM."} */
246 if (ldv_10_pm_ops->freeze_noirq) {
247 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->freeze_noirq(ldv_10_device);", "comment": "freeze_noirq"} */
248 ldv_10_pm_ops->freeze_noirq(ldv_10_device);
249 }
250 /* LDV {"action": "FREEZE_NOIRQ_9", "type": "CALL_END"} */
251
252 /* LDV {"action": "THAW_NOIRQ_18", "type": "CALL_BEGIN", "callback": true, "comment": "Prepare for the execution of @thaw() performing actions that might be racing with device's interrupt handler. Invoke callback thaw_noirq from PLATFORM."} */
253 if (ldv_10_pm_ops->thaw_noirq) {
254 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->thaw_noirq(ldv_10_device);", "comment": "thaw_noirq"} */
255 ldv_10_pm_ops->thaw_noirq(ldv_10_device);
256 }
257 /* LDV {"action": "THAW_NOIRQ_18", "type": "CALL_END"} */
258
259 }
260 /* LDV {"action": "THAW_24", "type": "CALL_BEGIN", "callback": true, "comment": "The hibernation image has created or creation has failed. Invoke callback thaw from PLATFORM."} */
261 if (ldv_10_pm_ops->thaw) {
262 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->thaw(ldv_10_device);", "comment": "thaw"} */
263 ldv_10_pm_ops->thaw(ldv_10_device);
264 }
265 /* LDV {"action": "THAW_24", "type": "CALL_END"} */
266
267 break;
268 }
269 case 3: {
270 /* LDV {"action": "POWEROFF_11", "type": "CALL_BEGIN", "callback": true, "comment": "Hibernation image has been created. Invoke callback poweroff from PLATFORM."} */
271 if (ldv_10_pm_ops->poweroff) {
272 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->poweroff(ldv_10_device);", "comment": "poweroff"} */
273 ldv_10_pm_ops->poweroff(ldv_10_device);
274 }
275 /* LDV {"action": "POWEROFF_11", "type": "CALL_END"} */
276
277 if (ldv_undef_int()) {
278 /* LDV {"action": "POWEROFF_LATE_12", "type": "CALL_BEGIN", "callback": true, "comment": "Continue operations started by @poweroff(). Invoke callback poweroff_late from PLATFORM."} */
279 if (ldv_10_pm_ops->poweroff_late) {
280 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->poweroff_late(ldv_10_device);", "comment": "poweroff_late"} */
281 ldv_10_pm_ops->poweroff_late(ldv_10_device);
282 }
283 /* LDV {"action": "POWEROFF_LATE_12", "type": "CALL_END"} */
284
285 /* LDV {"action": "RESTORE_EARLY_23", "type": "CALL_BEGIN", "callback": true, "comment": "Prepare to execute @restore(). Invoke callback restore_early from PLATFORM."} */
286 if (ldv_10_pm_ops->restore_early) {
287 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->restore_early(ldv_10_device);", "comment": "restore_early"} */
288 ldv_10_pm_ops->restore_early(ldv_10_device);
289 }
290 /* LDV {"action": "RESTORE_EARLY_23", "type": "CALL_END"} */
291
292 }
293 else {
294 /* LDV {"action": "POWEROFF_NOIRQ_14", "type": "CALL_BEGIN", "callback": true, "comment": "Complete the actions started by @poweroff(). Invoke callback poweroff_noirq from PLATFORM."} */
295 if (ldv_10_pm_ops->poweroff_noirq) {
296 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->poweroff_noirq(ldv_10_device);", "comment": "poweroff_noirq"} */
297 ldv_10_pm_ops->poweroff_noirq(ldv_10_device);
298 }
299 /* LDV {"action": "POWEROFF_NOIRQ_14", "type": "CALL_END"} */
300
301 /* LDV {"action": "RESTORE_NOIRQ_4", "type": "CALL_BEGIN", "callback": true, "comment": "Prepare for the execution of @restore() performing actions that might be racing with device's interrupt handler. Invoke callback restore_noirq from PLATFORM."} */
302 if (ldv_10_pm_ops->restore_noirq) {
303 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->restore_noirq(ldv_10_device);", "comment": "restore_noirq"} */
304 ldv_10_pm_ops->restore_noirq(ldv_10_device);
305 }
306 /* LDV {"action": "RESTORE_NOIRQ_4", "type": "CALL_END"} */
307
308 }
309 /* LDV {"action": "RESTORE_6", "type": "CALL_BEGIN", "callback": true, "comment": "Restoration of the contents of main memory from a hibernation image has been done. Invoke callback restore from PLATFORM."} */
310 if (ldv_10_pm_ops->restore) {
311 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->restore(ldv_10_device);", "comment": "restore"} */
312 ldv_10_pm_ops->restore(ldv_10_device);
313 }
314 /* LDV {"action": "RESTORE_6", "type": "CALL_END"} */
315
316 break;
317 }
318 default: ldv_assume(0);
319 }
320 /* LDV {"action": "COMPLETE_8", "type": "CALL_BEGIN", "callback": true, "comment": "Undo the changes made by @prepare(). Invoke callback complete from PLATFORM."} */
321 if (ldv_10_pm_ops->complete) {
322 /* LDV {"type": "CALLBACK", "call": "ldv_10_pm_ops->complete(ldv_10_device);", "comment": "complete"} */
323 ldv_10_pm_ops->complete(ldv_10_device);
324 }
325 /* LDV {"action": "COMPLETE_8", "type": "CALL_END"} */
326
327 /* LDV {"action": "DO", "type": "SUBPROCESS_BEGIN", "comment": "Begin a power management scenario."} */
328 /* LDV {"action": "DO", "type": "SUBPROCESS_END"} */
329
330 /* Jump to a subprocess 'do' initial state */
331 goto ldv_do_10;
332 break;
333 }
334 case 4: {
335 /* LDV {"action": "PM_DEREGISTER", "type": "RECEIVE_BEGIN", "comment": "Do not expect power management scenarios."} */
336 /* Skip a non-replicative signal receiving */
337 /* LDV {"action": "PM_DEREGISTER", "type": "RECEIVE_END"} */
338
339 /* Exit function at a terminal state */
340 return 0;
341 break;
342 }
343 default: ldv_assume(0);
344 }
345 /* End of the subprocess 'do' */
346 return 0;
347 /* LDV {"comment": "End of control function based on process 'pm_ops_scenario(platform)'", "type": "CONTROL_FUNCTION_END", "function": "ldv_pm_ops_scenario_10"} */
348 }
349
350 /* AUX_FUNC ldv_emg_platform_driver_unregister */
351 void ldv_emg_platform_driver_unregister(struct platform_driver *arg0) {
352 /* LDV {"comment": "Unregister a driver for platform-level device. (Relevant to 'dnet_driver')", "type": "CONTROL_FUNCTION_BEGIN", "function": "ldv_emg_platform_driver_unregister"} */
353 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
354 struct platform_driver *ldv_4_platform_driver = ldv_emg_alias_dnet_driver_2;
355 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
356 /* LDV {"action": "ASSIGN", "type": "CONDITION_BEGIN", "comment": "Get 'platform_driver' argument."} */
357 ldv_4_platform_driver = arg0;
358 /* LDV {"action": "ASSIGN", "type": "CONDITION_END"} */
359
360 /* LDV {"action": "DEREGISTER", "type": "DISPATCH_BEGIN", "comment": "Deregister 'platform_driver' callbacks."} */
361 ldv_dispatch_deregister_4_1(ldv_4_platform_driver);
362 /* LDV {"action": "DEREGISTER", "type": "DISPATCH_END"} */
363
364 /* Exit function at a terminal state */
365 return;
366 /* End of the process */
367 return;
368 /* LDV {"comment": "End of control function based on process 'platform_driver_unregister'", "type": "CONTROL_FUNCTION_END", "function": "ldv_emg_platform_driver_unregister"} */
369 }
370
371 /* AUX_FUNC ldv_dispatch_irq_deregister_3_1 */
372 void ldv_dispatch_irq_deregister_3_1(int arg0) {
373 int ret;
374 struct ldv_struct_free_irq_3 *cf_arg_13;
375 switch (ldv_undef_int()) {
376 case 0: {
377 ret = pthread_join(ldv_thread_13, 0);
378 ldv_assume(ret == 0);
379 break;
380 };
381 default: ldv_assume(0);
382 };
383 return;
384 }
385
386 /* AUX_FUNC ldv_emg_alloc_etherdev_mqs */
387 struct net_device *ldv_emg_alloc_etherdev_mqs(int arg0, unsigned int arg1, unsigned int arg2) {
388 /* LDV {"comment": "Allocate and set up an ethernet device.", "type": "CONTROL_FUNCTION_BEGIN", "function": "ldv_emg_alloc_etherdev_mqs"} */
389 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
390 struct net_device *ldv_5_netdev;
391 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
392 /* LDV {"action": null, "type": "ARTIFICIAL", "comment": "Artificial state in scenario"} */
393
394 if (ldv_undef_int()) {
395 /* LDV {"action": "ALLOC", "type": "CONDITION_BEGIN", "comment": "Allocate memory for an ethernet device."} */
396 ldv_5_netdev = ldv_xmalloc_unknown_size(0);
397 /* LDV {"action": "ALLOC", "type": "CONDITION_END"} */
398
399 /* LDV {"action": "SUCCESS", "type": "CONDITION_BEGIN", "comment": "Memory has been allocated properly."} */
400 return ldv_5_netdev;
401 /* LDV {"action": "SUCCESS", "type": "CONDITION_END"} */
402
403 /* Exit function at a terminal state */
404 }
405 else {
406 /* LDV {"action": "FAIL", "type": "CONDITION_BEGIN", "comment": "Memory has not been allocated."} */
407 return 0;
408 /* LDV {"action": "FAIL", "type": "CONDITION_END"} */
409
410 /* Exit function at a terminal state */
411 }
412 /* End of the process */
413 /* LDV {"comment": "End of control function based on process 'alloc_etherdev_mqs'", "type": "CONTROL_FUNCTION_END", "function": "ldv_emg_alloc_etherdev_mqs"} */
414 }
415
416 /* AUX_FUNC ldv_dispatch_register_8_4 */
417 void ldv_dispatch_register_8_4(struct net_device *arg0) {
418 int ret;
419 struct ldv_struct_random_allocationless_scenario_11 *cf_arg_11;
420 switch (ldv_undef_int()) {
421 case 0: {
422 cf_arg_11 = ldv_xmalloc(sizeof(struct ldv_struct_random_allocationless_scenario_11));
423 cf_arg_11->arg0 = arg0;
424 ret = pthread_create(& ldv_thread_11, 0, ldv_random_allocationless_scenario_11, cf_arg_11);
425 ldv_assume(ret == 0);
426 break;
427 };
428 default: ldv_assume(0);
429 };
430 return;
431 }
432
433 /* AUX_FUNC ldv_dispatch_register_7_3 */
434 void ldv_dispatch_register_7_3(struct platform_driver *arg0) {
435 int ret;
436 struct ldv_struct_platform_instance_12 *cf_arg_12;
437 switch (ldv_undef_int()) {
438 case 0: {
439 cf_arg_12 = ldv_xmalloc(sizeof(struct ldv_struct_platform_instance_12));
440 cf_arg_12->arg0 = arg0;
441 ret = pthread_create(& ldv_thread_12, 0, ldv_platform_instance_12, cf_arg_12);
442 ldv_assume(ret == 0);
443 break;
444 };
445 default: ldv_assume(0);
446 };
447 return;
448 }
449
450 /* AUX_FUNC ldv_emg_request_irq */
451 int ldv_emg_request_irq(unsigned int arg0, enum irqreturn (*arg1)(int, void *), long unsigned int arg2, char *arg3, void *arg4) {
452 /* LDV {"comment": "Allocate an interrupt line for a managed device. (Relevant to 'dnet_interrupt')", "type": "CONTROL_FUNCTION_BEGIN", "function": "ldv_emg_request_irq"} */
453 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
454 int ldv_9_line;
455 void *ldv_9_data;
456 enum irqreturn (*ldv_9_callback)(int, void *) = &ldv_emg_wrapper_dnet_interrupt_2;
457 enum irqreturn (*ldv_9_thread)(int, void *);
458 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
459 /* LDV {"action": null, "type": "ARTIFICIAL", "comment": "Artificial state in scenario"} */
460
461 if (ldv_undef_int()) {
462 /* LDV {"action": "ASSIGN", "type": "CONDITION_BEGIN", "comment": "Get line, callbacks and data arguments."} */
463 ldv_9_line = arg0;
464 ldv_9_callback = arg1;
465 ldv_9_thread = 0;
466 ldv_9_data = arg4;
467 /* LDV {"action": "ASSIGN", "type": "CONDITION_END"} */
468
469 /* LDV {"action": "IRQ_REGISTER", "type": "DISPATCH_BEGIN", "comment": "Register interrupt callback (callbacks)."} */
470 ldv_dispatch_irq_register_9_3(ldv_9_line, ldv_9_callback, ldv_9_thread, ldv_9_data);
471 /* LDV {"action": "IRQ_REGISTER", "type": "DISPATCH_END"} */
472
473 /* LDV {"action": "SUCCESS", "type": "CONDITION_BEGIN", "comment": "Successfully allocated an interrupt line for a managed device."} */
474 return 0;
475 /* LDV {"action": "SUCCESS", "type": "CONDITION_END"} */
476
477 /* Exit function at a terminal state */
478 }
479 else {
480 /* LDV {"action": "FAIL", "type": "CONDITION_BEGIN", "comment": "Failed to allocate an interrupt line for a managed device."} */
481 return ldv_undef_int_negative();
482 /* LDV {"action": "FAIL", "type": "CONDITION_END"} */
483
484 /* Exit function at a terminal state */
485 }
486 /* End of the process */
487 /* LDV {"comment": "End of control function based on process 'request_irq'", "type": "CONTROL_FUNCTION_END", "function": "ldv_emg_request_irq"} */
488 }
489
490 /* AUX_FUNC ldv_platform_instance_12 */
491 void *ldv_platform_instance_12(void *arg0) {
492 /* LDV {"thread": 13, "type": "CONTROL_FUNCTION_BEGIN", "comment": "Invoke platfrom callbacks. (Relevant to 'dnet_driver')", "function": "ldv_platform_instance_12"} */
493 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
494 struct platform_device *ldv_12_resource;
495 struct platform_driver *ldv_12_container = ldv_emg_alias_dnet_driver_2;
496 int ldv_12_probed = 1;
497 /* Received labels */
498 struct ldv_struct_platform_instance_12 *data = (struct ldv_struct_platform_instance_12*) arg0;
499
500 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
501 /* Initialize automaton variables */
502 ldv_12_probed = 1;
503 /* LDV {"action": "REGISTER", "type": "RECEIVE_BEGIN", "comment": "Register a driver callbacks for platform-level device."} */
504 /* Assign recieved labels */
505 if (data) {
506 ldv_12_container = data->arg0;
507 ldv_free(data);
508 }
509 /* LDV {"action": "REGISTER", "type": "RECEIVE_END"} */
510
511 /* LDV {"action": "INIT", "type": "CONDITION_BEGIN", "comment": "Alloc memory for 'platform_device' structure."} */
512 ldv_12_resource = ldv_xmalloc_unknown_size(0);
513 /* LDV {"action": "INIT", "type": "CONDITION_END"} */
514
515 /* LDV {"action": "MAIN", "type": "SUBPROCESS_BEGIN", "comment": "Check that device is truely in the system and begin callback invocations."} */
516 /* LDV {"action": "MAIN", "type": "SUBPROCESS_END"} */
517
518 /* Jump to a subprocess 'main' initial state */
519 goto ldv_main_12;
520 /* End of the process */
521 return 0;
522
523 /* Sbprocess main */
524 ldv_main_12:
525 /* LDV {"action": null, "type": "ARTIFICIAL", "comment": "Artificial state in scenario"} */
526
527 if (ldv_undef_int()) {
528 /* LDV {"action": "PROBE_3", "type": "CALL_BEGIN", "callback": true, "comment": "Check that the device in the system and do driver initializations. Invoke callback probe from platform_driver."} */
529 /* Callback pre-call */
530 ldv_pre_probe();
531 /* LDV {"type": "CALLBACK", "call": "ldv_12_probed = ldv_emg_wrapper_dnet_probe_2(ldv_12_resource);", "comment": "probe"} */
532 ldv_12_probed = ldv_emg_wrapper_dnet_probe_2(ldv_12_resource);
533 /* Callback post-call */
534 ldv_12_probed = ldv_post_probe(ldv_12_probed);
535 /* LDV {"action": "PROBE_3", "type": "CALL_END"} */
536
537 if (ldv_undef_int()) {
538 /* LDV {"action": "POSITIVE_PROBE", "type": "CONDITION_BEGIN", "comment": "Platform device is probed successfully now."} */
539 ldv_assume(ldv_12_probed == 0);
540 /* LDV {"action": "POSITIVE_PROBE", "type": "CONDITION_END"} */
541
542 /* LDV {"action": "CALL", "type": "SUBPROCESS_BEGIN", "comment": "Driver is probed. Call power management callbacks or release the device."} */
543 /* LDV {"action": "CALL", "type": "SUBPROCESS_END"} */
544
545 /* Jump to a subprocess 'call' initial state */
546 goto ldv_call_12;
547 }
548 else {
549 /* LDV {"action": "NEGATIVE_PROBE", "type": "CONDITION_BEGIN", "comment": "Failed to probe the device."} */
550 ldv_assume(ldv_12_probed != 0);
551 /* LDV {"action": "NEGATIVE_PROBE", "type": "CONDITION_END"} */
552
553 /* LDV {"action": "MAIN", "type": "SUBPROCESS_BEGIN", "comment": "Check that device is truely in the system and begin callback invocations."} */
554 /* LDV {"action": "MAIN", "type": "SUBPROCESS_END"} */
555
556 /* Jump to a subprocess 'main' initial state */
557 goto ldv_main_12;
558 }
559 }
560 else {
561 /* LDV {"action": "FREE", "type": "CONDITION_BEGIN", "comment": "Free memory for 'platform_device' structure."} */
562 ldv_free(ldv_12_resource);
563 /* LDV {"action": "FREE", "type": "CONDITION_END"} */
564
565 /* LDV {"action": "DEREGISTER", "type": "RECEIVE_BEGIN", "comment": "Finish PLATFORM callbacks invocations scenario."} */
566 /* Skip a non-replicative signal receiving */
567 /* LDV {"action": "DEREGISTER", "type": "RECEIVE_END"} */
568
569 /* Exit function at a terminal state */
570 return 0;
571 }
572 /* End of the subprocess 'main' */
573 return 0;
574
575 /* Sbprocess call */
576 ldv_call_12:
577 /* LDV {"action": null, "type": "ARTIFICIAL", "comment": "Artificial state in scenario"} */
578
579 switch (ldv_undef_int()) {
580 case 1: {
581 /* LDV {"action": "CALLBACK_2", "type": "CONDITION_BEGIN", "comment": "No callbacks implemented to call here"} */
582 /* Skip callback without implementations */
583 /* LDV {"action": "CALLBACK_2", "type": "CONDITION_END"} */
584
585 /* LDV {"action": "CALL", "type": "SUBPROCESS_BEGIN", "comment": "Driver is probed. Call power management callbacks or release the device."} */
586 /* LDV {"action": "CALL", "type": "SUBPROCESS_END"} */
587
588 /* Jump to a subprocess 'call' initial state */
589 goto ldv_call_12;
590 break;
591 }
592 case 2: {
593 /* LDV {"action": "PM_REGISTER", "type": "DISPATCH_BEGIN", "comment": "Proceed to a power management scenario."} */
594 ldv_dispatch_pm_register_12_13();
595 /* LDV {"action": "PM_REGISTER", "type": "DISPATCH_END"} */
596
597 /* LDV {"action": "PM_DEREGISTER", "type": "DISPATCH_BEGIN", "comment": "Finish the power management scenario."} */
598 ldv_dispatch_pm_deregister_12_12();
599 /* LDV {"action": "PM_DEREGISTER", "type": "DISPATCH_END"} */
600
601 /* LDV {"action": "CALL", "type": "SUBPROCESS_BEGIN", "comment": "Driver is probed. Call power management callbacks or release the device."} */
602 /* LDV {"action": "CALL", "type": "SUBPROCESS_END"} */
603
604 /* Jump to a subprocess 'call' initial state */
605 goto ldv_call_12;
606 break;
607 }
608 case 3: {
609 /* LDV {"action": "RELEASE_4", "type": "CALL_BEGIN", "callback": true, "comment": "Remove device from the system. Invoke callback remove from platform_driver."} */
610 /* LDV {"type": "CALLBACK", "call": "ldv_emg_wrapper_dnet_remove_3(ldv_12_resource);", "comment": "release"} */
611 ldv_emg_wrapper_dnet_remove_3(ldv_12_resource);
612 /* LDV {"action": "RELEASE_4", "type": "CALL_END"} */
613
614 /* LDV {"action": "AFTER_RELEASE", "type": "CONDITION_BEGIN", "comment": "Platform device is released now."} */
615 ldv_12_probed = 1;
616 /* LDV {"action": "AFTER_RELEASE", "type": "CONDITION_END"} */
617
618 /* LDV {"action": "MAIN", "type": "SUBPROCESS_BEGIN", "comment": "Check that device is truely in the system and begin callback invocations."} */
619 /* LDV {"action": "MAIN", "type": "SUBPROCESS_END"} */
620
621 /* Jump to a subprocess 'main' initial state */
622 goto ldv_main_12;
623 break;
624 }
625 default: ldv_assume(0);
626 }
627 /* End of the subprocess 'call' */
628 return 0;
629 /* LDV {"comment": "End of control function based on process 'platform_instance(platform)'", "type": "CONTROL_FUNCTION_END", "function": "ldv_platform_instance_12"} */
630 }
631
632 /* AUX_FUNC ldv_random_allocationless_scenario_11 */
633 void *ldv_random_allocationless_scenario_11(void *arg0) {
634 /* LDV {"thread": 12, "type": "CONTROL_FUNCTION_BEGIN", "comment": "Invoke callbacks randomly without parameters allocation. (Relevant to '& dnet_get_drvinfo' '& ethtool_op_get_link' '& ethtool_op_get_ts_info')", "function": "ldv_random_allocationless_scenario_11"} */
635 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
636 struct ifreq *ldv_11_ldv_param_1_5;
637 struct sk_buff *ldv_11_ldv_param_0_9;
638 struct ethtool_drvinfo *ldv_11_ldv_param_1_2;
639 struct ethtool_ts_info *ldv_11_ldv_param_1_3;
640 struct ethtool_link_ksettings *ldv_11_ldv_param_1_4;
641 int ldv_11_ldv_param_2_6;
642 struct ethtool_link_ksettings *ldv_11_ldv_param_1_7;
643 struct net_device *ldv_11_container;
644 void *ldv_11_ldv_param_1_8;
645 /* Received labels */
646 struct ldv_struct_random_allocationless_scenario_11 *data = (struct ldv_struct_random_allocationless_scenario_11*) arg0;
647
648 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
649 /* LDV {"action": "REGISTER", "type": "RECEIVE_BEGIN", "comment": "Begin NET callbacks invocations scenario."} */
650 /* Assign recieved labels */
651 if (data) {
652 ldv_11_container = data->arg0;
653 ldv_free(data);
654 }
655 /* LDV {"action": "REGISTER", "type": "RECEIVE_END"} */
656
657 /* LDV {"action": "CALL", "type": "SUBPROCESS_BEGIN", "comment": "Prepare to call a random callback or deregister the callbacks."} */
658 /* LDV {"action": "CALL", "type": "SUBPROCESS_END"} */
659
660 /* Jump to a subprocess 'call' initial state */
661 goto ldv_call_11;
662 /* End of the process */
663 return 0;
664
665 /* Sbprocess call */
666 ldv_call_11:
667 /* LDV {"action": null, "type": "ARTIFICIAL", "comment": "Artificial state in scenario"} */
668
669 if (ldv_undef_int()) {
670 /* LDV {"action": "PRE_CALL_2", "type": "CONDITION_BEGIN", "comment": "Allocate memory for adhoc callback parameters."} */
671 ldv_11_ldv_param_1_2 = ldv_xmalloc_unknown_size(0);
672 /* LDV {"action": "PRE_CALL_2", "type": "CONDITION_END"} */
673
674 switch (ldv_undef_int()) {
675 case 1: {
676 /* LDV {"action": "CALLBACK_4", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback get_drvinfo from ethtool_ops."} */
677 /* LDV {"type": "CALLBACK", "call": "ldv_emg_wrapper_dnet_get_drvinfo_2(ldv_11_container, ldv_11_ldv_param_1_2);", "comment": "callback"} */
678 ldv_emg_wrapper_dnet_get_drvinfo_2(ldv_11_container, ldv_11_ldv_param_1_2);
679 /* LDV {"action": "CALLBACK_4", "type": "CALL_END"} */
680
681 break;
682 }
683 case 2: {
684 /* LDV {"action": "PRE_CALL_23", "type": "CONDITION_BEGIN", "comment": "Allocate memory for adhoc callback parameters."} */
685 ldv_11_ldv_param_0_9 = ldv_xmalloc_unknown_size(0);
686 /* LDV {"action": "PRE_CALL_23", "type": "CONDITION_END"} */
687
688 /* LDV {"action": "CALLBACK_25", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback ndo_start_xmit from net_device_ops."} */
689 /* LDV {"type": "CALLBACK", "call": "ldv_emg_wrapper_dnet_start_xmit_11(ldv_11_ldv_param_0_9, ldv_11_container);", "comment": "callback"} */
690 ldv_emg_wrapper_dnet_start_xmit_11(ldv_11_ldv_param_0_9, ldv_11_container);
691 /* LDV {"action": "CALLBACK_25", "type": "CALL_END"} */
692
693 /* LDV {"action": "POST_CALL_24", "type": "CONDITION_BEGIN", "comment": "Free memory of adhoc callback parameters."} */
694 ldv_free(ldv_11_ldv_param_0_9);
695 /* LDV {"action": "POST_CALL_24", "type": "CONDITION_END"} */
696
697 break;
698 }
699 case 3: {
700 /* LDV {"action": "PRE_CALL_20", "type": "CONDITION_BEGIN", "comment": "Allocate memory for adhoc callback parameters."} */
701 ldv_11_ldv_param_1_8 = ldv_xmalloc_unknown_size(0);
702 /* LDV {"action": "PRE_CALL_20", "type": "CONDITION_END"} */
703
704 /* LDV {"action": "CALLBACK_22", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback ndo_set_mac_address from net_device_ops."} */
705 /* LDV {"type": "CALLBACK", "call": "ldv_emg_alias_eth_mac_addr_10(ldv_11_container, ldv_11_ldv_param_1_8);", "comment": "callback"} */
706 ldv_emg_alias_eth_mac_addr_10(ldv_11_container, ldv_11_ldv_param_1_8);
707 /* LDV {"action": "CALLBACK_22", "type": "CALL_END"} */
708
709 /* LDV {"action": "POST_CALL_21", "type": "CONDITION_BEGIN", "comment": "Free memory of adhoc callback parameters."} */
710 ldv_free(ldv_11_ldv_param_1_8);
711 /* LDV {"action": "POST_CALL_21", "type": "CONDITION_END"} */
712
713 break;
714 }
715 case 4: {
716 /* LDV {"action": "CALLBACK_19", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback ndo_get_stats from net_device_ops."} */
717 /* LDV {"type": "CALLBACK", "call": "ldv_emg_wrapper_dnet_get_stats_9(ldv_11_container);", "comment": "callback"} */
718 ldv_emg_wrapper_dnet_get_stats_9(ldv_11_container);
719 /* LDV {"action": "CALLBACK_19", "type": "CALL_END"} */
720
721 break;
722 }
723 case 5: {
724 /* LDV {"action": "CALLBACK_18", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback ndo_validate_addr from net_device_ops."} */
725 /* LDV {"type": "CALLBACK", "call": "ldv_emg_alias_eth_validate_addr_8(ldv_11_container);", "comment": "callback"} */
726 ldv_emg_alias_eth_validate_addr_8(ldv_11_container);
727 /* LDV {"action": "CALLBACK_18", "type": "CALL_END"} */
728
729 break;
730 }
731 case 6: {
732 /* LDV {"action": "PRE_CALL_15", "type": "CONDITION_BEGIN", "comment": "Allocate memory for adhoc callback parameters."} */
733 ldv_11_ldv_param_1_7 = ldv_xmalloc_unknown_size(0);
734 /* LDV {"action": "PRE_CALL_15", "type": "CONDITION_END"} */
735
736 /* LDV {"action": "CALLBACK_17", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback set_link_ksettings from ethtool_ops."} */
737 /* LDV {"type": "CALLBACK", "call": "ldv_emg_alias_phy_ethtool_set_link_ksettings_7(ldv_11_container, ldv_11_ldv_param_1_7);", "comment": "callback"} */
738 ldv_emg_alias_phy_ethtool_set_link_ksettings_7(ldv_11_container, ldv_11_ldv_param_1_7);
739 /* LDV {"action": "CALLBACK_17", "type": "CALL_END"} */
740
741 /* LDV {"action": "POST_CALL_16", "type": "CONDITION_BEGIN", "comment": "Free memory of adhoc callback parameters."} */
742 ldv_free(ldv_11_ldv_param_1_7);
743 /* LDV {"action": "POST_CALL_16", "type": "CONDITION_END"} */
744
745 break;
746 }
747 case 7: {
748 /* LDV {"action": "PRE_CALL_12", "type": "CONDITION_BEGIN", "comment": "Allocate memory for adhoc callback parameters."} */
749 ldv_11_ldv_param_1_5 = ldv_xmalloc_unknown_size(0);
750 /* LDV {"action": "PRE_CALL_12", "type": "CONDITION_END"} */
751
752 /* LDV {"action": "CALLBACK_14", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback ndo_do_ioctl from net_device_ops."} */
753 /* LDV {"type": "CALLBACK", "call": "ldv_emg_wrapper_dnet_ioctl_6(ldv_11_container, ldv_11_ldv_param_1_5, ldv_11_ldv_param_2_6);", "comment": "callback"} */
754 ldv_emg_wrapper_dnet_ioctl_6(ldv_11_container, ldv_11_ldv_param_1_5, ldv_11_ldv_param_2_6);
755 /* LDV {"action": "CALLBACK_14", "type": "CALL_END"} */
756
757 /* LDV {"action": "POST_CALL_13", "type": "CONDITION_BEGIN", "comment": "Free memory of adhoc callback parameters."} */
758 ldv_free(ldv_11_ldv_param_1_5);
759 /* LDV {"action": "POST_CALL_13", "type": "CONDITION_END"} */
760
761 break;
762 }
763 case 8: {
764 /* LDV {"action": "PRE_CALL_9", "type": "CONDITION_BEGIN", "comment": "Allocate memory for adhoc callback parameters."} */
765 ldv_11_ldv_param_1_4 = ldv_xmalloc_unknown_size(0);
766 /* LDV {"action": "PRE_CALL_9", "type": "CONDITION_END"} */
767
768 /* LDV {"action": "CALLBACK_11", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback get_link_ksettings from ethtool_ops."} */
769 /* LDV {"type": "CALLBACK", "call": "ldv_emg_alias_phy_ethtool_get_link_ksettings_5(ldv_11_container, ldv_11_ldv_param_1_4);", "comment": "callback"} */
770 ldv_emg_alias_phy_ethtool_get_link_ksettings_5(ldv_11_container, ldv_11_ldv_param_1_4);
771 /* LDV {"action": "CALLBACK_11", "type": "CALL_END"} */
772
773 /* LDV {"action": "POST_CALL_10", "type": "CONDITION_BEGIN", "comment": "Free memory of adhoc callback parameters."} */
774 ldv_free(ldv_11_ldv_param_1_4);
775 /* LDV {"action": "POST_CALL_10", "type": "CONDITION_END"} */
776
777 break;
778 }
779 case 9: {
780 /* LDV {"action": "PRE_CALL_6", "type": "CONDITION_BEGIN", "comment": "Allocate memory for adhoc callback parameters."} */
781 ldv_11_ldv_param_1_3 = ldv_xmalloc_unknown_size(0);
782 /* LDV {"action": "PRE_CALL_6", "type": "CONDITION_END"} */
783
784 /* LDV {"action": "CALLBACK_8", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback get_ts_info from ethtool_ops."} */
785 /* LDV {"type": "CALLBACK", "call": "ldv_emg_alias_ethtool_op_get_ts_info_4(ldv_11_container, ldv_11_ldv_param_1_3);", "comment": "callback"} */
786 ldv_emg_alias_ethtool_op_get_ts_info_4(ldv_11_container, ldv_11_ldv_param_1_3);
787 /* LDV {"action": "CALLBACK_8", "type": "CALL_END"} */
788
789 /* LDV {"action": "POST_CALL_7", "type": "CONDITION_BEGIN", "comment": "Free memory of adhoc callback parameters."} */
790 ldv_free(ldv_11_ldv_param_1_3);
791 /* LDV {"action": "POST_CALL_7", "type": "CONDITION_END"} */
792
793 break;
794 }
795 case 10: {
796 /* LDV {"action": "CALLBACK_5", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback get_link from ethtool_ops."} */
797 /* LDV {"type": "CALLBACK", "call": "ldv_emg_alias_ethtool_op_get_link_3(ldv_11_container);", "comment": "callback"} */
798 ldv_emg_alias_ethtool_op_get_link_3(ldv_11_container);
799 /* LDV {"action": "CALLBACK_5", "type": "CALL_END"} */
800
801 break;
802 }
803 default: ldv_assume(0);
804 }
805 /* LDV {"action": "POST_CALL_3", "type": "CONDITION_BEGIN", "comment": "Free memory of adhoc callback parameters."} */
806 ldv_free(ldv_11_ldv_param_1_2);
807 /* LDV {"action": "POST_CALL_3", "type": "CONDITION_END"} */
808
809 /* LDV {"action": "CALL", "type": "SUBPROCESS_BEGIN", "comment": "Prepare to call a random callback or deregister the callbacks."} */
810 /* LDV {"action": "CALL", "type": "SUBPROCESS_END"} */
811
812 /* Jump to a subprocess 'call' initial state */
813 goto ldv_call_11;
814 }
815 else {
816 /* LDV {"action": "DEREGISTER", "type": "RECEIVE_BEGIN", "comment": "Finish NET callbacks invocations scenario."} */
817 /* Skip a non-replicative signal receiving */
818 /* LDV {"action": "DEREGISTER", "type": "RECEIVE_END"} */
819
820 /* Exit function at a terminal state */
821 return 0;
822 }
823 /* End of the subprocess 'call' */
824 return 0;
825 /* LDV {"comment": "End of control function based on process 'random_allocationless_scenario(net)'", "type": "CONTROL_FUNCTION_END", "function": "ldv_random_allocationless_scenario_11"} */
826 }
827
828 /* AUX_FUNC ldv_initialization_1 */
829 void *ldv_initialization_1(void *arg0) {
830 /* LDV {"thread": 2, "type": "CONTROL_FUNCTION_BEGIN", "comment": "Initialize or exit module.", "function": "ldv_initialization_1"} */
831 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
832 int ldv_1_ret;
833 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
834 /* LDV {"action": "DNET_DRIVER_INIT", "type": "CALL_BEGIN", "callback": true, "comment": "Initialize the module after insmod with 'dnet_driver_init' function."} */
835 /* LDV {"type": "CALLBACK", "call": "dnet_driver_init();", "comment": "dnet_driver_init"} */
836 ldv_1_ret = ldv_emg_dnet_driver_init();
837 ldv_1_ret = ldv_post_init(ldv_1_ret);
838 /* LDV {"action": "DNET_DRIVER_INIT", "type": "CALL_END"} */
839
840 if (ldv_undef_int()) {
841 /* LDV {"action": "INIT_FAILED", "type": "CONDITION_BEGIN", "comment": "Failed to initialize the module."} */
842 ldv_assume(ldv_1_ret != 0);
843 /* LDV {"action": "INIT_FAILED", "type": "CONDITION_END"} */
844
845 /* Exit function at a terminal state */
846 return 0;
847 }
848 else {
849 /* LDV {"action": "INIT_SUCCESS", "type": "CONDITION_BEGIN", "comment": "Module has been initialized."} */
850 ldv_assume(ldv_1_ret == 0);
851 /* LDV {"action": "INIT_SUCCESS", "type": "CONDITION_END"} */
852
853 /* LDV {"action": "DNET_DRIVER_EXIT", "type": "CALL_BEGIN", "callback": true, "comment": "Exit the module before its unloading with 'dnet_driver_exit' function."} */
854 /* LDV {"type": "CALLBACK", "call": "dnet_driver_exit();", "comment": "dnet_driver_exit"} */
855 ldv_emg_dnet_driver_exit();
856 /* LDV {"action": "DNET_DRIVER_EXIT", "type": "CALL_END"} */
857
858 /* Exit function at a terminal state */
859 return 0;
860 }
861 /* End of the process */
862 return 0;
863 /* LDV {"comment": "End of control function based on process 'initialization(linux)'", "type": "CONTROL_FUNCTION_END", "function": "ldv_initialization_1"} */
864 }
865
866 /* AUX_FUNC ldv_dispatch_irq_register_9_3 */
867 void ldv_dispatch_irq_register_9_3(int arg0, enum irqreturn (*arg1)(int, void *), enum irqreturn (*arg2)(int, void *), void *arg3) {
868 int ret;
869 struct ldv_struct_interrupt_scenario_13 *cf_arg_13;
870 switch (ldv_undef_int()) {
871 case 0: {
872 cf_arg_13 = ldv_xmalloc(sizeof(struct ldv_struct_interrupt_scenario_13));
873 cf_arg_13->arg0 = arg0;
874 cf_arg_13->arg1 = arg1;
875 cf_arg_13->arg2 = arg2;
876 cf_arg_13->arg3 = arg3;
877 ret = pthread_create(& ldv_thread_13, 0, ldv_interrupt_scenario_13, cf_arg_13);
878 ldv_assume(ret == 0);
879 break;
880 };
881 default: ldv_assume(0);
882 };
883 return;
884 }
885
886 /* AUX_FUNC ldv_interrupt_scenario_13 */
887 void *ldv_interrupt_scenario_13(void *arg0) {
888 /* LDV {"thread": 14, "type": "CONTROL_FUNCTION_BEGIN", "comment": "Handle an interrupt. (Relevant to 'dnet_interrupt')", "function": "ldv_interrupt_scenario_13"} */
889 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
890 enum irqreturn ldv_13_ret_val;
891 int ldv_13_line;
892 void *ldv_13_data;
893 enum irqreturn (*ldv_13_callback)(int, void *) = &ldv_emg_wrapper_dnet_interrupt_2;
894 enum irqreturn (*ldv_13_thread)(int, void *);
895 /* Received labels */
896 struct ldv_struct_interrupt_scenario_13 *data = (struct ldv_struct_interrupt_scenario_13*) arg0;
897
898 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
899 /* LDV {"action": "IRQ_REGISTER", "type": "RECEIVE_BEGIN", "comment": "An interrupt is registered."} */
900 /* Assign recieved labels */
901 if (data) {
902 ldv_13_line = data->arg0;
903 ldv_13_callback = data->arg1;
904 ldv_13_thread = data->arg2;
905 ldv_13_data = data->arg3;
906 ldv_free(data);
907 }
908 /* LDV {"action": "IRQ_REGISTER", "type": "RECEIVE_END"} */
909
910 /* LDV {"action": "HANDLER_2", "type": "CALL_BEGIN", "callback": true, "comment": "An interrupt happens, execute the bottom half function to handle it. Invoke callback handler from INTERRUPT."} */
911 /* Callback pre-call */
912 ldv_switch_to_interrupt_context();
913 /* LDV {"type": "CALLBACK", "call": "ldv_13_ret_val = ldv_emg_wrapper_dnet_interrupt_2(ldv_13_line, ldv_13_data);", "comment": "handler"} */
914 ldv_13_ret_val = ldv_emg_wrapper_dnet_interrupt_2(ldv_13_line, ldv_13_data);
915 /* Callback post-call */
916 ldv_switch_to_process_context();
917 /* LDV {"action": "HANDLER_2", "type": "CALL_END"} */
918
919 if (ldv_undef_int()) {
920 /* LDV {"action": "NEED_THREAD", "type": "CONDITION_BEGIN", "comment": "Wake a thread to continue an interrupt handling."} */
921 ldv_assume(ldv_13_ret_val == IRQ_WAKE_THREAD);
922 /* LDV {"action": "NEED_THREAD", "type": "CONDITION_END"} */
923
924 /* LDV {"action": "THREAD_3", "type": "CALL_BEGIN", "callback": true, "comment": "Proceed with the interrupt handling, execute the top half function. Invoke callback thread from INTERRUPT."} */
925 if (ldv_13_thread) {
926 /* LDV {"type": "CALLBACK", "call": "ldv_13_thread(ldv_13_line, ldv_13_data);", "comment": "thread"} */
927 ldv_13_thread(ldv_13_line, ldv_13_data);
928 }
929 /* LDV {"action": "THREAD_3", "type": "CALL_END"} */
930
931 }
932 else {
933 /* LDV {"action": "HANDLED", "type": "CONDITION_BEGIN", "comment": "An interrupt has been handled."} */
934 ldv_assume(ldv_13_ret_val != IRQ_WAKE_THREAD);
935 /* LDV {"action": "HANDLED", "type": "CONDITION_END"} */
936
937 }
938 /* LDV {"action": "IRQ_DEREGISTER", "type": "RECEIVE_BEGIN", "comment": "An interrupt is deregistered."} */
939 /* Skip a non-replicative signal receiving */
940 /* LDV {"action": "IRQ_DEREGISTER", "type": "RECEIVE_END"} */
941
942 /* Exit function at a terminal state */
943 return 0;
944 /* End of the process */
945 return 0;
946 /* LDV {"comment": "End of control function based on process 'interrupt_scenario(interrupt)'", "type": "CONTROL_FUNCTION_END", "function": "ldv_interrupt_scenario_13"} */
947 }
948
949 /* AUX_FUNC ldv_dispatch_deregister_4_1 */
950 void ldv_dispatch_deregister_4_1(struct platform_driver *arg0) {
951 int ret;
952 struct ldv_struct_platform_instance_12 *cf_arg_12;
953 switch (ldv_undef_int()) {
954 case 0: {
955 ret = pthread_join(ldv_thread_12, 0);
956 ldv_assume(ret == 0);
957 break;
958 };
959 default: ldv_assume(0);
960 };
961 return;
962 }
963
964 /* AUX_FUNC ldv_dispatch_pm_deregister_12_12 */
965 void ldv_dispatch_pm_deregister_12_12(void) {
966 int ret;
967 struct ldv_struct_platform_instance_12 *cf_arg_10;
968 switch (ldv_undef_int()) {
969 case 0: {
970 ret = pthread_join(ldv_thread_10, 0);
971 ldv_assume(ret == 0);
972 break;
973 };
974 default: ldv_assume(0);
975 };
976 return;
977 }
978
979 /* AUX_FUNC ldv_dispatch_pm_register_12_13 */
980 void ldv_dispatch_pm_register_12_13(void) {
981 int ret;
982 struct ldv_struct_platform_instance_12 *cf_arg_10;
983 switch (ldv_undef_int()) {
984 case 0: {
985 cf_arg_10 = ldv_xmalloc(sizeof(struct ldv_struct_platform_instance_12));
986 ret = pthread_create(& ldv_thread_10, 0, ldv_pm_ops_scenario_10, cf_arg_10);
987 ldv_assume(ret == 0);
988 break;
989 };
990 default: ldv_assume(0);
991 };
992 return;
993 }
994
995 /* AUX_FUNC ldv_emg_unregister_netdev */
996 void ldv_emg_unregister_netdev(struct net_device *arg0) {
997 /* LDV {"comment": "Deregister network device and its callbacks. (Relevant to '& dnet_close')", "type": "CONTROL_FUNCTION_BEGIN", "function": "ldv_emg_unregister_netdev"} */
998 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
999 struct net_device *ldv_6_netdev;
1000 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
1001 /* LDV {"action": "ASSIGN", "type": "CONDITION_BEGIN", "comment": "Get network device structure."} */
1002 ldv_6_netdev = arg0;
1003 /* LDV {"action": "ASSIGN", "type": "CONDITION_END"} */
1004
1005 /* LDV {"action": "STOP_2", "type": "CALL_BEGIN", "callback": true, "comment": "Switch network device to the down state. Invoke callback ndo_stop from net_device_ops."} */
1006 /* LDV {"type": "CALLBACK", "call": "ldv_emg_wrapper_dnet_close_2(ldv_6_netdev);", "comment": "stop"} */
1007 ldv_emg_wrapper_dnet_close_2(ldv_6_netdev);
1008 /* LDV {"action": "STOP_2", "type": "CALL_END"} */
1009
1010 /* LDV {"action": "DEREGISTER", "type": "DISPATCH_BEGIN", "comment": "Deregiste of the network device has finished."} */
1011 ldv_dispatch_deregister_6_1(ldv_6_netdev);
1012 /* LDV {"action": "DEREGISTER", "type": "DISPATCH_END"} */
1013
1014 /* Exit function at a terminal state */
1015 return;
1016 /* End of the process */
1017 return;
1018 /* LDV {"comment": "End of control function based on process 'unregister_netdev'", "type": "CONTROL_FUNCTION_END", "function": "ldv_emg_unregister_netdev"} */
1019 }
1020
1021 /* AUX_FUNC ldv_emg_free_irq */
1022 void *ldv_emg_free_irq(unsigned int arg0, void *arg1) {
1023 /* LDV {"comment": "Free an interrupt.", "type": "CONTROL_FUNCTION_BEGIN", "function": "ldv_emg_free_irq"} */
1024 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
1025 int ldv_3_line;
1026 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
1027 /* LDV {"action": "ASSIGN", "type": "CONDITION_BEGIN", "comment": "Get an interrupt line argument."} */
1028 ldv_3_line = arg0;
1029 /* LDV {"action": "ASSIGN", "type": "CONDITION_END"} */
1030
1031 /* LDV {"action": "IRQ_DEREGISTER", "type": "DISPATCH_BEGIN", "comment": "The interrupt line is freed."} */
1032 ldv_dispatch_irq_deregister_3_1(ldv_3_line);
1033 /* LDV {"action": "IRQ_DEREGISTER", "type": "DISPATCH_END"} */
1034
1035 /* Exit function at a terminal state */
1036 /* End of the process */
1037 /* LDV {"comment": "End of control function based on process 'free_irq'", "type": "CONTROL_FUNCTION_END", "function": "ldv_emg_free_irq"} */
1038 }
1039
1040 /* AUX_FUNC ldv_dispatch_deregister_6_1 */
1041 void ldv_dispatch_deregister_6_1(struct net_device *arg0) {
1042 int ret;
1043 struct ldv_struct_random_allocationless_scenario_11 *cf_arg_11;
1044 switch (ldv_undef_int()) {
1045 case 0: {
1046 ret = pthread_join(ldv_thread_11, 0);
1047 ldv_assume(ret == 0);
1048 break;
1049 };
1050 default: ldv_assume(0);
1051 };
1052 return;
1053 }
1054
1055 /* AUX_FUNC ldv_emg_free_netdev */
1056 void ldv_emg_free_netdev(struct net_device *arg0) {
1057 /* LDV {"comment": "Free memory of a network device.", "type": "CONTROL_FUNCTION_BEGIN", "function": "ldv_emg_free_netdev"} */
1058 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
1059 struct net_device *ldv_2_netdev;
1060 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
1061 /* LDV {"action": "FREE", "type": "CONDITION_BEGIN", "comment": "Freeing memory of a network device."} */
1062 ldv_2_netdev = arg0;
1063 ldv_free(ldv_2_netdev);
1064 /* LDV {"action": "FREE", "type": "CONDITION_END"} */
1065
1066 /* Exit function at a terminal state */
1067 return;
1068 /* End of the process */
1069 return;
1070 /* LDV {"comment": "End of control function based on process 'free_netdev'", "type": "CONTROL_FUNCTION_END", "function": "ldv_emg_free_netdev"} */
1071 }
1072
1073 /* AUX_FUNC ldv_emg___platform_driver_register */
1074 int ldv_emg___platform_driver_register(struct platform_driver *arg0, struct module *arg1) {
1075 /* LDV {"comment": "Register a driver for platform-level device. (Relevant to 'dnet_driver')", "type": "CONTROL_FUNCTION_BEGIN", "function": "ldv_emg___platform_driver_register"} */
1076 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
1077 struct platform_driver *ldv_7_platform_driver = ldv_emg_alias_dnet_driver_2;
1078 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
1079 /* LDV {"action": null, "type": "ARTIFICIAL", "comment": "Artificial state in scenario"} */
1080
1081 if (ldv_undef_int()) {
1082 /* LDV {"action": "ASSIGN", "type": "CONDITION_BEGIN", "comment": "Get platform_driver structure argument."} */
1083 ldv_7_platform_driver = arg0;
1084 /* LDV {"action": "ASSIGN", "type": "CONDITION_END"} */
1085
1086 /* LDV {"action": "REGISTER", "type": "DISPATCH_BEGIN", "comment": "Register platform_driver callbacks."} */
1087 ldv_dispatch_register_7_3(ldv_7_platform_driver);
1088 /* LDV {"action": "REGISTER", "type": "DISPATCH_END"} */
1089
1090 /* LDV {"action": "SUCCESS", "type": "CONDITION_BEGIN", "comment": "Successfully registered a driver for platform-level device."} */
1091 return 0;
1092 /* LDV {"action": "SUCCESS", "type": "CONDITION_END"} */
1093
1094 /* Exit function at a terminal state */
1095 }
1096 else {
1097 /* LDV {"action": "FAIL", "type": "CONDITION_BEGIN", "comment": "Fail to register a driver for platform-level device."} */
1098 return ldv_undef_int_negative();
1099 /* LDV {"action": "FAIL", "type": "CONDITION_END"} */
1100
1101 /* Exit function at a terminal state */
1102 }
1103 /* End of the process */
1104 /* LDV {"comment": "End of control function based on process '__platform_driver_register'", "type": "CONTROL_FUNCTION_END", "function": "ldv_emg___platform_driver_register"} */
1105 }
1106
1107 /* AUX_FUNC ldv_emg_register_netdev */
1108 int ldv_emg_register_netdev(struct net_device *arg0) {
1109 /* LDV {"comment": "Register network device and its callbacks. (Relevant to '& dnet_open')", "type": "CONTROL_FUNCTION_BEGIN", "function": "ldv_emg_register_netdev"} */
1110 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
1111 struct net_device *ldv_8_netdev;
1112 int ldv_8_ret = ldv_undef_int();
1113 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
1114 /* Initialize automaton variables */
1115 ldv_8_ret = ldv_undef_int();
1116 /* LDV {"action": null, "type": "ARTIFICIAL", "comment": "Artificial state in scenario"} */
1117
1118 if (ldv_undef_int()) {
1119 /* LDV {"action": "ASSIGN", "type": "CONDITION_BEGIN", "comment": "Get network device structure."} */
1120 ldv_8_netdev = arg0;
1121 /* LDV {"action": "ASSIGN", "type": "CONDITION_END"} */
1122
1123 /* LDV {"action": "OPEN_2", "type": "CALL_BEGIN", "callback": true, "comment": "Switch network device to the up state. Invoke callback ndo_open from net_device_ops."} */
1124 /* LDV {"type": "CALLBACK", "call": "ldv_8_ret = ldv_emg_wrapper_dnet_open_2(ldv_8_netdev);", "comment": "open"} */
1125 ldv_8_ret = ldv_emg_wrapper_dnet_open_2(ldv_8_netdev);
1126 /* LDV {"action": "OPEN_2", "type": "CALL_END"} */
1127
1128 if (ldv_undef_int()) {
1129 /* LDV {"action": "OPEN_SUCCESS", "type": "CONDITION_BEGIN", "comment": "Network device is in the up state."} */
1130 ldv_assume(ldv_8_ret == 0);
1131 /* LDV {"action": "OPEN_SUCCESS", "type": "CONDITION_END"} */
1132
1133 /* LDV {"action": "REGISTER", "type": "DISPATCH_BEGIN", "comment": "Register network device callbacks."} */
1134 ldv_dispatch_register_8_4(ldv_8_netdev);
1135 /* LDV {"action": "REGISTER", "type": "DISPATCH_END"} */
1136
1137 /* LDV {"action": "SUCCESS", "type": "CONDITION_BEGIN", "comment": "Registration of the network device has successfully finished."} */
1138 return 0;
1139 /* LDV {"action": "SUCCESS", "type": "CONDITION_END"} */
1140
1141 /* Exit function at a terminal state */
1142 }
1143 else {
1144 /* LDV {"action": "OPEN_FAIL", "type": "CONDITION_BEGIN", "comment": "Open at the registration of the network device has failed."} */
1145 ldv_assume(ldv_8_ret != 0);
1146 ldv_failed_register_netdev();
1147 return ldv_undef_int_negative();
1148 /* LDV {"action": "OPEN_FAIL", "type": "CONDITION_END"} */
1149
1150 /* Exit function at a terminal state */
1151 }
1152 }
1153 else {
1154 /* LDV {"action": "FAIL", "type": "CONDITION_BEGIN", "comment": "Registration of the network device has failed."} */
1155 ldv_failed_register_netdev();
1156 return ldv_undef_int_negative();
1157 /* LDV {"action": "FAIL", "type": "CONDITION_END"} */
1158
1159 /* Exit function at a terminal state */
1160 }
1161 /* End of the process */
1162 /* LDV {"comment": "End of control function based on process 'register_netdev'", "type": "CONTROL_FUNCTION_END", "function": "ldv_emg_register_netdev"} */
1163 }
(2-2/2)