#include <cover.h>

Collaboration diagram for cover_configt:

Public Attributes
bool	keep_assertions

bool	cover_failed_assertions

bool	traces_must_terminate

irep_idt	mode

function_filterst	function_filters

std::unique_ptr< goal_filterst >	goal_filters

cover_instrumenterst	cover_instrumenters

cover_instrumenter_baset::assertion_factoryt	make_assertion

Detailed Description

Definition at line 57 of file cover.h.

Member Data Documentation

◆ cover_failed_assertions

bool cover_configt::cover_failed_assertions

Definition at line 60 of file cover.h.

◆ cover_instrumenters

cover_instrumenterst cover_configt::cover_instrumenters

Definition at line 67 of file cover.h.

◆ function_filters

function_filterst cover_configt::function_filters

Definition at line 63 of file cover.h.

◆ goal_filters

std::unique_ptr<goal_filterst> cover_configt::goal_filters

Initial value:

=

std::make_unique<goal_filterst>()

Definition at line 65 of file cover.h.

◆ keep_assertions

bool cover_configt::keep_assertions

Definition at line 59 of file cover.h.

◆ make_assertion

cover_instrumenter_baset::assertion_factoryt cover_configt::make_assertion

Initial value:

=

goto_programt::make_assertion

static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())

Definition goto_program.h:932

Definition at line 68 of file cover.h.

◆ mode

irep_idt cover_configt::mode

Definition at line 62 of file cover.h.

◆ traces_must_terminate

bool cover_configt::traces_must_terminate

Definition at line 61 of file cover.h.

The documentation for this struct was generated from the following file:

/home/runner/work/cbmc/cbmc/src/goto-instrument/cover.h

Public Attributes