[PATCH v3 0/4] address violation of MISRA C:2012 Rule 13.1

Simone Ballarin posted 4 patches 3 months ago
Patches applied successfully (tree, apply log)
git fetch https://gitlab.com/xen-project/patchew/xen tags/patchew/cover.1706700228.git.maria.celeste.cesario@bugseng.com
There is a newer version of this series
.../eclair_analysis/ECLAIR/analysis.ecl       |   1 +
automation/eclair_analysis/prepare.sh         |   2 +
docs/misra/safe.json                          |  16 +
docs/properties.json                          | 841 ++++++++++++++++++
docs/properties.rst                           |  58 ++
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 +-
13 files changed, 948 insertions(+), 10 deletions(-)
create mode 100644 docs/properties.json
create mode 100644 docs/properties.rst
[PATCH v3 0/4] address violation of MISRA C:2012 Rule 13.1
Posted by Simone Ballarin 3 months ago
From: Maria Celeste Cesario <maria.celeste.cesario@bugseng.com>

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 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: add and manage properties

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 +
 automation/eclair_analysis/prepare.sh         |   2 +
 docs/misra/safe.json                          |  16 +
 docs/properties.json                          | 841 ++++++++++++++++++
 docs/properties.rst                           |  58 ++
 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 +-
 13 files changed, 948 insertions(+), 10 deletions(-)
 create mode 100644 docs/properties.json
 create mode 100644 docs/properties.rst

-- 
2.40.0
Re: [PATCH v3 0/4] address violation of MISRA C:2012 Rule 13.1
Posted by Simone Ballarin 3 months ago
On 02/02/24 10:37, Simone Ballarin wrote:
> From: Maria Celeste Cesario <maria.celeste.cesario@bugseng.com>
> 
> 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 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: add and manage properties
> 
> 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 +
>   automation/eclair_analysis/prepare.sh         |   2 +
>   docs/misra/safe.json                          |  16 +
>   docs/properties.json                          | 841 ++++++++++++++++++
>   docs/properties.rst                           |  58 ++
>   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 +-
>   13 files changed, 948 insertions(+), 10 deletions(-)
>   create mode 100644 docs/properties.json
>   create mode 100644 docs/properties.rst
> 

Sorry, patch "eclair: add and manage properties" is incomplete,
please ignore this series: v4 has already been submitted.

-- 
Simone Ballarin, M.Sc.

Field Application Engineer, BUGSENG (https://bugseng.com)