bmc.h File Reference

#include <goto-programs/dead_store_advisory.h>
#include <goto-programs/goto_coverage.h>
#include <goto-programs/property_verdict.h>
#include <goto-symex/equation/slice.h>
#include <goto-symex/scheduler/reachability_tree.h>
#include <goto-symex/equation/symex_target_equation.h>
#include <goto-symex/witness/witnesses.h>
#include <goto-symex/testgen/pytest.h>
#include <goto-symex/testgen/ctest.h>
#include <langapi/language_ui.h>
#include <list>
#include <map>
#include <set>
#include <solvers/smt/smt_result.h>
#include <solvers/solve.h>
#include <util/config/options.h>
#include <goto-symex/equation/ssa_step_algorithm.h>
#include <util/config/cmdline.h>
#include <atomic>

Include dependency graph for bmc.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	bmct
struct	bmct::witness_recordt
	One enumerated witness for a failing property. More...

Functions
void	report_k_step_property_table (const optionst &options, const goto_functionst &goto_functions, const namespacet &ns)
	Print the property table a k-step strategy accumulated across its phases, once, where the strategy concludes without a phase of its own having reported (the k steps ran out).
void	report_coverage (const optionst &options, std::unordered_set< std::string > &reached_claims, const std::unordered_multiset< std::string > &reached_mul_claims, pytest_generator &pytest_gen, ctest_generator &ctest_gen)
void	note_cov_incomplete (const std::string &reason)
	Record why a coverage measurement is not exhaustive; the reason is listed under the closing COVERAGE ANALYSIS INCOMPLETE line.
void	report_coverage_completeness ()
	Closing line of a coverage run: whether every goal was actually decided, and if not, why.

Function Documentation

note_cov_incomplete()

void note_cov_incomplete

(

const std::string &

reason

)

Record why a coverage measurement is not exhaustive; the reason is listed under the closing COVERAGE ANALYSIS INCOMPLETE line.

report_coverage()

void report_coverage	(	const optionst &	options,
		std::unordered_set< std::string > &	reached_claims,
		const std::unordered_multiset< std::string > &	reached_mul_claims,
		pytest_generator &	pytest_gen,
		ctest_generator &	ctest_gen )

the reached_claims might not be empty (due to unwinding assertions)

Might got incorrect total number when using –k-induction due to that the symex->goto_functions has been simplified

report_coverage_completeness()

void report_coverage_completeness

(

)

Closing line of a coverage run: whether every goal was actually decided, and if not, why.

Printed by the driver once, after the last [Coverage] block (k-induction prints one per phase).

report_k_step_property_table()

void report_k_step_property_table	(	const optionst &	options,
		const goto_functionst &	goto_functions,
		const namespacet &	ns )

Print the property table a k-step strategy accumulated across its phases, once, where the strategy concludes without a phase of its own having reported (the k steps ran out).

Rows the run never decided print as UNKNOWN: every base case checked them, none settled them. A no-op on a run that keeps a table per phase.