diff mbox series

[XEN,2/4] automation/eclair: add deviations and call properties.

Message ID 8f426cc761c734d457a74416dd5b83fd10128c26.1697638210.git.simone.ballarin@bugseng.com (mailing list archive)
State New, archived
Headers show
Series xen: address violations of Rule 13.1 | expand

Commit Message

Simone Ballarin Oct. 18, 2023, 2:18 p.m. UTC
Deviate violations of MISRA C:2012 Rule 13.1 caused by
functions vcpu_runnable and __bad_atomic_size. These functions
contain side-effects such as debugging logs, assertions and
failures that cannot cause unexpected behaviors.

Add "noeffect" call property to functions read_u.*_atomic and
get_cycles.

Signed-off-by: Simone Ballarin <simone.ballarin@bugseng.com>
---
 .../eclair_analysis/ECLAIR/call_properties.ecl      | 10 ++++++++++
 automation/eclair_analysis/ECLAIR/deviations.ecl    | 13 +++++++++++++
 docs/misra/deviations.rst                           | 11 +++++++++++
 3 files changed, 34 insertions(+)

Comments

Stefano Stabellini Oct. 19, 2023, 12:57 a.m. UTC | #1
On Wed, 18 Oct 2023, Simone Ballarin wrote:
> Deviate violations of MISRA C:2012 Rule 13.1 caused by
> functions vcpu_runnable and __bad_atomic_size. These functions
> contain side-effects such as debugging logs, assertions and
> failures that cannot cause unexpected behaviors.
> 
> Add "noeffect" call property to functions read_u.*_atomic and
> get_cycles.
> 
> Signed-off-by: Simone Ballarin <simone.ballarin@bugseng.com>

Acked-by: Stefano Stabellini <sstabellini@kernel.org>

However one comment below


> ---
>  .../eclair_analysis/ECLAIR/call_properties.ecl      | 10 ++++++++++
>  automation/eclair_analysis/ECLAIR/deviations.ecl    | 13 +++++++++++++
>  docs/misra/deviations.rst                           | 11 +++++++++++
>  3 files changed, 34 insertions(+)
> 
> diff --git a/automation/eclair_analysis/ECLAIR/call_properties.ecl b/automation/eclair_analysis/ECLAIR/call_properties.ecl
> index 3f7794bf8b..f410a6aa58 100644
> --- a/automation/eclair_analysis/ECLAIR/call_properties.ecl
> +++ b/automation/eclair_analysis/ECLAIR/call_properties.ecl
> @@ -104,3 +104,13 @@ Furthermore, their uses do initialize the involved variables as needed by futher
>  -call_properties+={"macro(^(__)?(raw_)?copy_from_(paddr|guest|compat)(_offset)?$)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
>  -call_properties+={"macro(^(__)?copy_to_(guest|compat)(_offset)?$)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
>  -doc_end
> +
> +-doc_begin="Functions generated by build_atomic_read cannot be considered pure
> +since the input pointer is volatile."
> +-call_properties+={"^read_u(8|16|32|64|int)_atomic.*$", {"noeffect"}}
> +-doc_end
> +
> +-doc_begin="get_cycles does not perform visible side-effects "
> +-call_property+={"name(get_cycles)", {"noeffect"}}
> +-doc_end
> +
> diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/automation/eclair_analysis/ECLAIR/deviations.ecl
> index fa56e5c00a..b80ccea7bc 100644
> --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
> +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
> @@ -233,6 +233,19 @@ this."
>  -config=MC3R1.R10.1,etypes+={safe,
>    "stmt(operator(and||or||xor||not||and_assign||or_assign||xor_assign))",
>    "any()"}
> +#
> +# Series 13.
> +#
> +
> +-doc_begin="Function __bad_atomic_size is intended to generate a linkage error
> +if invoked. Calling it in intentionally unreachable switch cases is safe even
> +in a initializer list."
> +-config=MC3R1.R13.1,reports+={safe, "first_area(^.*__bad_atomic_size.*$)"}
> +-doc_end
> +
> +-doc_begin="Function vcpu_runnable contains pragmas and other side-effects for
> +debugging purposes, their invocation is safe even in a initializer list."
> +-config=MC3R1.R13.1,reports+={safe, "first_area(^.*vcpu_runnable.*$)"}
>  -doc_end
>  
>  -doc_begin="See Section \"4.5 Integers\" of \"GCC_MANUAL\", where it says that
> diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
> index 8511a18925..2fcdb8da58 100644
> --- a/docs/misra/deviations.rst
> +++ b/docs/misra/deviations.rst
> @@ -192,6 +192,17 @@ Deviations related to MISRA C:2012 Rules:
>         See automation/eclair_analysis/deviations.ecl for the full explanation.
>       - Tagged as `safe` for ECLAIR.
>  
> +   * - R13.1
> +     - Function __bad_atomic_size is intended to generate a linkage error if
> +       invoked. Calling it in intentionally unreachable switch cases is
> +       safe even in a initializer list.
> +     - Tagged as `safe` for ECLAIR.
> +
> +   * - R13.1
> +     - Function vcpu_runnable contains pragmas and other side-effects for
> +       debugging purposes, their invocation is safe even in a initializer list.
> +     - Tagged as `safe` for ECLAIR.


Would it be possible to use SAF instead? If not, this is fine.
Simone Ballarin Oct. 19, 2023, 7:44 a.m. UTC | #2
On 19/10/23 02:57, Stefano Stabellini wrote:
> On Wed, 18 Oct 2023, Simone Ballarin wrote:
>> Deviate violations of MISRA C:2012 Rule 13.1 caused by
>> functions vcpu_runnable and __bad_atomic_size. These functions
>> contain side-effects such as debugging logs, assertions and
>> failures that cannot cause unexpected behaviors.
>>
>> Add "noeffect" call property to functions read_u.*_atomic and
>> get_cycles.
>>
>> Signed-off-by: Simone Ballarin <simone.ballarin@bugseng.com>
> 
> Acked-by: Stefano Stabellini <sstabellini@kernel.org>
> 
> However one comment below
> 
> 
>> ---
>>   .../eclair_analysis/ECLAIR/call_properties.ecl      | 10 ++++++++++
>>   automation/eclair_analysis/ECLAIR/deviations.ecl    | 13 +++++++++++++
>>   docs/misra/deviations.rst                           | 11 +++++++++++
>>   3 files changed, 34 insertions(+)
>>
>> diff --git a/automation/eclair_analysis/ECLAIR/call_properties.ecl b/automation/eclair_analysis/ECLAIR/call_properties.ecl
>> index 3f7794bf8b..f410a6aa58 100644
>> --- a/automation/eclair_analysis/ECLAIR/call_properties.ecl
>> +++ b/automation/eclair_analysis/ECLAIR/call_properties.ecl
>> @@ -104,3 +104,13 @@ Furthermore, their uses do initialize the involved variables as needed by futher
>>   -call_properties+={"macro(^(__)?(raw_)?copy_from_(paddr|guest|compat)(_offset)?$)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
>>   -call_properties+={"macro(^(__)?copy_to_(guest|compat)(_offset)?$)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
>>   -doc_end
>> +
>> +-doc_begin="Functions generated by build_atomic_read cannot be considered pure
>> +since the input pointer is volatile."
>> +-call_properties+={"^read_u(8|16|32|64|int)_atomic.*$", {"noeffect"}}
>> +-doc_end
>> +
>> +-doc_begin="get_cycles does not perform visible side-effects "
>> +-call_property+={"name(get_cycles)", {"noeffect"}}
>> +-doc_end
>> +
>> diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/automation/eclair_analysis/ECLAIR/deviations.ecl
>> index fa56e5c00a..b80ccea7bc 100644
>> --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
>> +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
>> @@ -233,6 +233,19 @@ this."
>>   -config=MC3R1.R10.1,etypes+={safe,
>>     "stmt(operator(and||or||xor||not||and_assign||or_assign||xor_assign))",
>>     "any()"}
>> +#
>> +# Series 13.
>> +#
>> +
>> +-doc_begin="Function __bad_atomic_size is intended to generate a linkage error
>> +if invoked. Calling it in intentionally unreachable switch cases is safe even
>> +in a initializer list."
>> +-config=MC3R1.R13.1,reports+={safe, "first_area(^.*__bad_atomic_size.*$)"}
>> +-doc_end
>> +
>> +-doc_begin="Function vcpu_runnable contains pragmas and other side-effects for
>> +debugging purposes, their invocation is safe even in a initializer list."
>> +-config=MC3R1.R13.1,reports+={safe, "first_area(^.*vcpu_runnable.*$)"}
>>   -doc_end
>>   
>>   -doc_begin="See Section \"4.5 Integers\" of \"GCC_MANUAL\", where it says that
>> diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
>> index 8511a18925..2fcdb8da58 100644
>> --- a/docs/misra/deviations.rst
>> +++ b/docs/misra/deviations.rst
>> @@ -192,6 +192,17 @@ Deviations related to MISRA C:2012 Rules:
>>          See automation/eclair_analysis/deviations.ecl for the full explanation.
>>        - Tagged as `safe` for ECLAIR.
>>   
>> +   * - R13.1
>> +     - Function __bad_atomic_size is intended to generate a linkage error if
>> +       invoked. Calling it in intentionally unreachable switch cases is
>> +       safe even in a initializer list.
>> +     - Tagged as `safe` for ECLAIR.
>> +
>> +   * - R13.1
>> +     - Function vcpu_runnable contains pragmas and other side-effects for
>> +       debugging purposes, their invocation is safe even in a initializer list.
>> +     - Tagged as `safe` for ECLAIR.
> 
> 
> Would it be possible to use SAF instead? If not, this is fine.

Yes, but I do not suggest using SAF comments in these cases.
The SAF should be placed before every non-compliant invocation and not 
only in the declaration, this could cause a lot of SAF comments instead
of a simple deviation.
Julien Grall Oct. 19, 2023, 8:26 a.m. UTC | #3
Hi Simone,

On 19/10/2023 08:44, Simone Ballarin wrote:
> On 19/10/23 02:57, Stefano Stabellini wrote:
>> On Wed, 18 Oct 2023, Simone Ballarin wrote:
>>> Deviate violations of MISRA C:2012 Rule 13.1 caused by
>>> functions vcpu_runnable and __bad_atomic_size. These functions
>>> contain side-effects such as debugging logs, assertions and
>>> failures that cannot cause unexpected behaviors.
>>>
>>> Add "noeffect" call property to functions read_u.*_atomic and
>>> get_cycles.
>>>
>>> Signed-off-by: Simone Ballarin <simone.ballarin@bugseng.com>
>>
>> Acked-by: Stefano Stabellini <sstabellini@kernel.org>
>>
>> However one comment below
>>
>>
>>> ---
>>>   .../eclair_analysis/ECLAIR/call_properties.ecl      | 10 ++++++++++
>>>   automation/eclair_analysis/ECLAIR/deviations.ecl    | 13 +++++++++++++
>>>   docs/misra/deviations.rst                           | 11 +++++++++++
>>>   3 files changed, 34 insertions(+)
>>>
>>> diff --git a/automation/eclair_analysis/ECLAIR/call_properties.ecl 
>>> b/automation/eclair_analysis/ECLAIR/call_properties.ecl
>>> index 3f7794bf8b..f410a6aa58 100644
>>> --- a/automation/eclair_analysis/ECLAIR/call_properties.ecl
>>> +++ b/automation/eclair_analysis/ECLAIR/call_properties.ecl
>>> @@ -104,3 +104,13 @@ Furthermore, their uses do initialize the 
>>> involved variables as needed by futher
>>>   
>>> -call_properties+={"macro(^(__)?(raw_)?copy_from_(paddr|guest|compat)(_offset)?$)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
>>>   
>>> -call_properties+={"macro(^(__)?copy_to_(guest|compat)(_offset)?$)", 
>>> {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
>>>   -doc_end
>>> +
>>> +-doc_begin="Functions generated by build_atomic_read cannot be 
>>> considered pure
>>> +since the input pointer is volatile."
>>> +-call_properties+={"^read_u(8|16|32|64|int)_atomic.*$", {"noeffect"}}
>>> +-doc_end
>>> +
>>> +-doc_begin="get_cycles does not perform visible side-effects "
>>> +-call_property+={"name(get_cycles)", {"noeffect"}}
>>> +-doc_end
>>> +
>>> diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl 
>>> b/automation/eclair_analysis/ECLAIR/deviations.ecl
>>> index fa56e5c00a..b80ccea7bc 100644
>>> --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
>>> +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
>>> @@ -233,6 +233,19 @@ this."
>>>   -config=MC3R1.R10.1,etypes+={safe,
>>>     
>>> "stmt(operator(and||or||xor||not||and_assign||or_assign||xor_assign))",
>>>     "any()"}
>>> +#
>>> +# Series 13.
>>> +#
>>> +
>>> +-doc_begin="Function __bad_atomic_size is intended to generate a 
>>> linkage error
>>> +if invoked. Calling it in intentionally unreachable switch cases is 
>>> safe even
>>> +in a initializer list."
>>> +-config=MC3R1.R13.1,reports+={safe, 
>>> "first_area(^.*__bad_atomic_size.*$)"}
>>> +-doc_end
>>> +
>>> +-doc_begin="Function vcpu_runnable contains pragmas and other 
>>> side-effects for
>>> +debugging purposes, their invocation is safe even in a initializer 
>>> list."
>>> +-config=MC3R1.R13.1,reports+={safe, "first_area(^.*vcpu_runnable.*$)"}
>>>   -doc_end
>>>   -doc_begin="See Section \"4.5 Integers\" of \"GCC_MANUAL\", where 
>>> it says that
>>> diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
>>> index 8511a18925..2fcdb8da58 100644
>>> --- a/docs/misra/deviations.rst
>>> +++ b/docs/misra/deviations.rst
>>> @@ -192,6 +192,17 @@ Deviations related to MISRA C:2012 Rules:
>>>          See automation/eclair_analysis/deviations.ecl for the full 
>>> explanation.
>>>        - Tagged as `safe` for ECLAIR.
>>> +   * - R13.1
>>> +     - Function __bad_atomic_size is intended to generate a linkage 
>>> error if
>>> +       invoked. Calling it in intentionally unreachable switch cases is
>>> +       safe even in a initializer list.
>>> +     - Tagged as `safe` for ECLAIR.
>>> +
>>> +   * - R13.1
>>> +     - Function vcpu_runnable contains pragmas and other 
>>> side-effects for
>>> +       debugging purposes, their invocation is safe even in a 
>>> initializer list.
>>> +     - Tagged as `safe` for ECLAIR.
>>
>>
>> Would it be possible to use SAF instead? If not, this is fine.
> 
> Yes, but I do not suggest using SAF comments in these cases.

There are not many use of __bad_atomic_size() and I don't expect much 
more. So I think SAF- makes more sense.

For vcpu_runnable(), I don't quite understand the argument. I can't find 
any pragma around the function and I can't find any side-effects in it. 
Can you clarify?

Cheers,
Simone Ballarin Oct. 19, 2023, 9:04 a.m. UTC | #4
On 19/10/23 10:26, Julien Grall wrote:
> Hi Simone,
> 
> On 19/10/2023 08:44, Simone Ballarin wrote:
>> On 19/10/23 02:57, Stefano Stabellini wrote:
>>> On Wed, 18 Oct 2023, Simone Ballarin wrote:
>>>> Deviate violations of MISRA C:2012 Rule 13.1 caused by
>>>> functions vcpu_runnable and __bad_atomic_size. These functions
>>>> contain side-effects such as debugging logs, assertions and
>>>> failures that cannot cause unexpected behaviors.
>>>>
>>>> Add "noeffect" call property to functions read_u.*_atomic and
>>>> get_cycles.
>>>>
>>>> Signed-off-by: Simone Ballarin <simone.ballarin@bugseng.com>
>>>
>>> Acked-by: Stefano Stabellini <sstabellini@kernel.org>
>>>
>>> However one comment below
>>>
>>>
>>>> ---
>>>>   .../eclair_analysis/ECLAIR/call_properties.ecl      | 10 ++++++++++
>>>>   automation/eclair_analysis/ECLAIR/deviations.ecl    | 13 
>>>> +++++++++++++
>>>>   docs/misra/deviations.rst                           | 11 +++++++++++
>>>>   3 files changed, 34 insertions(+)
>>>>
>>>> diff --git a/automation/eclair_analysis/ECLAIR/call_properties.ecl 
>>>> b/automation/eclair_analysis/ECLAIR/call_properties.ecl
>>>> index 3f7794bf8b..f410a6aa58 100644
>>>> --- a/automation/eclair_analysis/ECLAIR/call_properties.ecl
>>>> +++ b/automation/eclair_analysis/ECLAIR/call_properties.ecl
>>>> @@ -104,3 +104,13 @@ Furthermore, their uses do initialize the 
>>>> involved variables as needed by futher
>>>> -call_properties+={"macro(^(__)?(raw_)?copy_from_(paddr|guest|compat)(_offset)?$)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
>>>> -call_properties+={"macro(^(__)?copy_to_(guest|compat)(_offset)?$)", 
>>>> {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
>>>>   -doc_end
>>>> +
>>>> +-doc_begin="Functions generated by build_atomic_read cannot be 
>>>> considered pure
>>>> +since the input pointer is volatile."
>>>> +-call_properties+={"^read_u(8|16|32|64|int)_atomic.*$", {"noeffect"}}
>>>> +-doc_end
>>>> +
>>>> +-doc_begin="get_cycles does not perform visible side-effects "
>>>> +-call_property+={"name(get_cycles)", {"noeffect"}}
>>>> +-doc_end
>>>> +
>>>> diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl 
>>>> b/automation/eclair_analysis/ECLAIR/deviations.ecl
>>>> index fa56e5c00a..b80ccea7bc 100644
>>>> --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
>>>> +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
>>>> @@ -233,6 +233,19 @@ this."
>>>>   -config=MC3R1.R10.1,etypes+={safe,
>>>> "stmt(operator(and||or||xor||not||and_assign||or_assign||xor_assign))",
>>>>     "any()"}
>>>> +#
>>>> +# Series 13.
>>>> +#
>>>> +
>>>> +-doc_begin="Function __bad_atomic_size is intended to generate a 
>>>> linkage error
>>>> +if invoked. Calling it in intentionally unreachable switch cases is 
>>>> safe even
>>>> +in a initializer list."
>>>> +-config=MC3R1.R13.1,reports+={safe, 
>>>> "first_area(^.*__bad_atomic_size.*$)"}
>>>> +-doc_end
>>>> +
>>>> +-doc_begin="Function vcpu_runnable contains pragmas and other 
>>>> side-effects for
>>>> +debugging purposes, their invocation is safe even in a initializer 
>>>> list."
>>>> +-config=MC3R1.R13.1,reports+={safe, "first_area(^.*vcpu_runnable.*$)"}
>>>>   -doc_end
>>>>   -doc_begin="See Section \"4.5 Integers\" of \"GCC_MANUAL\", where 
>>>> it says that
>>>> diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
>>>> index 8511a18925..2fcdb8da58 100644
>>>> --- a/docs/misra/deviations.rst
>>>> +++ b/docs/misra/deviations.rst
>>>> @@ -192,6 +192,17 @@ Deviations related to MISRA C:2012 Rules:
>>>>          See automation/eclair_analysis/deviations.ecl for the full 
>>>> explanation.
>>>>        - Tagged as `safe` for ECLAIR.
>>>> +   * - R13.1
>>>> +     - Function __bad_atomic_size is intended to generate a linkage 
>>>> error if
>>>> +       invoked. Calling it in intentionally unreachable switch 
>>>> cases is
>>>> +       safe even in a initializer list.
>>>> +     - Tagged as `safe` for ECLAIR.
>>>> +
>>>> +   * - R13.1
>>>> +     - Function vcpu_runnable contains pragmas and other 
>>>> side-effects for
>>>> +       debugging purposes, their invocation is safe even in a 
>>>> initializer list.
>>>> +     - Tagged as `safe` for ECLAIR.
>>>
>>>
>>> Would it be possible to use SAF instead? If not, this is fine.
>>
>> Yes, but I do not suggest using SAF comments in these cases.
> 
> There are not many use of __bad_atomic_size() and I don't expect much 
> more. So I think SAF- makes more sense.

There are 13 invocations in the preprocessed code: some of them are 
contained in macro expansions. Adding a SAF in a macro means to add 
useless comments if the macro is not expanded in an initializer list.

The correct thing would be adding 13 SAFs. If this is ok, I can do it.

> 
> For vcpu_runnable(), I don't quite understand the argument. I can't find 
> any pragma around the function and I can't find any side-effects in it. 
> Can you clarify?
> 


vcpu_runnable calls atomic_read.

In ARM, atomic_read uses a volatile pointer (that's a side-effect).

In X86 it contains a MACRO (read_atomic) that contains the pragmas
and also __bad_atomic_size.

Maybe the text should discriminate the two cases.

> Cheers,
>
diff mbox series

Patch

diff --git a/automation/eclair_analysis/ECLAIR/call_properties.ecl b/automation/eclair_analysis/ECLAIR/call_properties.ecl
index 3f7794bf8b..f410a6aa58 100644
--- a/automation/eclair_analysis/ECLAIR/call_properties.ecl
+++ b/automation/eclair_analysis/ECLAIR/call_properties.ecl
@@ -104,3 +104,13 @@  Furthermore, their uses do initialize the involved variables as needed by futher
 -call_properties+={"macro(^(__)?(raw_)?copy_from_(paddr|guest|compat)(_offset)?$)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}}
 -call_properties+={"macro(^(__)?copy_to_(guest|compat)(_offset)?$)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}}
 -doc_end
+
+-doc_begin="Functions generated by build_atomic_read cannot be considered pure
+since the input pointer is volatile."
+-call_properties+={"^read_u(8|16|32|64|int)_atomic.*$", {"noeffect"}}
+-doc_end
+
+-doc_begin="get_cycles does not perform visible side-effects "
+-call_property+={"name(get_cycles)", {"noeffect"}}
+-doc_end
+
diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/automation/eclair_analysis/ECLAIR/deviations.ecl
index fa56e5c00a..b80ccea7bc 100644
--- a/automation/eclair_analysis/ECLAIR/deviations.ecl
+++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
@@ -233,6 +233,19 @@  this."
 -config=MC3R1.R10.1,etypes+={safe,
   "stmt(operator(and||or||xor||not||and_assign||or_assign||xor_assign))",
   "any()"}
+#
+# Series 13.
+#
+
+-doc_begin="Function __bad_atomic_size is intended to generate a linkage error
+if invoked. Calling it in intentionally unreachable switch cases is safe even
+in a initializer list."
+-config=MC3R1.R13.1,reports+={safe, "first_area(^.*__bad_atomic_size.*$)"}
+-doc_end
+
+-doc_begin="Function vcpu_runnable contains pragmas and other side-effects for
+debugging purposes, their invocation is safe even in a initializer list."
+-config=MC3R1.R13.1,reports+={safe, "first_area(^.*vcpu_runnable.*$)"}
 -doc_end
 
 -doc_begin="See Section \"4.5 Integers\" of \"GCC_MANUAL\", where it says that
diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
index 8511a18925..2fcdb8da58 100644
--- a/docs/misra/deviations.rst
+++ b/docs/misra/deviations.rst
@@ -192,6 +192,17 @@  Deviations related to MISRA C:2012 Rules:
        See automation/eclair_analysis/deviations.ecl for the full explanation.
      - Tagged as `safe` for ECLAIR.
 
+   * - R13.1
+     - Function __bad_atomic_size is intended to generate a linkage error if
+       invoked. Calling it in intentionally unreachable switch cases is
+       safe even in a initializer list.
+     - Tagged as `safe` for ECLAIR.
+
+   * - R13.1
+     - Function vcpu_runnable contains pragmas and other side-effects for
+       debugging purposes, their invocation is safe even in a initializer list.
+     - Tagged as `safe` for ECLAIR.
+
    * - R13.5
      - All developers and reviewers can be safely assumed to be well aware of
        the short-circuit evaluation strategy for logical operators.