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

[Simone Ballarin <simone.ballarin@bugseng.com>]

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(+)

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.
-- 
2.34.1