ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
goto_coveraget Class Reference

#include <goto_coverage.h>

Public Member Functions

 goto_coveraget (const namespacet &ns, goto_functionst &goto_functions)
 goto_coveraget (const namespacet &ns, goto_functionst &goto_functions, const std::string filename)
void assertion_coverage ()
void branch_coverage ()
void branch_function_coverage ()
void k_path_coverage ()
void insert_assert (goto_programt &goto_program, goto_programt::targett &it, const expr2tc &guard)
void insert_assert (goto_programt &goto_program, goto_programt::targett &it, const expr2tc &guard, const std::string &idf)
void replace_all_asserts_to_guard (const expr2tc &guard, bool is_instrumentation=false)
void replace_assert_to_guard (const expr2tc &guard, goto_programt::instructiont::targett &it, bool is_instrumentation)
void replace_assert_to_assume (goto_programt::instructiont::targett &it)
void replace_all_asserts_to_assume ()
void negating_asserts (const std::string &tgt_fname)
void condition_coverage ()
expr2tc gen_not_eq_expr (const expr2tc &lhs, const expr2tc &rhs)
expr2tc gen_and_expr (const expr2tc &lhs, const expr2tc &rhs)
expr2tc gen_not_expr (const expr2tc &expr) const
int get_total_instrument () const
int get_total_assert_instance () const
std::set< std::pair< std::string, std::string > > get_total_cond_assert () const
std::string get_filename_from_path (std::string path)
void set_target (const std::string &_tgt)
bool is_target_func (const irep_idt &f, const std::string &tgt_name) const
bool filter (const irep_idt &func_name, const goto_programt &goto_program) const

Public Attributes

std::string target_function = ""
bool cov_assume_asserts = false
size_t k_path_n = 4
size_t k_path_witness_depth = 8
size_t k_path_max_goals = 10000

Static Public Attributes

static size_t total_assert = 0
static size_t total_assert_ins = 0
static std::set< std::pair< std::string, std::string > > total_cond
static size_t total_branch = 0
static size_t total_func_branch = 0
static size_t total_kpath = 0
static size_t total_kpath_spanning = 0
static std::set< std::pair< std::string, std::string > > k_path_spanning_redundant
static std::set< std::pair< std::string, std::string > > all_claims
static std::map< std::pair< std::string, std::string >, std::string > claim_negation

Protected Member Functions

expr2tc handle_single_guard (const expr2tc &expr, bool top_level)
void handle_operands_guard (const expr2tc &expr, goto_programt &goto_program, goto_programt::instructiont::targett &it)
void add_cond_cov_assert (const expr2tc &top_ptr, const expr2tc &pre_cond, goto_programt &goto_program, goto_programt::instructiont::targett &it)
void gen_cond_cov_assert (const expr2tc &top_ptr, const expr2tc &pre_cond, goto_programt &goto_program, goto_programt::instructiont::targett &it)
 Recurse into all sub-expressions of ptr, calling gen_cond_cov_assert on each.

Protected Attributes

namespacet ns
goto_functionst & goto_functions
std::string filename
int target_num

Constructor & Destructor Documentation

◆ goto_coveraget() [1/2]

goto_coveraget::goto_coveraget ( const namespacet & ns,
goto_functionst & goto_functions )
inlineexplicit

◆ goto_coveraget() [2/2]

goto_coveraget::goto_coveraget ( const namespacet & ns,
goto_functionst & goto_functions,
const std::string filename )
inlineexplicit

Member Function Documentation

◆ add_cond_cov_assert()

void goto_coveraget::add_cond_cov_assert ( const expr2tc & top_ptr,
const expr2tc & pre_cond,
goto_programt & goto_program,
goto_programt::instructiont::targett & it )
protected

◆ assertion_coverage()

void goto_coveraget::assertion_coverage ( )

◆ branch_coverage()

void goto_coveraget::branch_coverage ( )

◆ branch_function_coverage()

void goto_coveraget::branch_function_coverage ( )

◆ condition_coverage()

void goto_coveraget::condition_coverage ( )

◆ filter()

bool goto_coveraget::filter ( const irep_idt & func_name,
const goto_programt & goto_program ) const

◆ gen_and_expr()

expr2tc goto_coveraget::gen_and_expr ( const expr2tc & lhs,
const expr2tc & rhs )

◆ gen_cond_cov_assert()

void goto_coveraget::gen_cond_cov_assert ( const expr2tc & top_ptr,
const expr2tc & pre_cond,
goto_programt & goto_program,
goto_programt::instructiont::targett & it )
protected

Recurse into all sub-expressions of ptr, calling gen_cond_cov_assert on each.

◆ gen_not_eq_expr()

expr2tc goto_coveraget::gen_not_eq_expr ( const expr2tc & lhs,
const expr2tc & rhs )

◆ gen_not_expr()

expr2tc goto_coveraget::gen_not_expr ( const expr2tc & expr) const

◆ get_filename_from_path()

std::string goto_coveraget::get_filename_from_path ( std::string path)

◆ get_total_assert_instance()

int goto_coveraget::get_total_assert_instance ( ) const

◆ get_total_cond_assert()

std::set< std::pair< std::string, std::string > > goto_coveraget::get_total_cond_assert ( ) const

◆ get_total_instrument()

int goto_coveraget::get_total_instrument ( ) const

◆ handle_operands_guard()

void goto_coveraget::handle_operands_guard ( const expr2tc & expr,
goto_programt & goto_program,
goto_programt::instructiont::targett & it )
protected

◆ handle_single_guard()

expr2tc goto_coveraget::handle_single_guard ( const expr2tc & expr,
bool top_level )
protected

◆ insert_assert() [1/2]

void goto_coveraget::insert_assert ( goto_programt & goto_program,
goto_programt::targett & it,
const expr2tc & guard )

◆ insert_assert() [2/2]

void goto_coveraget::insert_assert ( goto_programt & goto_program,
goto_programt::targett & it,
const expr2tc & guard,
const std::string & idf )

◆ is_target_func()

bool goto_coveraget::is_target_func ( const irep_idt & f,
const std::string & tgt_name ) const

◆ k_path_coverage()

void goto_coveraget::k_path_coverage ( )

◆ negating_asserts()

void goto_coveraget::negating_asserts ( const std::string & tgt_fname)

◆ replace_all_asserts_to_assume()

void goto_coveraget::replace_all_asserts_to_assume ( )

◆ replace_all_asserts_to_guard()

void goto_coveraget::replace_all_asserts_to_guard ( const expr2tc & guard,
bool is_instrumentation = false )

◆ replace_assert_to_assume()

void goto_coveraget::replace_assert_to_assume ( goto_programt::instructiont::targett & it)

◆ replace_assert_to_guard()

void goto_coveraget::replace_assert_to_guard ( const expr2tc & guard,
goto_programt::instructiont::targett & it,
bool is_instrumentation )

◆ set_target()

void goto_coveraget::set_target ( const std::string & _tgt)

Member Data Documentation

◆ all_claims

std::set< std::pair< std::string, std::string > > goto_coveraget::all_claims
static

◆ claim_negation

std::map< std::pair< std::string, std::string >, std::string > goto_coveraget::claim_negation
static

◆ cov_assume_asserts

bool goto_coveraget::cov_assume_asserts = false

◆ filename

std::string goto_coveraget::filename
protected

◆ goto_functions

goto_functionst& goto_coveraget::goto_functions
protected

◆ k_path_max_goals

size_t goto_coveraget::k_path_max_goals = 10000

◆ k_path_n

size_t goto_coveraget::k_path_n = 4

◆ k_path_spanning_redundant

std::set< std::pair< std::string, std::string > > goto_coveraget::k_path_spanning_redundant
static

◆ k_path_witness_depth

size_t goto_coveraget::k_path_witness_depth = 8

◆ ns

namespacet goto_coveraget::ns
protected

◆ target_function

std::string goto_coveraget::target_function = ""

◆ target_num

int goto_coveraget::target_num
protected

◆ total_assert

size_t goto_coveraget::total_assert = 0
static

◆ total_assert_ins

size_t goto_coveraget::total_assert_ins = 0
static

◆ total_branch

size_t goto_coveraget::total_branch = 0
static

◆ total_cond

std::set< std::pair< std::string, std::string > > goto_coveraget::total_cond
static

◆ total_func_branch

size_t goto_coveraget::total_func_branch = 0
static

◆ total_kpath

size_t goto_coveraget::total_kpath = 0
static

◆ total_kpath_spanning

size_t goto_coveraget::total_kpath_spanning = 0
static
The documentation for this class was generated from the following files: