bmc_strategy.cpp File Reference

#include <ac_config.h>
#include <fcntl.h>
#include <unistd.h>
#include <sys/resource.h>
#include <sys/time.h>
#include <sys/types.h>
#include <esbmc/bmc.h>
#include <esbmc/esbmc_parseoptions.h>
#include <goto-symex/engine/goto_symex.h>
#include <goto-symex/trace/goto_trace.h>
#include <goto-symex/trace/sarif.h>
#include <util/base/cwe_mapping.h>
#include <solvers/smt/smt_result.h>
#include <solvers/smtlib/smtlib_conv.h>
#include <solvers/solve.h>
#include <cctype>
#include <charconv>
#include <clang-c-frontend/clang_c_language.h>
#include <util/config/config.h>
#include <util/base/filesystem.h>
#include <csignal>
#include <cstdlib>
#include <limits>
#include <util/expr/expr_util.h>
#include <iostream>
#include <fstream>
#include <goto-programs/add_race_assertions.h>
#include <goto-programs/add_restrict_assertions.h>
#include <goto-programs/goto_atomicity_check.h>
#include <goto-programs/goto_check.h>
#include <goto-programs/goto_convert_functions.h>
#include <goto-programs/goto_inline.h>
#include <goto-programs/goto_k_induction.h>
#include <goto-programs/goto_termination.h>
#include <esbmc/ranking_synthesis.h>
#include <esbmc/non_termination.h>
#include <goto-programs/goto_loop_simplify.h>
#include <goto-programs/goto_loop_invariant.h>
#include <goto-programs/abstract-interpretation/interval_analysis.h>
#include <goto-programs/abstract-interpretation/gcse.h>
#include <goto-programs/loop_numbers.h>
#include <goto-programs/goto_binary_reader.h>
#include <goto-programs/read_cbmc_goto_object.h>
#include <goto-programs/write_goto_binary.h>
#include <goto-programs/remove_no_op.h>
#include <goto-programs/remove_unreachable.h>
#include <goto-programs/remove_exceptions.h>
#include <goto-programs/set_claims.h>
#include <goto-programs/show_claims.h>
#include <goto-programs/loop_unroll.h>
#include <goto-programs/goto_check_uninit_vars.h>
#include <goto-programs/goto_check_unchecked_return.h>
#include <goto-programs/dead_store_analysis.h>
#include <goto-programs/mark_decl_as_non_det.h>
#include <goto-programs/assign_params_as_non_det.h>
#include <goto2c/goto2c.h>
#include <util/irep/irep.h>
#include <langapi/languages.h>
#include <langapi/mode.h>
#include <memory>
#include <pointer-analysis/goto_program_dereference.h>
#include <pointer-analysis/show_value_sets.h>
#include <pointer-analysis/value_set_analysis.h>
#include <util/symtab/symbol.h>
#include <util/base/time_stopping.h>
#include <goto-programs/goto_cfg.h>
#include <langapi/language_util.h>
#include <goto-programs/contracts/contracts.h>
#include <sys/wait.h>

Functions
static void	report_non_termination_cwe (optionst &options, const namespacet &ns, const goto_functionst &goto_functions, const std::string &comment)
static void	adopt_one_property_table (optionst &options, bool is_coverage)
	Give this run one property table for all its k steps, where it should have one: the strategy then owns the verdict store, each phase records into it, and the table is printed once where the run concludes (W3b of docs/roadmap/multi-property-strategy-plan.md).
static bool	ends_at_violation (optionst &options, bool &any_violation_found)
	Records a base case's violation.
static bool	may_follow_base_case (const optionst &options, const tvt &base_case)
	Whether the forward condition and inductive step may follow the base case: a proof needs the base case refuted, not merely left unviolated.

Function Documentation

adopt_one_property_table()

void adopt_one_property_table ( optionst & options, bool is_coverage )

static

Give this run one property table for all its k steps, where it should have one: the strategy then owns the verdict store, each phase records into it, and the table is printed once where the run concludes (W3b of docs/roadmap/multi-property-strategy-plan.md).

A coverage run reports reachability rather than properties and resets per pass by design; –termination asks about the loops, not the assertions; and a run that only emits a formula decides nothing to put in a table; so none of them join in.

ends_at_violation()

bool ends_at_violation ( optionst & options, bool & any_violation_found )

static

Records a base case's violation.

The run ends there unless –multi-property keeps it looking for the claims violated at a larger k.

may_follow_base_case()

bool may_follow_base_case ( const optionst & options, const tvt & base_case )

static

Whether the forward condition and inductive step may follow the base case: a proof needs the base case refuted, not merely left unviolated.

A formula-only run decides no phase, so each still emits its formula.

report_non_termination_cwe()

void report_non_termination_cwe ( optionst & options, const namespacet & ns, const goto_functionst & goto_functions, const std::string & comment )

static