From: Simone Ballarin <simone.ballarin@bugseng.com>
To: xen-devel@lists.xenproject.org
Cc: consulting@bugseng.com, sstabellini@kernel.org,
"Simone Ballarin" <simone.ballarin@bugseng.com>,
"Andrew Cooper" <andrew.cooper3@citrix.com>,
"George Dunlap" <george.dunlap@citrix.com>,
"Jan Beulich" <jbeulich@suse.com>,
"Julien Grall" <julien@xen.org>, "Wei Liu" <wl@xen.org>,
"Bertrand Marquis" <bertrand.marquis@arm.com>,
"Michal Orzel" <michal.orzel@amd.com>,
"Volodymyr Babchuk" <Volodymyr_Babchuk@epam.com>,
"Roger Pau Monné" <roger.pau@citrix.com>,
"Dario Faggioli" <dfaggioli@suse.com>,
"Doug Goldstein" <cardoe@cardoe.com>
Subject: [XEN PATCH v4 0/4] address violation of MISRA C:2012 Rule 13.1
Date: Fri, 2 Feb 2024 16:16:01 +0100 [thread overview]
Message-ID: <cover.1706886631.git.simone.ballarin@bugseng.com> (raw)
The Xen sources contain violations of MISRA C:2012 Rule 13.1 whose headline states:
"Initializer lists shall not contain persistent side effects".
The file properties.json containing function and macro properties is introduced, as
stated in v2 discussion. Some functions and macros are found to have properties that
can be exploited by static analyzers. For this reason, the file docs/properties.json
contains all the needed properties. A description of the json file is documented in
docs/properties.rst.
Some persistent effects have been moved outside initializer lists to address violations
of Rule 13.1.
Link to the discussion: https://lore.kernel.org/all/cover.1700844359.git.simone.ballarin@bugseng.com/T/#u
Changes in v4:
- added missing script for converting function_macro_properties.json in ECL configurations
and other related improvements.
Changes in v3:
- change prefix from xen to xen/ns16550
- add assignment of rc in xen/ns16550
- use rc as controlling expression in the following if-statement
- change commit prefix from xen/arm to xen
- specify where saf-3-safe comments are applied in guestcopy.c
- reword saf comments text
Maria Celeste Cesario (1):
eclair: move function and macro properties outside ECLAIR
Simone Ballarin (3):
xen: add SAF deviation for debugging and logging effects
xen/ns16550: address violations of MISRA C:2012 Rule 13.1
xen/x86: address violations of MISRA C:2012 Rule 13.1
.../eclair_analysis/ECLAIR/analysis.ecl | 1 +
.../ECLAIR/call_properties.ecl | 128 ---
automation/eclair_analysis/prepare.sh | 2 +
automation/eclair_analysis/propertyparser.py | 37 +
docs/function_macro_properties.json | 841 ++++++++++++++++++
docs/function_macro_properties.rst | 58 ++
docs/misra/safe.json | 16 +
xen/arch/arm/device.c | 1 +
xen/arch/arm/guestcopy.c | 16 +-
xen/arch/x86/hvm/hvm.c | 1 +
xen/arch/x86/io_apic.c | 9 +-
xen/arch/x86/mpparse.c | 3 +-
xen/arch/x86/setup.c | 3 +-
xen/common/sched/core.c | 3 +
xen/drivers/char/ns16550.c | 4 +-
15 files changed, 985 insertions(+), 138 deletions(-)
delete mode 100644 automation/eclair_analysis/ECLAIR/call_properties.ecl
create mode 100644 automation/eclair_analysis/propertyparser.py
create mode 100644 docs/function_macro_properties.json
create mode 100644 docs/function_macro_properties.rst
--
2.34.1
next reply other threads:[~2024-02-02 15:17 UTC|newest]
Thread overview: 23+ messages / expand[flat|nested] mbox.gz Atom feed top
2024-02-02 15:16 Simone Ballarin [this message]
2024-02-02 15:16 ` [XEN PATCH v4 1/4] xen: add SAF deviation for debugging and logging effects Simone Ballarin
2024-02-06 12:04 ` Jan Beulich
2024-02-07 10:03 ` Simone Ballarin
2024-02-07 10:24 ` Jan Beulich
2024-02-07 12:21 ` Simone Ballarin
2024-02-07 12:40 ` Jan Beulich
2024-02-09 9:25 ` Simone Ballarin
2024-02-09 11:54 ` Jan Beulich
2024-02-09 22:08 ` Stefano Stabellini
2024-02-09 22:13 ` Stefano Stabellini
2024-02-12 7:23 ` Simone Ballarin
2024-02-02 15:16 ` [XEN PATCH v4 2/4] xen/ns16550: address violations of MISRA C:2012 Rule 13.1 Simone Ballarin
2024-02-06 13:10 ` Jan Beulich
2024-02-02 15:16 ` [XEN PATCH v4 3/4] xen/x86: " Simone Ballarin
2024-02-06 13:13 ` Jan Beulich
2024-02-07 0:56 ` Stefano Stabellini
2024-02-07 7:35 ` Jan Beulich
2024-02-07 12:28 ` Simone Ballarin
2024-02-02 15:16 ` [XEN PATCH v4 4/4] eclair: move function and macro properties outside ECLAIR Simone Ballarin
2024-02-07 0:58 ` Stefano Stabellini
2024-02-26 15:44 ` [REGRESSION] " Andrew Cooper
2024-02-27 15:39 ` Simone Ballarin
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=cover.1706886631.git.simone.ballarin@bugseng.com \
--to=simone.ballarin@bugseng.com \
--cc=Volodymyr_Babchuk@epam.com \
--cc=andrew.cooper3@citrix.com \
--cc=bertrand.marquis@arm.com \
--cc=cardoe@cardoe.com \
--cc=consulting@bugseng.com \
--cc=dfaggioli@suse.com \
--cc=george.dunlap@citrix.com \
--cc=jbeulich@suse.com \
--cc=julien@xen.org \
--cc=michal.orzel@amd.com \
--cc=roger.pau@citrix.com \
--cc=sstabellini@kernel.org \
--cc=wl@xen.org \
--cc=xen-devel@lists.xenproject.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.