Loading...

Searching...

No Matches

cover.cpp File Reference

Coverage Instrumentation. More...

#include "cover.h"
#include <util/message.h>
#include <util/cmdline.h>
#include <util/options.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_skip.h>
#include "cover_basic_blocks.h"

+ Include dependency graph for cover.cpp:

[フレーム]

Go to the source code of this file.

Functions

static void instrument_cover_goals (const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler, const cover_instrumenter_baset::assertion_factoryt &make_assertion)

Applies instrumenters to given goto program.

coverage_criteriont parse_coverage_criterion (const std::string &criterion_string)

Parses a coverage criterion.

void parse_cover_options (const cmdlinet &cmdline, optionst &options)

Parses coverage-related command line options.

cover_configt get_cover_config (const optionst &options, const symbol_tablet &symbol_table, message_handlert &message_handler)

Build data structures controlling coverage from command-line options.

cover_configt get_cover_config (const optionst &options, const irep_idt &main_function_id, const symbol_tablet &symbol_table, message_handlert &message_handler)

Build data structures controlling coverage from command-line options.

static void instrument_cover_goals (const cover_configt &cover_config, const symbolt &function_symbol, goto_functionst::goto_functiont &function, message_handlert &message_handler)

Instruments a single goto program based on the given configuration.

void instrument_cover_goals (const cover_configt &cover_config, goto_model_functiont &function, message_handlert &message_handler)

Instruments a single goto program based on the given configuration.

bool instrument_cover_goals (const cover_configt &cover_config, const symbol_tablet &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)

Instruments goto functions based on given command line options.

bool instrument_cover_goals (const cover_configt &cover_config, goto_modelt &goto_model, message_handlert &message_handler)

Instruments a goto model based on given command line options.

Detailed Description

Coverage Instrumentation.

Definition in file cover.cpp.

Function Documentation

◆ get_cover_config() [1/2]

cover_configt get_cover_config ( const optionst & options,

const irep_idt & main_function_id,

const symbol_tablet & symbol_table,

message_handlert & message_handler

)

Build data structures controlling coverage from command-line options.

Include options that depend on the main function specified by the user.

Parameters: options command-line options

main_function_id symbol of the user-specified main program function

symbol_table global symbol table

message_handler used to log incorrect option specifications

Returns: a cover_configt on success, or null otherwise.

Definition at line 247 of file cover.cpp.

◆ get_cover_config() [2/2]

cover_configt get_cover_config ( const optionst & options,

const symbol_tablet & symbol_table,

message_handlert & message_handler

)

Build data structures controlling coverage from command-line options.

Do not include the options that depend on the main function specified by the user.

Parameters: options command-line options

symbol_table global symbol table

message_handler used to log incorrect option specifications

Returns: a cover_configt on success, or null otherwise.

Definition at line 181 of file cover.cpp.

◆ instrument_cover_goals() [1/5]

bool instrument_cover_goals ( const cover_configt & cover_config,

const symbol_tablet & symbol_table,

goto_functionst & goto_functions,

message_handlert & message_handler

)

Instruments goto functions based on given command line options.

Parameters: cover_config configuration, produced using get_cover_config

symbol_table the symbol table

goto_functions the goto functions

message_handler a message handler

Definition at line 375 of file cover.cpp.

◆ instrument_cover_goals() [2/5]

static void instrument_cover_goals ( const cover_configt & cover_config,

const symbolt & function_symbol,

goto_functionst::goto_functiont & function,

message_handlert & message_handler

)

static

Instruments a single goto program based on the given configuration.

Parameters: cover_config configuration, produced using get_cover_config

function_symbol symbol of the function to be instrumented

function function to instrument

message_handler log output

Definition at line 286 of file cover.cpp.

◆ instrument_cover_goals() [3/5]

void instrument_cover_goals ( const cover_configt & cover_config,

goto_model_functiont & function,

message_handlert & message_handler

)

Instruments a single goto program based on the given configuration.

Parameters: cover_config configuration, produced using get_cover_config

function goto program to instrument

message_handler log output

Definition at line 354 of file cover.cpp.

◆ instrument_cover_goals() [4/5]

bool instrument_cover_goals ( const cover_configt & cover_config,

goto_modelt & goto_model,

message_handlert & message_handler

)

Instruments a goto model based on given command line options.

Parameters: cover_config configuration, produced using get_cover_config

goto_model the goto model

message_handler a message handler

Definition at line 412 of file cover.cpp.

◆ instrument_cover_goals() [5/5]

static void instrument_cover_goals ( const irep_idt & function_id,

goto_programt & goto_program,

const cover_instrumenterst & instrumenters,

const irep_idt & mode,

message_handlert & message_handler,

const cover_instrumenter_baset::assertion_factoryt & make_assertion

)

static

Applies instrumenters to given goto program.

Parameters: function_id name of goto_program

goto_program the goto program

instrumenters the instrumenters

mode mode of the function to instrument (for instance ID_C or ID_java)

message_handler a message handler

make_assertion A function which takes an expression, with a source location and makes an assertion based on that expression. The expression asserted is expected to include the expression passed in, but may include other additional conditions.

Definition at line 36 of file cover.cpp.

◆ parse_cover_options()

void parse_cover_options ( const cmdlinet & cmdline,

optionst & options

)

Parses coverage-related command line options.

Parameters: cmdline the command line

options the options

Definition at line 143 of file cover.cpp.

◆ parse_coverage_criterion()

coverage_criteriont parse_coverage_criterion ( const std::string & criterion_string )

Parses a coverage criterion.

Parameters: criterion_string a string

Returns: a coverage criterion or throws an exception

Definition at line 108 of file cover.cpp.