2018-11-06 01:57:43 +08:00
|
|
|
/// Use unsigned int as the return value for irq_lock()
|
|
|
|
///
|
|
|
|
// Confidence: High
|
2018-08-15 08:57:08 +08:00
|
|
|
// Copyright (c) 2017 Intel Corporation
|
|
|
|
//
|
|
|
|
// SPDX-License-Identifier: Apache-2.0
|
|
|
|
|
2018-11-06 01:57:43 +08:00
|
|
|
virtual patch
|
|
|
|
|
|
|
|
@find depends on !(file in "ext")@
|
2018-08-15 08:57:08 +08:00
|
|
|
type T;
|
|
|
|
identifier i;
|
2020-05-28 00:26:57 +08:00
|
|
|
typedef uint32_t,uint32_t;
|
2018-08-15 08:57:08 +08:00
|
|
|
@@
|
|
|
|
|
2018-11-06 01:57:43 +08:00
|
|
|
(
|
|
|
|
uint32_t i = irq_lock();
|
|
|
|
|
|
|
|
|
unsigned int i = irq_lock();
|
|
|
|
|
|
2020-05-28 00:26:57 +08:00
|
|
|
uint32_t i = irq_lock();
|
2018-11-06 01:57:43 +08:00
|
|
|
|
|
|
|
|
- T
|
2018-08-15 08:57:08 +08:00
|
|
|
+ unsigned int
|
2018-11-06 01:57:43 +08:00
|
|
|
i = irq_lock();
|
|
|
|
)
|
2018-08-15 08:57:08 +08:00
|
|
|
|
2018-11-06 01:57:43 +08:00
|
|
|
@find2 depends on !(file in "ext") exists@
|
2018-08-15 08:57:08 +08:00
|
|
|
type T;
|
|
|
|
identifier i;
|
|
|
|
@@
|
|
|
|
|
2018-11-06 01:57:43 +08:00
|
|
|
(
|
|
|
|
uint32_t i;
|
|
|
|
|
|
|
|
|
unsigned int i;
|
|
|
|
|
|
2020-05-28 00:26:57 +08:00
|
|
|
uint32_t i;
|
2018-11-06 01:57:43 +08:00
|
|
|
|
|
|
|
|
- T
|
|
|
|
+ unsigned int
|
|
|
|
i;
|
|
|
|
...
|
|
|
|
i = irq_lock();
|
|
|
|
)
|