Coverage Instrumentation for MC/DC. More...

#include <util/expr_util.h>
#include <langapi/language_util.h>
#include "cover_instrument.h"
#include "cover_util.h"
#include <algorithm>
#include <iterator>
#include <map>

Include dependency graph for cover_instrument_mcdc.cpp:

Go to the source code of this file.

Functions
void	collect_mcdc_controlling_rec (const exprt &src, const std::vector< exprt > &conditions, std::set< exprt > &result)
	To recursively collect controlling exprs for for mcdc coverage. More...

std::set< exprt >	collect_mcdc_controlling (const std::set< exprt > &decisions)

std::set< exprt >	replacement_conjunction (const std::set< exprt > &replacement_exprs, const std::vector< exprt > &operands, const std::size_t i)
	To replace the i-th expr of ''operands'' with each expr inside ''replacement_exprs''. More...

std::set< exprt >	collect_mcdc_controlling_nested (const std::set< exprt > &decisions)
	This nested method iteratively applies ''collect_mcdc_controlling'' to every non-atomic expr within a decision. More...

std::set< signed >	sign_of_expr (const exprt &e, const exprt &E)
	The sign of expr ''e'' within the super-expr ''E''. More...

void	remove_repetition (std::set< exprt > &exprs)
	After the ''collect_mcdc_controlling_nested'', there can be the recurrence of the same expr in the resulted set of exprs, and this method will remove the repetitive ones. More...

bool	eval_expr (const std::map< exprt, signed > &atomic_exprs, const exprt &src)
	To evaluate the value of expr ''src'', according to the atomic expr values. More...

std::map< exprt, signed >	values_of_atomic_exprs (const exprt &e, const std::set< exprt > &conditions)
	To obtain values of atomic exprs within the super expr. More...

bool	is_mcdc_pair (const exprt &e1, const exprt &e2, const exprt &c, const std::set< exprt > &conditions, const exprt &decision)
	To check if the two input controlling exprs are mcdc pairs regarding an atomic expr ''c''. More...

bool	has_mcdc_pair (const exprt &c, const std::set< exprt > &expr_set, const std::set< exprt > &conditions, const exprt &decision)
	To check if we can find the mcdc pair of the input ''expr_set'' regarding the atomic expr ''c''. More...

void	minimize_mcdc_controlling (std::set< exprt > &controlling, const exprt &decision)
	This method minimizes the controlling conditions for mcdc coverage. More...

Detailed Description

Coverage Instrumentation for MC/DC.

Definition in file cover_instrument_mcdc.cpp.

Function Documentation

◆ collect_mcdc_controlling()

std::set<exprt> collect_mcdc_controlling ( const std::set< exprt > & decisions )

Definition at line 131 of file cover_instrument_mcdc.cpp.

◆ collect_mcdc_controlling_nested()

std::set<exprt> collect_mcdc_controlling_nested ( const std::set< exprt > & decisions )

This nested method iteratively applies ''collect_mcdc_controlling'' to every non-atomic expr within a decision.

Definition at line 166 of file cover_instrument_mcdc.cpp.

◆ collect_mcdc_controlling_rec()

void collect_mcdc_controlling_rec	(	const exprt &	src,
		const std::vector< exprt > &	conditions,
		std::set< exprt > &	result
	)

To recursively collect controlling exprs for for mcdc coverage.

Definition at line 24 of file cover_instrument_mcdc.cpp.

◆ eval_expr()

bool eval_expr	(	const std::map< exprt, signed > &	atomic_exprs,
		const exprt &	src
	)

To evaluate the value of expr ''src'', according to the atomic expr values.

Definition at line 395 of file cover_instrument_mcdc.cpp.

◆ has_mcdc_pair()

bool has_mcdc_pair	(	const exprt &	c,
		const std::set< exprt > &	expr_set,
		const std::set< exprt > &	conditions,
		const exprt &	decision
	)

To check if we can find the mcdc pair of the input ''expr_set'' regarding the atomic expr ''c''.

Definition at line 525 of file cover_instrument_mcdc.cpp.

◆ is_mcdc_pair()

bool is_mcdc_pair	(	const exprt &	e1,
		const exprt &	e2,
		const exprt &	c,
		const std::set< exprt > &	conditions,
		const exprt &	decision
	)

To check if the two input controlling exprs are mcdc pairs regarding an atomic expr ''c''.

A mcdc pair of (e1, e2) regarding ''c'' means that ''e1'' and ''e2'' result in different ''decision'' values, and this is caused by the different choice of ''c'' value.

Definition at line 464 of file cover_instrument_mcdc.cpp.

◆ minimize_mcdc_controlling()

void minimize_mcdc_controlling	(	std::set< exprt > &	controlling,
		const exprt &	decision
	)

This method minimizes the controlling conditions for mcdc coverage.

The minimum is in a sense that by deleting any controlling condition in the set, the mcdc coverage for the decision will be not complete.

parameters: The input ''controlling'' should have been processed by: ''collect_mcdc_controlling_nested'' and ''remove_repetition''

Definition at line 550 of file cover_instrument_mcdc.cpp.

◆ remove_repetition()

void remove_repetition ( std::set< exprt > & exprs )

After the ''collect_mcdc_controlling_nested'', there can be the recurrence of the same expr in the resulted set of exprs, and this method will remove the repetitive ones.

Definition at line 312 of file cover_instrument_mcdc.cpp.

◆ replacement_conjunction()

std::set<exprt> replacement_conjunction	(	const std::set< exprt > &	replacement_exprs,
		const std::vector< exprt > &	operands,
		const std::size_t	i
	)

To replace the i-th expr of ''operands'' with each expr inside ''replacement_exprs''.

Definition at line 143 of file cover_instrument_mcdc.cpp.

◆ sign_of_expr()

std::set<signed> sign_of_expr	(	const exprt &	e,
		const exprt &	E
	)

The sign of expr ''e'' within the super-expr ''E''.

parameters: E should be the pre-processed output by: ''collect_mcdc_controlling_nested''

Returns: +1 : not negated -1 : negated

Definition at line 258 of file cover_instrument_mcdc.cpp.

◆ values_of_atomic_exprs()

std::map<exprt, signed> values_of_atomic_exprs	(	const exprt &	e,
		const std::set< exprt > &	conditions
	)

To obtain values of atomic exprs within the super expr.

Definition at line 439 of file cover_instrument_mcdc.cpp.

Functions