MC/DC support for gcov?

MC/DC support for gcov?

[Sebastian Huber]

Hello,

gcov supports currently branch coverage. Some projects require modified 
condition/decision coverage (MC/DC):

https://en.wikipedia.org/wiki/Modified_condition/decision_coverage

In general, 100% branch coverage does not imply 100% MC/DC coverage:

https://www.adacore.com/uploads_gems/Couverture_ERTS-2012.pdf

The paper contains a criterion under which 100% branch coverage implies 
100% MC/DC coverage:

"Theorem 1 If the BDD of a decision D is a tree (with
only one path from the root to any condition node),
then BDD edge coverage implies MCDC"

The BDD is the Binary Decision Diagram. I have no idea how the compiler 
and the coverage supports works in GCC. Is this BDD available for the 
coverage support and could the coverage support check for this property 
and then for example add it to the gcov information? If the BDD of a 
decision is not a tree, then we would have to record which paths through 
the BDD are covered to get the MC/DC coverage. This would require extra 
storage and instrumentation. According to the paper, the BDD is usually 
a tree in real world applications. Does this sound like feasible feature 
for GCC? Could it be even a GSoC project?

Kind regards,
	Sebastian

-- 
embedded brains GmbH
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.huber@embedded-brains.de
phone: +49-89-18 94 741 - 16
fax:   +49-89-18 94 741 - 08

Registergericht: Amtsgericht München
Registernummer: HRB 157899
Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler
Unsere Datenschutzerklärung finden Sie hier:
https://embedded-brains.de/datenschutzerklaerung/

Re: MC/DC support for gcov?

[Martin Liška]

On 3/31/22 16:55, Sebastian Huber wrote:
> Hello,
> 
> gcov supports currently branch coverage. Some projects require modified condition/decision coverage (MC/DC):
> 
> https://en.wikipedia.org/wiki/Modified_condition/decision_coverage
> 
> In general, 100% branch coverage does not imply 100% MC/DC coverage:
> 
> https://www.adacore.com/uploads_gems/Couverture_ERTS-2012.pdf
> 
> The paper contains a criterion under which 100% branch coverage implies 100% MC/DC coverage:
> 
> "Theorem 1 If the BDD of a decision D is a tree (with
> only one path from the root to any condition node),
> then BDD edge coverage implies MCDC"
> 
> The BDD is the Binary Decision Diagram. I have no idea how the compiler and the coverage supports works in GCC. Is this BDD available for the coverage support and could the coverage support check for this property and then for example add it to the gcov information? If the BDD of a decision is not a tree, then we would have to record which paths through the BDD are covered to get the MC/DC coverage. This would require extra storage and instrumentation. According to the paper, the BDD is usually a tree in real world applications. Does this sound like feasible feature for GCC? Could it be even a GSoC project?
> 
> Kind regards,
>      Sebastian
> 

Hi.

There's a patch review for the feature:
https://gcc.gnu.org/pipermail/gcc-patches/2022-March/592065.html

Martin