#include <bmc.h>

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

Public Types
enum	ltl_res { ltl_res_good , ltl_res_succeeding , ltl_res_failing , ltl_res_bad }

Public Member Functions
	bmct (goto_functionst &funcs, optionst &opts, contextt &_context)
virtual smt_resultt	start_bmc ()
virtual smt_resultt	run (std::shared_ptr< symex_target_equationt > &eq)
virtual	~bmct ()
bool	violates_only_the_abstraction () const
	Whether every violation found refutes only the –loop-invariant-check abstraction, so the run neither refutes nor proves the program (#7480).

Public Attributes
optionst &	options
std::vector< dead_store_advisoryt >	dead_store_advisories
bool	dead_store_sarif_written = false
size_t	ltl_results_seen [4]
std::atomic< bool >	ltl_uninstrumented {false}
BigInt	interleaving_number
BigInt	interleaving_failed
bool	cs_bound_pruned = false
	Mirrors reachability_treet::cs_bound_pruned; valid after start_bmc().

Static Public Attributes
static constexpr int	ltl_res_uninstrumented = -3

Protected Types
enum class	enumeration_stop_reasont { Unsat , CapHit , NoInputs , Error , Disabled }
	Reason why witness enumeration stopped, used in the report footer. More...

Protected Member Functions
virtual smt_resultt	run_decision_procedure (smt_convt &smt_conv, symex_target_equationt &eq) const
smt_resultt	check_vacuity (symex_target_equationt &local_eq) const
smt_resultt	check_claim_unsatisfiable (symex_target_equationt &local_eq) const
	Whether the kept claim can hold at all on a feasible path.
bool	invariant_refutes (const symex_target_equationt &eq, size_t claim_index)
	Whether the invariant leaves one claim no way to hold (issue #7585).
virtual void	show_program (const symex_target_equationt &eq)
virtual void	report_success ()
virtual void	report_failure ()
void	report_violation ()
	Emit the verdict for a satisfiable run: FAILED, or UNKNOWN when every violated claim was abstraction-derived (issue #7480).
virtual void	report_unknown ()
virtual void	keep_alive_function () const
virtual void	error_trace (smt_convt &smt_conv, const symex_target_equationt &eq)
virtual void	successful_trace (const symex_target_equationt &eq)
virtual void	show_vcc (const symex_target_equationt &eq)
virtual void	show_vcc (std::ostream &out, const symex_target_equationt &eq)
virtual void	report_trace (smt_resultt &res, const symex_target_equationt &eq)
virtual void	report_result (smt_resultt &res)
virtual void	bidirectional_search (smt_convt &smt_conv, const symex_target_equationt &eq)
smt_resultt	run_thread (std::shared_ptr< symex_target_equationt > &eq)
int	ltl_run_thread (symex_target_equationt &equation)
smt_resultt	multi_property_check (const symex_target_equationt &eq, size_t remaining_claims, smt_convt &runtime_solver, unsigned int truncated_loops)
void	generate_smt_from_equation (smt_convt &smt_conv, symex_target_equationt &eq) const
void	clear_verified_claims_in_ssa (symex_target_equationt &local_eq, const claim_slicer &claim, const bool &is_goto_cov)
void	clear_verified_claims_in_goto (const claim_slicer &claim, const bool &is_goto_cov)
virtual void	report_multi_property_trace (const smt_resultt &res, const std::vector< witness_recordt > &witnesses, enumeration_stop_reasont stop_reason, const std::string &msg, bool reachability_trace=false)
	Multi-witness textual reporter.
void	report_coverage_verbose (const claim_slicer &claim, const std::string &claim_sig, const bool &is_assert_cov, const bool &is_cond_cov, const bool &is_branch_cov, const bool &is_branch_func_cov, const bool &is_k_path_cov, const std::unordered_set< std::string > &reached_claims, const std::unordered_multiset< std::string > &reached_mul_claims)

Protected Attributes
const contextt &	context
namespacet	ns
const goto_functionst &	program
std::unique_ptr< smt_convt >	runtime_solver
std::unique_ptr< reachability_treet >	symex
pytest_generator	pytest_gen
ctest_generator	ctest_gen
std::atomic< bool >	keep_alive_running
std::atomic< int >	keep_alive_interval
std::atomic< bool >	vacuity_detected {false}
std::atomic< bool >	weak_invariant_detected {false}
bool	verdict_is_unknown = false
	Set when the run printed UNKNOWN over a satisfiable result, so start_bmc can return the exit code the verdict earns without misreporting what the solver answered.
std::vector< std::unique_ptr< ssa_step_algorithm > >	algorithms

Member Enumeration Documentation

◆ enumeration_stop_reasont

enum class bmct::enumeration_stop_reasont

strongprotected

Reason why witness enumeration stopped, used in the report footer.

Enumerator
Unsat
CapHit
NoInputs
Error
Disabled

◆ ltl_res

enum bmct::ltl_res

Enumerator
ltl_res_good
ltl_res_succeeding
ltl_res_failing
ltl_res_bad

Constructor & Destructor Documentation

◆ bmct()

bmct::bmct	(	goto_functionst &	funcs,
		optionst &	opts,
		contextt &	_context )

◆ ~bmct()

bmct::~bmct ( )

virtualdefault

Member Function Documentation

◆ bidirectional_search()

void bmct::bidirectional_search	(	smt_convt &	smt_conv,
		const symex_target_equationt &	eq )

protectedvirtual

◆ check_claim_unsatisfiable()

smt_resultt bmct::check_claim_unsatisfiable ( symex_target_equationt & local_eq ) const

protected

Whether the kept claim can hold at all on a feasible path.

UNSAT iff no feasible path satisfies the kept claim.

A violation found downstream of a loop-invariant havoc is then one the invariant itself forces, not an artefact of the abstraction (issue #7585).

◆ check_vacuity()

smt_resultt bmct::check_vacuity ( symex_target_equationt & local_eq ) const

protected

◆ clear_verified_claims_in_goto()

void bmct::clear_verified_claims_in_goto	(	const claim_slicer &	claim,
		const bool &	is_goto_cov )

protected

◆ clear_verified_claims_in_ssa()

void bmct::clear_verified_claims_in_ssa	(	symex_target_equationt &	local_eq,
		const claim_slicer &	claim,
		const bool &	is_goto_cov )

protected

◆ error_trace()

void bmct::error_trace	(	smt_convt &	smt_conv,
		const symex_target_equationt &	eq )

protectedvirtual

◆ generate_smt_from_equation()

void bmct::generate_smt_from_equation	(	smt_convt &	smt_conv,
		symex_target_equationt &	eq ) const

protected

◆ invariant_refutes()

bool bmct::invariant_refutes	(	const symex_target_equationt &	eq,
		size_t	claim_index )

protected

Whether the invariant leaves one claim no way to hold (issue #7585).

Whether the invariant leaves the claim at claim_index no way to hold.

The single-formula path has no per-claim equation, so slice one the way multi_property_check does and run the same probe.

◆ keep_alive_function()

void bmct::keep_alive_function ( ) const

protectedvirtual

◆ ltl_run_thread()

int bmct::ltl_run_thread ( symex_target_equationt & equation )

protected

◆ multi_property_check()

smt_resultt bmct::multi_property_check	(	const symex_target_equationt &	eq,
		size_t	remaining_claims,
		smt_convt &	runtime_solver,
		unsigned int	truncated_loops )

protected

Parameters

truncated_loops how many loops exploration cut off at the unwinding bound, carried in from the symex result rather than read back from live state, which –schedule has already invalidated (#6423).

◆ report_coverage_verbose()

void bmct::report_coverage_verbose	(	const claim_slicer &	claim,
		const std::string &	claim_sig,
		const bool &	is_assert_cov,
		const bool &	is_cond_cov,
		const bool &	is_branch_cov,
		const bool &	is_branch_func_cov,
		const bool &	is_k_path_cov,
		const std::unordered_set< std::string > &	reached_claims,
		const std::unordered_multiset< std::string > &	reached_mul_claims )

protected

◆ report_failure()

void bmct::report_failure ( )

protectedvirtual

◆ report_multi_property_trace()

void bmct::report_multi_property_trace	(	const smt_resultt &	res,
		const std::vector< witness_recordt > &	witnesses,
		enumeration_stop_reasont	stop_reason,
		const std::string &	msg,
		bool	reachability_trace = false )

protectedvirtual

Multi-witness textual reporter.

Machine-readable artifacts (cex, testcase, html, json, graphml, yaml) are emitted by the caller while each witness's solver model is still live; this function only handles the human-readable counterexample output.

Parameters

reachability_trace render as evidence that the location is reachable, not as a property violation (coverage runs; issue #6387).

◆ report_result()

void bmct::report_result ( smt_resultt & res )

protectedvirtual

◆ report_success()

void bmct::report_success ( )

protectedvirtual

◆ report_trace()

void bmct::report_trace	(	smt_resultt &	res,
		const symex_target_equationt &	eq )

protectedvirtual

◆ report_unknown()

void bmct::report_unknown ( )

protectedvirtual

◆ report_violation()

void bmct::report_violation ( )

protected

Emit the verdict for a satisfiable run: FAILED, or UNKNOWN when every violated claim was abstraction-derived (issue #7480).

◆ run()

smt_resultt bmct::run ( std::shared_ptr< symex_target_equationt > & eq )

virtual

◆ run_decision_procedure()

smt_resultt bmct::run_decision_procedure	(	smt_convt &	smt_conv,
		symex_target_equationt &	eq ) const

protectedvirtual

◆ run_thread()

smt_resultt bmct::run_thread ( std::shared_ptr< symex_target_equationt > & eq )

protected

◆ show_program()

void bmct::show_program ( const symex_target_equationt & eq )

protectedvirtual

◆ show_vcc() [1/2]

void bmct::show_vcc ( const symex_target_equationt & eq )

protectedvirtual

◆ show_vcc() [2/2]

void bmct::show_vcc	(	std::ostream &	out,
		const symex_target_equationt &	eq )

protectedvirtual

◆ start_bmc()

smt_resultt bmct::start_bmc ( )

virtual

◆ successful_trace()

void bmct::successful_trace ( const symex_target_equationt & eq )

protectedvirtual

◆ violates_only_the_abstraction()

bool bmct::violates_only_the_abstraction ( ) const

Whether every violation found refutes only the –loop-invariant-check abstraction, so the run neither refutes nor proves the program (#7480).

Member Data Documentation

◆ algorithms

std::vector<std::unique_ptr<ssa_step_algorithm> > bmct::algorithms

protected

◆ context

const contextt& bmct::context

protected

◆ cs_bound_pruned

bool bmct::cs_bound_pruned = false

Mirrors reachability_treet::cs_bound_pruned; valid after start_bmc().

◆ ctest_gen

ctest_generator bmct::ctest_gen

protected

◆ dead_store_advisories

std::vector<dead_store_advisoryt> bmct::dead_store_advisories

◆ dead_store_sarif_written

bool bmct::dead_store_sarif_written = false

◆ interleaving_failed

BigInt bmct::interleaving_failed

◆ interleaving_number

BigInt bmct::interleaving_number

◆ keep_alive_interval

std::atomic<int> bmct::keep_alive_interval

mutableprotected

◆ keep_alive_running

std::atomic<bool> bmct::keep_alive_running

mutableprotected

◆ ltl_res_uninstrumented

int bmct::ltl_res_uninstrumented = -3

staticconstexpr

◆ ltl_results_seen

size_t bmct::ltl_results_seen[4]

◆ ltl_uninstrumented

std::atomic<bool> bmct::ltl_uninstrumented {false}

◆ ns

namespacet bmct::ns

protected

◆ options

optionst& bmct::options

◆ program

const goto_functionst& bmct::program

protected

◆ pytest_gen

pytest_generator bmct::pytest_gen

protected

◆ runtime_solver

std::unique_ptr<smt_convt> bmct::runtime_solver

protected

◆ symex

std::unique_ptr<reachability_treet> bmct::symex

protected

◆ vacuity_detected

std::atomic<bool> bmct::vacuity_detected {false}

protected

◆ verdict_is_unknown

bool bmct::verdict_is_unknown = false

protected

Set when the run printed UNKNOWN over a satisfiable result, so start_bmc can return the exit code the verdict earns without misreporting what the solver answered.

◆ weak_invariant_detected

std::atomic<bool> bmct::weak_invariant_detected {false}

protected

The documentation for this class was generated from the following files:

src/esbmc/bmc.h
src/esbmc/bmc.cpp
src/esbmc/show_vcc.cpp

Classes

Public Types

Public Member Functions

Public Attributes

Static Public Attributes

Protected Types

Protected Member Functions

Protected Attributes

Member Enumeration Documentation

◆ enumeration_stop_reasont

◆ ltl_res

Constructor & Destructor Documentation

◆ bmct()

◆ ~bmct()

Member Function Documentation

◆ bidirectional_search()

◆ check_claim_unsatisfiable()

◆ check_vacuity()

◆ clear_verified_claims_in_goto()

◆ clear_verified_claims_in_ssa()

◆ error_trace()

◆ generate_smt_from_equation()

◆ invariant_refutes()

◆ keep_alive_function()

◆ ltl_run_thread()

◆ multi_property_check()

◆ report_coverage_verbose()

◆ report_failure()

◆ report_multi_property_trace()

◆ report_result()

◆ report_success()

◆ report_trace()

◆ report_unknown()

◆ report_violation()

◆ run()

◆ run_decision_procedure()

◆ run_thread()

◆ show_program()

◆ show_vcc() [1/2]

◆ show_vcc() [2/2]

◆ start_bmc()

◆ successful_trace()

◆ violates_only_the_abstraction()

Member Data Documentation

◆ algorithms

◆ context

◆ cs_bound_pruned

◆ ctest_gen

◆ dead_store_advisories

◆ dead_store_sarif_written

◆ interleaving_failed

◆ interleaving_number

◆ keep_alive_interval

◆ keep_alive_running

◆ ltl_res_uninstrumented

◆ ltl_results_seen

◆ ltl_uninstrumented

◆ ns

◆ options

◆ program

◆ pytest_gen

◆ runtime_solver

◆ symex

◆ vacuity_detected

◆ verdict_is_unknown

◆ weak_invariant_detected