Project

General

Profile

Download (69.3 KB)

Bug #9820 » environment_model2.c

The second 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/netdevice.h>
9 #include <linux/interrupt.h>
10 #include <linux/platform_device.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_12 {
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_11 {
27 struct platform_driver *arg0;
28 int signal_pending;
29 };
30
31 struct ldv_struct_random_scenario_13 {
32 struct net_device *arg0;
33 int signal_pending;
34 };
35
36
37 /* EMG aliases */
38 extern int ldv_emg_wrapper_dnet_ioctl_6(struct net_device *, struct ifreq *, int);
39 extern int ldv_emg_wrapper_dnet_close_2(struct net_device *);
40 extern void ldv_emg_dnet_driver_exit(void);
41 extern int ldv_emg_wrapper_dnet_open_2(struct net_device *);
42 extern int ldv_emg_wrapper_dnet_probe_2(struct platform_device *);
43 extern int (*ldv_emg_alias_eth_validate_addr_8)(struct net_device *);
44 extern int (*ldv_emg_alias_eth_mac_addr_10)(struct net_device *, void *);
45 extern struct platform_driver *ldv_emg_alias_dnet_driver_2;
46 extern int (*ldv_emg_alias_phy_ethtool_get_link_ksettings_5)(struct net_device *, struct ethtool_link_ksettings *);
47 extern int ldv_emg_dnet_driver_init(void);
48 extern int (*ldv_emg_alias_ethtool_op_get_ts_info_4)(struct net_device *, struct ethtool_ts_info *);
49 extern int ldv_emg_wrapper_dnet_remove_3(struct platform_device *);
50 extern int (*ldv_emg_alias_phy_ethtool_set_link_ksettings_7)(struct net_device *, struct ethtool_link_ksettings *);
51 extern void ldv_emg_wrapper_dnet_get_drvinfo_2(struct net_device *, struct ethtool_drvinfo *);
52 extern unsigned int (*ldv_emg_alias_ethtool_op_get_link_3)(struct net_device *);
53 extern struct net_device_stats *ldv_emg_wrapper_dnet_get_stats_9(struct net_device *);
54 extern enum irqreturn ldv_emg_wrapper_dnet_interrupt_2(int, void *);
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_platform_instance_11(void *);
61 void ldv_emg_platform_driver_unregister(struct platform_driver *);
62 void ldv_dispatch_irq_deregister_3_1(int);
63 struct net_device *ldv_emg_alloc_etherdev_mqs(int, unsigned int, unsigned int);
64 void ldv_dispatch_pm_register_11_13(void);
65 void ldv_dispatch_pm_deregister_11_12(void);
66 void ldv_dispatch_register_7_3(struct platform_driver *);
67 int ldv_emg_request_irq(unsigned int, enum irqreturn (*)(int, void *), long unsigned int, char *, void *);
68 void *ldv_random_scenario_13(void *);
69 void *ldv_initialization_1(void *);
70 void ldv_dispatch_irq_register_9_3(int, enum irqreturn (*)(int, void *), enum irqreturn (*)(int, void *), void *);
71 void ldv_dispatch_deregister_4_1(struct platform_driver *);
72 void ldv_dispatch_register_8_4(struct net_device *);
73 void ldv_emg_unregister_netdev(struct net_device *);
74 void *ldv_emg_free_irq(unsigned int, void *);
75 void ldv_dispatch_deregister_6_1(struct net_device *);
76 void ldv_emg_free_netdev(struct net_device *);
77 void *ldv_interrupt_scenario_12(void *);
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_platform_instance_11 */
351 void *ldv_platform_instance_11(void *arg0) {
352 /* LDV {"thread": 12, "type": "CONTROL_FUNCTION_BEGIN", "comment": "Invoke platfrom callbacks. (Relevant to 'dnet_driver')", "function": "ldv_platform_instance_11"} */
353 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
354 struct platform_device *ldv_11_resource;
355 struct platform_driver *ldv_11_container = ldv_emg_alias_dnet_driver_2;
356 int ldv_11_probed = 1;
357 /* Received labels */
358 struct ldv_struct_platform_instance_11 *data = (struct ldv_struct_platform_instance_11*) arg0;
359
360 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
361 /* Initialize automaton variables */
362 ldv_11_probed = 1;
363 /* LDV {"action": "REGISTER", "type": "RECEIVE_BEGIN", "comment": "Register a driver callbacks for platform-level device."} */
364 /* Assign recieved labels */
365 if (data) {
366 ldv_11_container = data->arg0;
367 ldv_free(data);
368 }
369 /* LDV {"action": "REGISTER", "type": "RECEIVE_END"} */
370
371 /* LDV {"action": "INIT", "type": "CONDITION_BEGIN", "comment": "Alloc memory for 'platform_device' structure."} */
372 ldv_11_resource = ldv_xmalloc_unknown_size(0);
373 /* LDV {"action": "INIT", "type": "CONDITION_END"} */
374
375 /* LDV {"action": "MAIN", "type": "SUBPROCESS_BEGIN", "comment": "Check that device is truely in the system and begin callback invocations."} */
376 /* LDV {"action": "MAIN", "type": "SUBPROCESS_END"} */
377
378 /* Jump to a subprocess 'main' initial state */
379 goto ldv_main_11;
380 /* End of the process */
381 return 0;
382
383 /* Sbprocess main */
384 ldv_main_11:
385 /* LDV {"action": null, "type": "ARTIFICIAL", "comment": "Artificial state in scenario"} */
386
387 if (ldv_undef_int()) {
388 /* 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."} */
389 /* Callback pre-call */
390 ldv_pre_probe();
391 /* LDV {"type": "CALLBACK", "call": "ldv_11_probed = ldv_emg_wrapper_dnet_probe_2(ldv_11_resource);", "comment": "probe"} */
392 ldv_11_probed = ldv_emg_wrapper_dnet_probe_2(ldv_11_resource);
393 /* Callback post-call */
394 ldv_11_probed = ldv_post_probe(ldv_11_probed);
395 /* LDV {"action": "PROBE_3", "type": "CALL_END"} */
396
397 if (ldv_undef_int()) {
398 /* LDV {"action": "POSITIVE_PROBE", "type": "CONDITION_BEGIN", "comment": "Platform device is probed successfully now."} */
399 ldv_assume(ldv_11_probed == 0);
400 /* LDV {"action": "POSITIVE_PROBE", "type": "CONDITION_END"} */
401
402 /* LDV {"action": "CALL", "type": "SUBPROCESS_BEGIN", "comment": "Driver is probed. Call power management callbacks or release the device."} */
403 /* LDV {"action": "CALL", "type": "SUBPROCESS_END"} */
404
405 /* Jump to a subprocess 'call' initial state */
406 goto ldv_call_11;
407 }
408 else {
409 /* LDV {"action": "NEGATIVE_PROBE", "type": "CONDITION_BEGIN", "comment": "Failed to probe the device."} */
410 ldv_assume(ldv_11_probed != 0);
411 /* LDV {"action": "NEGATIVE_PROBE", "type": "CONDITION_END"} */
412
413 /* LDV {"action": "MAIN", "type": "SUBPROCESS_BEGIN", "comment": "Check that device is truely in the system and begin callback invocations."} */
414 /* LDV {"action": "MAIN", "type": "SUBPROCESS_END"} */
415
416 /* Jump to a subprocess 'main' initial state */
417 goto ldv_main_11;
418 }
419 }
420 else {
421 /* LDV {"action": "FREE", "type": "CONDITION_BEGIN", "comment": "Free memory for 'platform_device' structure."} */
422 ldv_free(ldv_11_resource);
423 /* LDV {"action": "FREE", "type": "CONDITION_END"} */
424
425 /* LDV {"action": "DEREGISTER", "type": "RECEIVE_BEGIN", "comment": "Finish PLATFORM callbacks invocations scenario."} */
426 /* Skip a non-replicative signal receiving */
427 /* LDV {"action": "DEREGISTER", "type": "RECEIVE_END"} */
428
429 /* Exit function at a terminal state */
430 return 0;
431 }
432 /* End of the subprocess 'main' */
433 return 0;
434
435 /* Sbprocess call */
436 ldv_call_11:
437 /* LDV {"action": null, "type": "ARTIFICIAL", "comment": "Artificial state in scenario"} */
438
439 switch (ldv_undef_int()) {
440 case 1: {
441 /* LDV {"action": "CALLBACK_2", "type": "CONDITION_BEGIN", "comment": "No callbacks implemented to call here"} */
442 /* Skip callback without implementations */
443 /* LDV {"action": "CALLBACK_2", "type": "CONDITION_END"} */
444
445 /* LDV {"action": "CALL", "type": "SUBPROCESS_BEGIN", "comment": "Driver is probed. Call power management callbacks or release the device."} */
446 /* LDV {"action": "CALL", "type": "SUBPROCESS_END"} */
447
448 /* Jump to a subprocess 'call' initial state */
449 goto ldv_call_11;
450 break;
451 }
452 case 2: {
453 /* LDV {"action": "PM_REGISTER", "type": "DISPATCH_BEGIN", "comment": "Proceed to a power management scenario."} */
454 ldv_dispatch_pm_register_11_13();
455 /* LDV {"action": "PM_REGISTER", "type": "DISPATCH_END"} */
456
457 /* LDV {"action": "PM_DEREGISTER", "type": "DISPATCH_BEGIN", "comment": "Finish the power management scenario."} */
458 ldv_dispatch_pm_deregister_11_12();
459 /* LDV {"action": "PM_DEREGISTER", "type": "DISPATCH_END"} */
460
461 /* LDV {"action": "CALL", "type": "SUBPROCESS_BEGIN", "comment": "Driver is probed. Call power management callbacks or release the device."} */
462 /* LDV {"action": "CALL", "type": "SUBPROCESS_END"} */
463
464 /* Jump to a subprocess 'call' initial state */
465 goto ldv_call_11;
466 break;
467 }
468 case 3: {
469 /* LDV {"action": "RELEASE_4", "type": "CALL_BEGIN", "callback": true, "comment": "Remove device from the system. Invoke callback remove from platform_driver."} */
470 /* LDV {"type": "CALLBACK", "call": "ldv_emg_wrapper_dnet_remove_3(ldv_11_resource);", "comment": "release"} */
471 ldv_emg_wrapper_dnet_remove_3(ldv_11_resource);
472 /* LDV {"action": "RELEASE_4", "type": "CALL_END"} */
473
474 /* LDV {"action": "AFTER_RELEASE", "type": "CONDITION_BEGIN", "comment": "Platform device is released now."} */
475 ldv_11_probed = 1;
476 /* LDV {"action": "AFTER_RELEASE", "type": "CONDITION_END"} */
477
478 /* LDV {"action": "MAIN", "type": "SUBPROCESS_BEGIN", "comment": "Check that device is truely in the system and begin callback invocations."} */
479 /* LDV {"action": "MAIN", "type": "SUBPROCESS_END"} */
480
481 /* Jump to a subprocess 'main' initial state */
482 goto ldv_main_11;
483 break;
484 }
485 default: ldv_assume(0);
486 }
487 /* End of the subprocess 'call' */
488 return 0;
489 /* LDV {"comment": "End of control function based on process 'platform_instance(platform)'", "type": "CONTROL_FUNCTION_END", "function": "ldv_platform_instance_11"} */
490 }
491
492 /* AUX_FUNC ldv_emg_platform_driver_unregister */
493 void ldv_emg_platform_driver_unregister(struct platform_driver *arg0) {
494 /* LDV {"comment": "Unregister a driver for platform-level device. (Relevant to 'dnet_driver')", "type": "CONTROL_FUNCTION_BEGIN", "function": "ldv_emg_platform_driver_unregister"} */
495 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
496 struct platform_driver *ldv_4_platform_driver = ldv_emg_alias_dnet_driver_2;
497 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
498 /* LDV {"action": "ASSIGN", "type": "CONDITION_BEGIN", "comment": "Get 'platform_driver' argument."} */
499 ldv_4_platform_driver = arg0;
500 /* LDV {"action": "ASSIGN", "type": "CONDITION_END"} */
501
502 /* LDV {"action": "DEREGISTER", "type": "DISPATCH_BEGIN", "comment": "Deregister 'platform_driver' callbacks."} */
503 ldv_dispatch_deregister_4_1(ldv_4_platform_driver);
504 /* LDV {"action": "DEREGISTER", "type": "DISPATCH_END"} */
505
506 /* Exit function at a terminal state */
507 return;
508 /* End of the process */
509 return;
510 /* LDV {"comment": "End of control function based on process 'platform_driver_unregister'", "type": "CONTROL_FUNCTION_END", "function": "ldv_emg_platform_driver_unregister"} */
511 }
512
513 /* AUX_FUNC ldv_dispatch_irq_deregister_3_1 */
514 void ldv_dispatch_irq_deregister_3_1(int arg0) {
515 int ret;
516 struct ldv_struct_free_irq_3 *cf_arg_12;
517 switch (ldv_undef_int()) {
518 case 0: {
519 ret = pthread_join(ldv_thread_12, 0);
520 ldv_assume(ret == 0);
521 break;
522 };
523 default: ldv_assume(0);
524 };
525 return;
526 }
527
528 /* AUX_FUNC ldv_emg_alloc_etherdev_mqs */
529 struct net_device *ldv_emg_alloc_etherdev_mqs(int arg0, unsigned int arg1, unsigned int arg2) {
530 /* LDV {"comment": "Allocate and set up an ethernet device.", "type": "CONTROL_FUNCTION_BEGIN", "function": "ldv_emg_alloc_etherdev_mqs"} */
531 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
532 struct net_device *ldv_5_netdev;
533 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
534 /* LDV {"action": null, "type": "ARTIFICIAL", "comment": "Artificial state in scenario"} */
535
536 if (ldv_undef_int()) {
537 /* LDV {"action": "ALLOC", "type": "CONDITION_BEGIN", "comment": "Allocate memory for an ethernet device."} */
538 ldv_5_netdev = ldv_xmalloc_unknown_size(0);
539 /* LDV {"action": "ALLOC", "type": "CONDITION_END"} */
540
541 /* LDV {"action": "SUCCESS", "type": "CONDITION_BEGIN", "comment": "Memory has been allocated properly."} */
542 return ldv_5_netdev;
543 /* LDV {"action": "SUCCESS", "type": "CONDITION_END"} */
544
545 /* Exit function at a terminal state */
546 }
547 else {
548 /* LDV {"action": "FAIL", "type": "CONDITION_BEGIN", "comment": "Memory has not been allocated."} */
549 return 0;
550 /* LDV {"action": "FAIL", "type": "CONDITION_END"} */
551
552 /* Exit function at a terminal state */
553 }
554 /* End of the process */
555 /* LDV {"comment": "End of control function based on process 'alloc_etherdev_mqs'", "type": "CONTROL_FUNCTION_END", "function": "ldv_emg_alloc_etherdev_mqs"} */
556 }
557
558 /* AUX_FUNC ldv_dispatch_pm_register_11_13 */
559 void ldv_dispatch_pm_register_11_13(void) {
560 int ret;
561 struct ldv_struct_platform_instance_11 *cf_arg_10;
562 switch (ldv_undef_int()) {
563 case 0: {
564 cf_arg_10 = ldv_xmalloc(sizeof(struct ldv_struct_platform_instance_11));
565 ret = pthread_create(& ldv_thread_10, 0, ldv_pm_ops_scenario_10, cf_arg_10);
566 ldv_assume(ret == 0);
567 break;
568 };
569 default: ldv_assume(0);
570 };
571 return;
572 }
573
574 /* AUX_FUNC ldv_dispatch_register_8_4 */
575 void ldv_dispatch_register_8_4(struct net_device *arg0) {
576 int ret;
577 struct ldv_struct_random_scenario_13 *cf_arg_13;
578 switch (ldv_undef_int()) {
579 case 0: {
580 cf_arg_13 = ldv_xmalloc(sizeof(struct ldv_struct_random_scenario_13));
581 cf_arg_13->arg0 = arg0;
582 ret = pthread_create(& ldv_thread_13, 0, ldv_random_scenario_13, cf_arg_13);
583 ldv_assume(ret == 0);
584 break;
585 };
586 default: ldv_assume(0);
587 };
588 return;
589 }
590
591 /* AUX_FUNC ldv_dispatch_register_7_3 */
592 void ldv_dispatch_register_7_3(struct platform_driver *arg0) {
593 int ret;
594 struct ldv_struct_platform_instance_11 *cf_arg_11;
595 switch (ldv_undef_int()) {
596 case 0: {
597 cf_arg_11 = ldv_xmalloc(sizeof(struct ldv_struct_platform_instance_11));
598 cf_arg_11->arg0 = arg0;
599 ret = pthread_create(& ldv_thread_11, 0, ldv_platform_instance_11, cf_arg_11);
600 ldv_assume(ret == 0);
601 break;
602 };
603 default: ldv_assume(0);
604 };
605 return;
606 }
607
608 /* AUX_FUNC ldv_emg_request_irq */
609 int ldv_emg_request_irq(unsigned int arg0, enum irqreturn (*arg1)(int, void *), long unsigned int arg2, char *arg3, void *arg4) {
610 /* LDV {"comment": "Allocate an interrupt line for a managed device. (Relevant to 'dnet_interrupt')", "type": "CONTROL_FUNCTION_BEGIN", "function": "ldv_emg_request_irq"} */
611 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
612 int ldv_9_line;
613 void *ldv_9_data;
614 enum irqreturn (*ldv_9_callback)(int, void *) = &ldv_emg_wrapper_dnet_interrupt_2;
615 enum irqreturn (*ldv_9_thread)(int, void *);
616 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
617 /* LDV {"action": null, "type": "ARTIFICIAL", "comment": "Artificial state in scenario"} */
618
619 if (ldv_undef_int()) {
620 /* LDV {"action": "ASSIGN", "type": "CONDITION_BEGIN", "comment": "Get line, callbacks and data arguments."} */
621 ldv_9_line = arg0;
622 ldv_9_callback = arg1;
623 ldv_9_thread = 0;
624 ldv_9_data = arg4;
625 /* LDV {"action": "ASSIGN", "type": "CONDITION_END"} */
626
627 /* LDV {"action": "IRQ_REGISTER", "type": "DISPATCH_BEGIN", "comment": "Register interrupt callback (callbacks)."} */
628 ldv_dispatch_irq_register_9_3(ldv_9_line, ldv_9_callback, ldv_9_thread, ldv_9_data);
629 /* LDV {"action": "IRQ_REGISTER", "type": "DISPATCH_END"} */
630
631 /* LDV {"action": "SUCCESS", "type": "CONDITION_BEGIN", "comment": "Successfully allocated an interrupt line for a managed device."} */
632 return 0;
633 /* LDV {"action": "SUCCESS", "type": "CONDITION_END"} */
634
635 /* Exit function at a terminal state */
636 }
637 else {
638 /* LDV {"action": "FAIL", "type": "CONDITION_BEGIN", "comment": "Failed to allocate an interrupt line for a managed device."} */
639 return ldv_undef_int_negative();
640 /* LDV {"action": "FAIL", "type": "CONDITION_END"} */
641
642 /* Exit function at a terminal state */
643 }
644 /* End of the process */
645 /* LDV {"comment": "End of control function based on process 'request_irq'", "type": "CONTROL_FUNCTION_END", "function": "ldv_emg_request_irq"} */
646 }
647
648 /* AUX_FUNC ldv_random_scenario_13 */
649 void *ldv_random_scenario_13(void *arg0) {
650 /* LDV {"thread": 14, "type": "CONTROL_FUNCTION_BEGIN", "comment": "Call callbacks randomly. (Relevant to '& dnet_get_drvinfo' '& ethtool_op_get_link' '& ethtool_op_get_ts_info')", "function": "ldv_random_scenario_13"} */
651 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
652 struct net_device *ldv_13_resource;
653 struct sk_buff *ldv_13_ldv_param_0_9;
654 struct ethtool_drvinfo *ldv_13_ldv_param_1_2;
655 struct ethtool_ts_info *ldv_13_ldv_param_1_3;
656 struct ethtool_link_ksettings *ldv_13_ldv_param_1_4;
657 int ldv_13_ldv_param_2_6;
658 struct ethtool_link_ksettings *ldv_13_ldv_param_1_7;
659 void *ldv_13_ldv_param_1_8;
660 struct net_device *ldv_13_container;
661 struct ifreq *ldv_13_ldv_param_1_5;
662 /* Received labels */
663 struct ldv_struct_random_scenario_13 *data = (struct ldv_struct_random_scenario_13*) arg0;
664
665 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
666 /* LDV {"action": "REGISTER", "type": "RECEIVE_BEGIN", "comment": "Begin NET callbacks invocations scenario."} */
667 /* Assign recieved labels */
668 if (data) {
669 ldv_13_container = data->arg0;
670 ldv_free(data);
671 }
672 /* LDV {"action": "REGISTER", "type": "RECEIVE_END"} */
673
674 /* LDV {"action": "INIT", "type": "CONDITION_BEGIN", "comment": "Allocate memory of common callback parameters."} */
675 ldv_13_resource = ldv_xmalloc_unknown_size(0);
676 /* LDV {"action": "INIT", "type": "CONDITION_END"} */
677
678 /* LDV {"action": "CALL", "type": "SUBPROCESS_BEGIN", "comment": "Prepare to call a random callback or deregister the callbacks."} */
679 /* LDV {"action": "CALL", "type": "SUBPROCESS_END"} */
680
681 /* Jump to a subprocess 'call' initial state */
682 goto ldv_call_13;
683 /* End of the process */
684 return 0;
685
686 /* Sbprocess call */
687 ldv_call_13:
688 /* LDV {"action": null, "type": "ARTIFICIAL", "comment": "Artificial state in scenario"} */
689
690 if (ldv_undef_int()) {
691 /* LDV {"action": "PRE_CALL_2", "type": "CONDITION_BEGIN", "comment": "Allocate memory for adhoc callback parameters."} */
692 ldv_13_ldv_param_1_2 = ldv_xmalloc_unknown_size(0);
693 /* LDV {"action": "PRE_CALL_2", "type": "CONDITION_END"} */
694
695 switch (ldv_undef_int()) {
696 case 1: {
697 /* LDV {"action": "CALLBACK_4", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback get_drvinfo from ethtool_ops."} */
698 /* LDV {"type": "CALLBACK", "call": "ldv_emg_wrapper_dnet_get_drvinfo_2(ldv_13_resource, ldv_13_ldv_param_1_2);", "comment": "callback"} */
699 ldv_emg_wrapper_dnet_get_drvinfo_2(ldv_13_resource, ldv_13_ldv_param_1_2);
700 /* LDV {"action": "CALLBACK_4", "type": "CALL_END"} */
701
702 break;
703 }
704 case 2: {
705 /* LDV {"action": "PRE_CALL_23", "type": "CONDITION_BEGIN", "comment": "Allocate memory for adhoc callback parameters."} */
706 ldv_13_ldv_param_0_9 = ldv_xmalloc_unknown_size(0);
707 /* LDV {"action": "PRE_CALL_23", "type": "CONDITION_END"} */
708
709 /* LDV {"action": "CALLBACK_25", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback ndo_start_xmit from net_device_ops."} */
710 /* LDV {"type": "CALLBACK", "call": "ldv_emg_wrapper_dnet_start_xmit_11(ldv_13_ldv_param_0_9, ldv_13_resource);", "comment": "callback"} */
711 ldv_emg_wrapper_dnet_start_xmit_11(ldv_13_ldv_param_0_9, ldv_13_resource);
712 /* LDV {"action": "CALLBACK_25", "type": "CALL_END"} */
713
714 /* LDV {"action": "POST_CALL_24", "type": "CONDITION_BEGIN", "comment": "Free memory of adhoc callback parameters."} */
715 ldv_free(ldv_13_ldv_param_0_9);
716 /* LDV {"action": "POST_CALL_24", "type": "CONDITION_END"} */
717
718 break;
719 }
720 case 3: {
721 /* LDV {"action": "PRE_CALL_20", "type": "CONDITION_BEGIN", "comment": "Allocate memory for adhoc callback parameters."} */
722 ldv_13_ldv_param_1_8 = ldv_xmalloc_unknown_size(0);
723 /* LDV {"action": "PRE_CALL_20", "type": "CONDITION_END"} */
724
725 /* LDV {"action": "CALLBACK_22", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback ndo_set_mac_address from net_device_ops."} */
726 /* LDV {"type": "CALLBACK", "call": "ldv_emg_alias_eth_mac_addr_10(ldv_13_resource, ldv_13_ldv_param_1_8);", "comment": "callback"} */
727 ldv_emg_alias_eth_mac_addr_10(ldv_13_resource, ldv_13_ldv_param_1_8);
728 /* LDV {"action": "CALLBACK_22", "type": "CALL_END"} */
729
730 /* LDV {"action": "POST_CALL_21", "type": "CONDITION_BEGIN", "comment": "Free memory of adhoc callback parameters."} */
731 ldv_free(ldv_13_ldv_param_1_8);
732 /* LDV {"action": "POST_CALL_21", "type": "CONDITION_END"} */
733
734 break;
735 }
736 case 4: {
737 /* LDV {"action": "CALLBACK_19", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback ndo_get_stats from net_device_ops."} */
738 /* LDV {"type": "CALLBACK", "call": "ldv_emg_wrapper_dnet_get_stats_9(ldv_13_resource);", "comment": "callback"} */
739 ldv_emg_wrapper_dnet_get_stats_9(ldv_13_resource);
740 /* LDV {"action": "CALLBACK_19", "type": "CALL_END"} */
741
742 break;
743 }
744 case 5: {
745 /* LDV {"action": "CALLBACK_18", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback ndo_validate_addr from net_device_ops."} */
746 /* LDV {"type": "CALLBACK", "call": "ldv_emg_alias_eth_validate_addr_8(ldv_13_resource);", "comment": "callback"} */
747 ldv_emg_alias_eth_validate_addr_8(ldv_13_resource);
748 /* LDV {"action": "CALLBACK_18", "type": "CALL_END"} */
749
750 break;
751 }
752 case 6: {
753 /* LDV {"action": "PRE_CALL_15", "type": "CONDITION_BEGIN", "comment": "Allocate memory for adhoc callback parameters."} */
754 ldv_13_ldv_param_1_7 = ldv_xmalloc_unknown_size(0);
755 /* LDV {"action": "PRE_CALL_15", "type": "CONDITION_END"} */
756
757 /* LDV {"action": "CALLBACK_17", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback set_link_ksettings from ethtool_ops."} */
758 /* LDV {"type": "CALLBACK", "call": "ldv_emg_alias_phy_ethtool_set_link_ksettings_7(ldv_13_resource, ldv_13_ldv_param_1_7);", "comment": "callback"} */
759 ldv_emg_alias_phy_ethtool_set_link_ksettings_7(ldv_13_resource, ldv_13_ldv_param_1_7);
760 /* LDV {"action": "CALLBACK_17", "type": "CALL_END"} */
761
762 /* LDV {"action": "POST_CALL_16", "type": "CONDITION_BEGIN", "comment": "Free memory of adhoc callback parameters."} */
763 ldv_free(ldv_13_ldv_param_1_7);
764 /* LDV {"action": "POST_CALL_16", "type": "CONDITION_END"} */
765
766 break;
767 }
768 case 7: {
769 /* LDV {"action": "PRE_CALL_12", "type": "CONDITION_BEGIN", "comment": "Allocate memory for adhoc callback parameters."} */
770 ldv_13_ldv_param_1_5 = ldv_xmalloc_unknown_size(0);
771 /* LDV {"action": "PRE_CALL_12", "type": "CONDITION_END"} */
772
773 /* LDV {"action": "CALLBACK_14", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback ndo_do_ioctl from net_device_ops."} */
774 /* LDV {"type": "CALLBACK", "call": "ldv_emg_wrapper_dnet_ioctl_6(ldv_13_resource, ldv_13_ldv_param_1_5, ldv_13_ldv_param_2_6);", "comment": "callback"} */
775 ldv_emg_wrapper_dnet_ioctl_6(ldv_13_resource, ldv_13_ldv_param_1_5, ldv_13_ldv_param_2_6);
776 /* LDV {"action": "CALLBACK_14", "type": "CALL_END"} */
777
778 /* LDV {"action": "POST_CALL_13", "type": "CONDITION_BEGIN", "comment": "Free memory of adhoc callback parameters."} */
779 ldv_free(ldv_13_ldv_param_1_5);
780 /* LDV {"action": "POST_CALL_13", "type": "CONDITION_END"} */
781
782 break;
783 }
784 case 8: {
785 /* LDV {"action": "PRE_CALL_9", "type": "CONDITION_BEGIN", "comment": "Allocate memory for adhoc callback parameters."} */
786 ldv_13_ldv_param_1_4 = ldv_xmalloc_unknown_size(0);
787 /* LDV {"action": "PRE_CALL_9", "type": "CONDITION_END"} */
788
789 /* LDV {"action": "CALLBACK_11", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback get_link_ksettings from ethtool_ops."} */
790 /* LDV {"type": "CALLBACK", "call": "ldv_emg_alias_phy_ethtool_get_link_ksettings_5(ldv_13_resource, ldv_13_ldv_param_1_4);", "comment": "callback"} */
791 ldv_emg_alias_phy_ethtool_get_link_ksettings_5(ldv_13_resource, ldv_13_ldv_param_1_4);
792 /* LDV {"action": "CALLBACK_11", "type": "CALL_END"} */
793
794 /* LDV {"action": "POST_CALL_10", "type": "CONDITION_BEGIN", "comment": "Free memory of adhoc callback parameters."} */
795 ldv_free(ldv_13_ldv_param_1_4);
796 /* LDV {"action": "POST_CALL_10", "type": "CONDITION_END"} */
797
798 break;
799 }
800 case 9: {
801 /* LDV {"action": "PRE_CALL_6", "type": "CONDITION_BEGIN", "comment": "Allocate memory for adhoc callback parameters."} */
802 ldv_13_ldv_param_1_3 = ldv_xmalloc_unknown_size(0);
803 /* LDV {"action": "PRE_CALL_6", "type": "CONDITION_END"} */
804
805 /* LDV {"action": "CALLBACK_8", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback get_ts_info from ethtool_ops."} */
806 /* LDV {"type": "CALLBACK", "call": "ldv_emg_alias_ethtool_op_get_ts_info_4(ldv_13_resource, ldv_13_ldv_param_1_3);", "comment": "callback"} */
807 ldv_emg_alias_ethtool_op_get_ts_info_4(ldv_13_resource, ldv_13_ldv_param_1_3);
808 /* LDV {"action": "CALLBACK_8", "type": "CALL_END"} */
809
810 /* LDV {"action": "POST_CALL_7", "type": "CONDITION_BEGIN", "comment": "Free memory of adhoc callback parameters."} */
811 ldv_free(ldv_13_ldv_param_1_3);
812 /* LDV {"action": "POST_CALL_7", "type": "CONDITION_END"} */
813
814 break;
815 }
816 case 10: {
817 /* LDV {"action": "CALLBACK_5", "type": "CALL_BEGIN", "callback": true, "comment": "Call any random callback. Invoke callback get_link from ethtool_ops."} */
818 /* LDV {"type": "CALLBACK", "call": "ldv_emg_alias_ethtool_op_get_link_3(ldv_13_resource);", "comment": "callback"} */
819 ldv_emg_alias_ethtool_op_get_link_3(ldv_13_resource);
820 /* LDV {"action": "CALLBACK_5", "type": "CALL_END"} */
821
822 break;
823 }
824 default: ldv_assume(0);
825 }
826 /* LDV {"action": "POST_CALL_3", "type": "CONDITION_BEGIN", "comment": "Free memory of adhoc callback parameters."} */
827 ldv_free(ldv_13_ldv_param_1_2);
828 /* LDV {"action": "POST_CALL_3", "type": "CONDITION_END"} */
829
830 /* LDV {"action": "CALL", "type": "SUBPROCESS_BEGIN", "comment": "Prepare to call a random callback or deregister the callbacks."} */
831 /* LDV {"action": "CALL", "type": "SUBPROCESS_END"} */
832
833 /* Jump to a subprocess 'call' initial state */
834 goto ldv_call_13;
835 }
836 else {
837 /* LDV {"action": "FREE", "type": "CONDITION_BEGIN", "comment": "Free memory of common callback parameters."} */
838 ldv_free(ldv_13_resource);
839 /* LDV {"action": "FREE", "type": "CONDITION_END"} */
840
841 /* LDV {"action": "DEREGISTER", "type": "RECEIVE_BEGIN", "comment": "Finish NET callbacks invocations scenario."} */
842 /* Skip a non-replicative signal receiving */
843 /* LDV {"action": "DEREGISTER", "type": "RECEIVE_END"} */
844
845 /* Exit function at a terminal state */
846 return 0;
847 }
848 /* End of the subprocess 'call' */
849 return 0;
850 /* LDV {"comment": "End of control function based on process 'random_scenario(net)'", "type": "CONTROL_FUNCTION_END", "function": "ldv_random_scenario_13"} */
851 }
852
853 /* AUX_FUNC ldv_initialization_1 */
854 void *ldv_initialization_1(void *arg0) {
855 /* LDV {"thread": 2, "type": "CONTROL_FUNCTION_BEGIN", "comment": "Initialize or exit module.", "function": "ldv_initialization_1"} */
856 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
857 int ldv_1_ret;
858 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
859 /* LDV {"action": "DNET_DRIVER_INIT", "type": "CALL_BEGIN", "callback": true, "comment": "Initialize the module after insmod with 'dnet_driver_init' function."} */
860 /* LDV {"type": "CALLBACK", "call": "dnet_driver_init();", "comment": "dnet_driver_init"} */
861 ldv_1_ret = ldv_emg_dnet_driver_init();
862 ldv_1_ret = ldv_post_init(ldv_1_ret);
863 /* LDV {"action": "DNET_DRIVER_INIT", "type": "CALL_END"} */
864
865 if (ldv_undef_int()) {
866 /* LDV {"action": "INIT_FAILED", "type": "CONDITION_BEGIN", "comment": "Failed to initialize the module."} */
867 ldv_assume(ldv_1_ret != 0);
868 /* LDV {"action": "INIT_FAILED", "type": "CONDITION_END"} */
869
870 /* Exit function at a terminal state */
871 return 0;
872 }
873 else {
874 /* LDV {"action": "INIT_SUCCESS", "type": "CONDITION_BEGIN", "comment": "Module has been initialized."} */
875 ldv_assume(ldv_1_ret == 0);
876 /* LDV {"action": "INIT_SUCCESS", "type": "CONDITION_END"} */
877
878 /* LDV {"action": "DNET_DRIVER_EXIT", "type": "CALL_BEGIN", "callback": true, "comment": "Exit the module before its unloading with 'dnet_driver_exit' function."} */
879 /* LDV {"type": "CALLBACK", "call": "dnet_driver_exit();", "comment": "dnet_driver_exit"} */
880 ldv_emg_dnet_driver_exit();
881 /* LDV {"action": "DNET_DRIVER_EXIT", "type": "CALL_END"} */
882
883 /* Exit function at a terminal state */
884 return 0;
885 }
886 /* End of the process */
887 return 0;
888 /* LDV {"comment": "End of control function based on process 'initialization(linux)'", "type": "CONTROL_FUNCTION_END", "function": "ldv_initialization_1"} */
889 }
890
891 /* AUX_FUNC ldv_dispatch_irq_register_9_3 */
892 void ldv_dispatch_irq_register_9_3(int arg0, enum irqreturn (*arg1)(int, void *), enum irqreturn (*arg2)(int, void *), void *arg3) {
893 int ret;
894 struct ldv_struct_interrupt_scenario_12 *cf_arg_12;
895 switch (ldv_undef_int()) {
896 case 0: {
897 cf_arg_12 = ldv_xmalloc(sizeof(struct ldv_struct_interrupt_scenario_12));
898 cf_arg_12->arg0 = arg0;
899 cf_arg_12->arg1 = arg1;
900 cf_arg_12->arg2 = arg2;
901 cf_arg_12->arg3 = arg3;
902 ret = pthread_create(& ldv_thread_12, 0, ldv_interrupt_scenario_12, cf_arg_12);
903 ldv_assume(ret == 0);
904 break;
905 };
906 default: ldv_assume(0);
907 };
908 return;
909 }
910
911 /* AUX_FUNC ldv_dispatch_deregister_4_1 */
912 void ldv_dispatch_deregister_4_1(struct platform_driver *arg0) {
913 int ret;
914 struct ldv_struct_platform_instance_11 *cf_arg_11;
915 switch (ldv_undef_int()) {
916 case 0: {
917 ret = pthread_join(ldv_thread_11, 0);
918 ldv_assume(ret == 0);
919 break;
920 };
921 default: ldv_assume(0);
922 };
923 return;
924 }
925
926 /* AUX_FUNC ldv_dispatch_pm_deregister_11_12 */
927 void ldv_dispatch_pm_deregister_11_12(void) {
928 int ret;
929 struct ldv_struct_platform_instance_11 *cf_arg_10;
930 switch (ldv_undef_int()) {
931 case 0: {
932 ret = pthread_join(ldv_thread_10, 0);
933 ldv_assume(ret == 0);
934 break;
935 };
936 default: ldv_assume(0);
937 };
938 return;
939 }
940
941 /* AUX_FUNC ldv_emg_unregister_netdev */
942 void ldv_emg_unregister_netdev(struct net_device *arg0) {
943 /* LDV {"comment": "Deregister network device and its callbacks. (Relevant to '& dnet_close')", "type": "CONTROL_FUNCTION_BEGIN", "function": "ldv_emg_unregister_netdev"} */
944 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
945 struct net_device *ldv_6_netdev;
946 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
947 /* LDV {"action": "ASSIGN", "type": "CONDITION_BEGIN", "comment": "Get network device structure."} */
948 ldv_6_netdev = arg0;
949 /* LDV {"action": "ASSIGN", "type": "CONDITION_END"} */
950
951 /* 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."} */
952 /* LDV {"type": "CALLBACK", "call": "ldv_emg_wrapper_dnet_close_2(ldv_6_netdev);", "comment": "stop"} */
953 ldv_emg_wrapper_dnet_close_2(ldv_6_netdev);
954 /* LDV {"action": "STOP_2", "type": "CALL_END"} */
955
956 /* LDV {"action": "DEREGISTER", "type": "DISPATCH_BEGIN", "comment": "Deregiste of the network device has finished."} */
957 ldv_dispatch_deregister_6_1(ldv_6_netdev);
958 /* LDV {"action": "DEREGISTER", "type": "DISPATCH_END"} */
959
960 /* Exit function at a terminal state */
961 return;
962 /* End of the process */
963 return;
964 /* LDV {"comment": "End of control function based on process 'unregister_netdev'", "type": "CONTROL_FUNCTION_END", "function": "ldv_emg_unregister_netdev"} */
965 }
966
967 /* AUX_FUNC ldv_emg_free_irq */
968 void *ldv_emg_free_irq(unsigned int arg0, void *arg1) {
969 /* LDV {"comment": "Free an interrupt.", "type": "CONTROL_FUNCTION_BEGIN", "function": "ldv_emg_free_irq"} */
970 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
971 int ldv_3_line;
972 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
973 /* LDV {"action": "ASSIGN", "type": "CONDITION_BEGIN", "comment": "Get an interrupt line argument."} */
974 ldv_3_line = arg0;
975 /* LDV {"action": "ASSIGN", "type": "CONDITION_END"} */
976
977 /* LDV {"action": "IRQ_DEREGISTER", "type": "DISPATCH_BEGIN", "comment": "The interrupt line is freed."} */
978 ldv_dispatch_irq_deregister_3_1(ldv_3_line);
979 /* LDV {"action": "IRQ_DEREGISTER", "type": "DISPATCH_END"} */
980
981 /* Exit function at a terminal state */
982 /* End of the process */
983 /* LDV {"comment": "End of control function based on process 'free_irq'", "type": "CONTROL_FUNCTION_END", "function": "ldv_emg_free_irq"} */
984 }
985
986 /* AUX_FUNC ldv_dispatch_deregister_6_1 */
987 void ldv_dispatch_deregister_6_1(struct net_device *arg0) {
988 int ret;
989 struct ldv_struct_random_scenario_13 *cf_arg_13;
990 switch (ldv_undef_int()) {
991 case 0: {
992 ret = pthread_join(ldv_thread_13, 0);
993 ldv_assume(ret == 0);
994 break;
995 };
996 default: ldv_assume(0);
997 };
998 return;
999 }
1000
1001 /* AUX_FUNC ldv_emg_free_netdev */
1002 void ldv_emg_free_netdev(struct net_device *arg0) {
1003 /* LDV {"comment": "Free memory of a network device.", "type": "CONTROL_FUNCTION_BEGIN", "function": "ldv_emg_free_netdev"} */
1004 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
1005 struct net_device *ldv_2_netdev;
1006 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
1007 /* LDV {"action": "FREE", "type": "CONDITION_BEGIN", "comment": "Freeing memory of a network device."} */
1008 ldv_2_netdev = arg0;
1009 ldv_free(ldv_2_netdev);
1010 /* LDV {"action": "FREE", "type": "CONDITION_END"} */
1011
1012 /* Exit function at a terminal state */
1013 return;
1014 /* End of the process */
1015 return;
1016 /* LDV {"comment": "End of control function based on process 'free_netdev'", "type": "CONTROL_FUNCTION_END", "function": "ldv_emg_free_netdev"} */
1017 }
1018
1019 /* AUX_FUNC ldv_interrupt_scenario_12 */
1020 void *ldv_interrupt_scenario_12(void *arg0) {
1021 /* LDV {"thread": 13, "type": "CONTROL_FUNCTION_BEGIN", "comment": "Handle an interrupt. (Relevant to 'dnet_interrupt')", "function": "ldv_interrupt_scenario_12"} */
1022 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
1023 enum irqreturn ldv_12_ret_val;
1024 int ldv_12_line;
1025 void *ldv_12_data;
1026 enum irqreturn (*ldv_12_callback)(int, void *) = &ldv_emg_wrapper_dnet_interrupt_2;
1027 enum irqreturn (*ldv_12_thread)(int, void *);
1028 /* Received labels */
1029 struct ldv_struct_interrupt_scenario_12 *data = (struct ldv_struct_interrupt_scenario_12*) arg0;
1030
1031 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
1032 /* LDV {"action": "IRQ_REGISTER", "type": "RECEIVE_BEGIN", "comment": "An interrupt is registered."} */
1033 /* Assign recieved labels */
1034 if (data) {
1035 ldv_12_line = data->arg0;
1036 ldv_12_callback = data->arg1;
1037 ldv_12_thread = data->arg2;
1038 ldv_12_data = data->arg3;
1039 ldv_free(data);
1040 }
1041 /* LDV {"action": "IRQ_REGISTER", "type": "RECEIVE_END"} */
1042
1043 /* 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."} */
1044 /* Callback pre-call */
1045 ldv_switch_to_interrupt_context();
1046 /* LDV {"type": "CALLBACK", "call": "ldv_12_ret_val = ldv_emg_wrapper_dnet_interrupt_2(ldv_12_line, ldv_12_data);", "comment": "handler"} */
1047 ldv_12_ret_val = ldv_emg_wrapper_dnet_interrupt_2(ldv_12_line, ldv_12_data);
1048 /* Callback post-call */
1049 ldv_switch_to_process_context();
1050 /* LDV {"action": "HANDLER_2", "type": "CALL_END"} */
1051
1052 if (ldv_undef_int()) {
1053 /* LDV {"action": "NEED_THREAD", "type": "CONDITION_BEGIN", "comment": "Wake a thread to continue an interrupt handling."} */
1054 ldv_assume(ldv_12_ret_val == IRQ_WAKE_THREAD);
1055 /* LDV {"action": "NEED_THREAD", "type": "CONDITION_END"} */
1056
1057 /* 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."} */
1058 if (ldv_12_thread) {
1059 /* LDV {"type": "CALLBACK", "call": "ldv_12_thread(ldv_12_line, ldv_12_data);", "comment": "thread"} */
1060 ldv_12_thread(ldv_12_line, ldv_12_data);
1061 }
1062 /* LDV {"action": "THREAD_3", "type": "CALL_END"} */
1063
1064 }
1065 else {
1066 /* LDV {"action": "HANDLED", "type": "CONDITION_BEGIN", "comment": "An interrupt has been handled."} */
1067 ldv_assume(ldv_12_ret_val != IRQ_WAKE_THREAD);
1068 /* LDV {"action": "HANDLED", "type": "CONDITION_END"} */
1069
1070 }
1071 /* LDV {"action": "IRQ_DEREGISTER", "type": "RECEIVE_BEGIN", "comment": "An interrupt is deregistered."} */
1072 /* Skip a non-replicative signal receiving */
1073 /* LDV {"action": "IRQ_DEREGISTER", "type": "RECEIVE_END"} */
1074
1075 /* Exit function at a terminal state */
1076 return 0;
1077 /* End of the process */
1078 return 0;
1079 /* LDV {"comment": "End of control function based on process 'interrupt_scenario(interrupt)'", "type": "CONTROL_FUNCTION_END", "function": "ldv_interrupt_scenario_12"} */
1080 }
1081
1082 /* AUX_FUNC ldv_emg___platform_driver_register */
1083 int ldv_emg___platform_driver_register(struct platform_driver *arg0, struct module *arg1) {
1084 /* LDV {"comment": "Register a driver for platform-level device. (Relevant to 'dnet_driver')", "type": "CONTROL_FUNCTION_BEGIN", "function": "ldv_emg___platform_driver_register"} */
1085 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
1086 struct platform_driver *ldv_7_platform_driver = ldv_emg_alias_dnet_driver_2;
1087 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
1088 /* LDV {"action": null, "type": "ARTIFICIAL", "comment": "Artificial state in scenario"} */
1089
1090 if (ldv_undef_int()) {
1091 /* LDV {"action": "ASSIGN", "type": "CONDITION_BEGIN", "comment": "Get platform_driver structure argument."} */
1092 ldv_7_platform_driver = arg0;
1093 /* LDV {"action": "ASSIGN", "type": "CONDITION_END"} */
1094
1095 /* LDV {"action": "REGISTER", "type": "DISPATCH_BEGIN", "comment": "Register platform_driver callbacks."} */
1096 ldv_dispatch_register_7_3(ldv_7_platform_driver);
1097 /* LDV {"action": "REGISTER", "type": "DISPATCH_END"} */
1098
1099 /* LDV {"action": "SUCCESS", "type": "CONDITION_BEGIN", "comment": "Successfully registered a driver for platform-level device."} */
1100 return 0;
1101 /* LDV {"action": "SUCCESS", "type": "CONDITION_END"} */
1102
1103 /* Exit function at a terminal state */
1104 }
1105 else {
1106 /* LDV {"action": "FAIL", "type": "CONDITION_BEGIN", "comment": "Fail to register a driver for platform-level device."} */
1107 return ldv_undef_int_negative();
1108 /* LDV {"action": "FAIL", "type": "CONDITION_END"} */
1109
1110 /* Exit function at a terminal state */
1111 }
1112 /* End of the process */
1113 /* LDV {"comment": "End of control function based on process '__platform_driver_register'", "type": "CONTROL_FUNCTION_END", "function": "ldv_emg___platform_driver_register"} */
1114 }
1115
1116 /* AUX_FUNC ldv_emg_register_netdev */
1117 int ldv_emg_register_netdev(struct net_device *arg0) {
1118 /* LDV {"comment": "Register network device and its callbacks. (Relevant to '& dnet_open')", "type": "CONTROL_FUNCTION_BEGIN", "function": "ldv_emg_register_netdev"} */
1119 /* LDV {"type": "CONTROL_FUNCTION_INIT_BEGIN", "comment": "Declare auxiliary variables."} */
1120 struct net_device *ldv_8_netdev;
1121 int ldv_8_ret = ldv_undef_int();
1122 /* LDV {"type": "CONTROL_FUNCTION_INIT_END", "comment": "Declare auxiliary variables."} */
1123 /* Initialize automaton variables */
1124 ldv_8_ret = ldv_undef_int();
1125 /* LDV {"action": null, "type": "ARTIFICIAL", "comment": "Artificial state in scenario"} */
1126
1127 if (ldv_undef_int()) {
1128 /* LDV {"action": "ASSIGN", "type": "CONDITION_BEGIN", "comment": "Get network device structure."} */
1129 ldv_8_netdev = arg0;
1130 /* LDV {"action": "ASSIGN", "type": "CONDITION_END"} */
1131
1132 /* 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."} */
1133 /* LDV {"type": "CALLBACK", "call": "ldv_8_ret = ldv_emg_wrapper_dnet_open_2(ldv_8_netdev);", "comment": "open"} */
1134 ldv_8_ret = ldv_emg_wrapper_dnet_open_2(ldv_8_netdev);
1135 /* LDV {"action": "OPEN_2", "type": "CALL_END"} */
1136
1137 if (ldv_undef_int()) {
1138 /* LDV {"action": "OPEN_SUCCESS", "type": "CONDITION_BEGIN", "comment": "Network device is in the up state."} */
1139 ldv_assume(ldv_8_ret == 0);
1140 /* LDV {"action": "OPEN_SUCCESS", "type": "CONDITION_END"} */
1141
1142 /* LDV {"action": "REGISTER", "type": "DISPATCH_BEGIN", "comment": "Register network device callbacks."} */
1143 ldv_dispatch_register_8_4(ldv_8_netdev);
1144 /* LDV {"action": "REGISTER", "type": "DISPATCH_END"} */
1145
1146 /* LDV {"action": "SUCCESS", "type": "CONDITION_BEGIN", "comment": "Registration of the network device has successfully finished."} */
1147 return 0;
1148 /* LDV {"action": "SUCCESS", "type": "CONDITION_END"} */
1149
1150 /* Exit function at a terminal state */
1151 }
1152 else {
1153 /* LDV {"action": "OPEN_FAIL", "type": "CONDITION_BEGIN", "comment": "Open at the registration of the network device has failed."} */
1154 ldv_assume(ldv_8_ret != 0);
1155 ldv_failed_register_netdev();
1156 return ldv_undef_int_negative();
1157 /* LDV {"action": "OPEN_FAIL", "type": "CONDITION_END"} */
1158
1159 /* Exit function at a terminal state */
1160 }
1161 }
1162 else {
1163 /* LDV {"action": "FAIL", "type": "CONDITION_BEGIN", "comment": "Registration of the network device has failed."} */
1164 ldv_failed_register_netdev();
1165 return ldv_undef_int_negative();
1166 /* LDV {"action": "FAIL", "type": "CONDITION_END"} */
1167
1168 /* Exit function at a terminal state */
1169 }
1170 /* End of the process */
1171 /* LDV {"comment": "End of control function based on process 'register_netdev'", "type": "CONTROL_FUNCTION_END", "function": "ldv_emg_register_netdev"} */
1172 }
1173
(1-1/2)