bmct Member List

This is the complete list of members for bmct, including all inherited members.

algorithms	bmct	protected
bidirectional_search(smt_convt &smt_conv, const symex_target_equationt &eq)	bmct	protectedvirtual
bmct(goto_functionst &funcs, optionst &opts, contextt &_context)	bmct
check_claim_unsatisfiable(symex_target_equationt &local_eq) const	bmct	protected
check_vacuity(symex_target_equationt &local_eq) const	bmct	protected
clear_verified_claims_in_goto(const claim_slicer &claim, const bool &is_goto_cov)	bmct	protected
clear_verified_claims_in_ssa(symex_target_equationt &local_eq, const claim_slicer &claim, const bool &is_goto_cov)	bmct	protected
context	bmct	protected
cs_bound_pruned	bmct
ctest_gen	bmct	protected
dead_store_advisories	bmct
dead_store_sarif_written	bmct
enumeration_stop_reasont enum name	bmct	protected
error_trace(smt_convt &smt_conv, const symex_target_equationt &eq)	bmct	protectedvirtual
generate_smt_from_equation(smt_convt &smt_conv, symex_target_equationt &eq) const	bmct	protected
interleaving_failed	bmct
interleaving_number	bmct
invariant_refutes(const symex_target_equationt &eq, size_t claim_index)	bmct	protected
keep_alive_function() const	bmct	protectedvirtual
keep_alive_interval	bmct	mutableprotected
keep_alive_running	bmct	mutableprotected
ltl_res enum name	bmct
ltl_res_bad enum value	bmct
ltl_res_failing enum value	bmct
ltl_res_good enum value	bmct
ltl_res_succeeding enum value	bmct
ltl_res_uninstrumented	bmct	static
ltl_results_seen	bmct
ltl_run_thread(symex_target_equationt &equation)	bmct	protected
ltl_uninstrumented	bmct
multi_property_check(const symex_target_equationt &eq, size_t remaining_claims, smt_convt &runtime_solver, unsigned int truncated_loops)	bmct	protected
ns	bmct	protected
options	bmct
program	bmct	protected
pytest_gen	bmct	protected
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)	bmct	protected
report_failure()	bmct	protectedvirtual
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)	bmct	protectedvirtual
report_result(smt_resultt &res)	bmct	protectedvirtual
report_success()	bmct	protectedvirtual
report_trace(smt_resultt &res, const symex_target_equationt &eq)	bmct	protectedvirtual
report_unknown()	bmct	protectedvirtual
report_violation()	bmct	protected
run(std::shared_ptr< symex_target_equationt > &eq)	bmct	virtual
run_decision_procedure(smt_convt &smt_conv, symex_target_equationt &eq) const	bmct	protectedvirtual
run_thread(std::shared_ptr< symex_target_equationt > &eq)	bmct	protected
runtime_solver	bmct	protected
show_program(const symex_target_equationt &eq)	bmct	protectedvirtual
show_vcc(const symex_target_equationt &eq)	bmct	protectedvirtual
show_vcc(std::ostream &out, const symex_target_equationt &eq)	bmct	protectedvirtual
start_bmc()	bmct	virtual
successful_trace(const symex_target_equationt &eq)	bmct	protectedvirtual
symex	bmct	protected
vacuity_detected	bmct	protected
verdict_is_unknown	bmct	protected
violates_only_the_abstraction() const	bmct
weak_invariant_detected	bmct	protected
~bmct()	bmct	virtual