- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <csignal>#include <memory>#include <sys/types.h>#include <algorithm>#include <cctype>#include <cstdlib>#include <mutex>#include <thread>#include <chrono>#include <unistd.h>#include <sched.h>#include <filesystem>#include <fmt/format.h>#include <regex>#include <ac_config.h>#include <esbmc/bmc.h>#include <esbmc/property_report.h>#include <fstream>#include <goto-programs/goto_loops.h>#include <goto-symex/trace/build_goto_trace.h>#include <goto-symex/symex_invariant.h>#include <goto-symex/trace/goto_trace.h>#include <goto-symex/equation/features.h>#include <goto-symex/trace/sarif.h>#include <goto-symex/equation/symex_symmetry.h>#include <goto-symex/trace/xml_goto_trace.h>#include <langapi/language_util.h>#include <langapi/languages.h>#include <langapi/mode.h>#include <solvers/smt/smt_conv.h>#include <sstream>#include <util/base/i2string.h>#include <irep2/irep2.h>#include <util/irep/location.h>#include <util/irep/migrate.h>#include <util/base/cwe_mapping.h>#include <util/symtab/show_symbol_table.h>#include <util/base/time_stopping.h>#include <util/ssa/cache.h>#include <util/ssa/fingerprint.h>#include <util/ssa/proof_cache.h>#include <esbmc/globals.h>#include <atomic>#include <vector>#include <nlohmann/json.hpp>Functions | |
| static std::string | ctest_output_dir (const optionst &options) |
| static std::string | pytest_output_dir (const optionst &options) |
| 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. | |
| static void | note_cov_suppressed_violation (const std::string &claim) |
| static void | note_undecided_cov_goal (const std::string &reason) |
| static bool | strategy_owns_property_table (const optionst &options) |
| Whether the k-step strategy driver owns the run's property table: it clears the store before its first phase, every phase records into it, and it is printed once where the run concludes (W3b of docs/roadmap/multi-property-strategy-plan.md). | |
| static bool | reports_multi_property_verdict (const optionst &options) |
| Whether this phase may report a –multi-property result of its own. | |
| static void | record_discharge (bool withhold_proofs, const std::string &property, property_verdictt verdict, const property_locationt &loc, const std::string ¬e="") |
Record what a solver's UNSAT earned property. | |
| static void | print_partial_report_note () |
| The closing line of a report that does not account for every property. | |
| static bool | run_fully_proved (const optionst &options) |
| Whether the table a k-step run accumulated says the program holds. | |
| static bool | phase_left_properties_undecided (bool report_incomplete, smt_resultt res) |
| Whether a phase left properties undecided that a later one must not take for proved: it skipped some claim, died before its per-claim loop, or only emitted a formula. | |
| static bool | is_bounded_round (const optionst &options) |
| Whether this phase is a k-step strategy's base case, which opens and completes a round and discharges a claim only within the current k (withholds_proofs()). | |
| static bool | is_loop_invariant_obligation (const locationt &location) |
| static bool | is_vacuity_probe_candidate (const std::string &claim_property) |
| static std::string | prettify_solidity_expr (const std::string &expr) |
| static nlohmann::json | parse_claim_location (const std::string &loc) |
| static bool | is_kpath_maximal (const std::string &claim_sig) |
| static void | report_dead_code (const optionst &options, const std::unordered_set< std::string > &reached_claims, const std::vector< dead_store_advisoryt > &dead_stores) |
| static size_t | count_reached_goals (const std::unordered_set< std::string > &reached_claims) |
| Coverage numerator over the branch instrumentation. | |
| 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 | report_coverage_completeness () |
| Closing line of a coverage run: whether every goal was actually decided, and if not, why. | |
| static void | prepare_property_verdicts (const optionst &options) |
| A k-step strategy clears the store once, before its first phase, and starts a round at each base case. | |
| static bool | proof_cache_hit (proof_cachet *cache, bool verify, const symex_target_equationt::SSA_stepst &steps, std::string &cone_key, bool &hit) |
| Look the claim's cone up in the cache. | |
| static void | proof_cache_store (proof_cachet *cache, const std::string &cone_key, bool hit, smt_resultt solver_result, bool is_vacuous, const std::string &claim, smt_resultt &final_result, std::mutex &result_mutex) |
| Store a fresh proof, or fail the run over a stored one the solver has just refuted. | |
| static bool | coverage_silences_claim (bool goto_cov, bool dead_code, const std::string &prop) |
| A dead-code probe is advisory and a non-probe claim in a coverage run is not being reported, so neither prints a per-claim solve (issue #4495). | |
| static bool | is_coverage_goal (bool cov_run, const std::string &prop) |
| A coverage probe: SAT means "this location is reachable". | |
| static const std::string & | proof_cache_identity () |
| Which ESBMC this is. | |
| static std::unique_ptr< proof_cachet > | make_proof_cache (const optionst &options, const std::string &dir, const BigInt &interleaving_number) |
| Build the cache only where a stored proof would be sound; nullptr disables every cache interaction downstream. | |
| static void | log_proof_cache_summary (const proof_cachet *cache) |
| A warm run solves nothing, so without this the report shows no solver activity at all and gives no sign of where the verdicts came from. | |
| static void | dump_claim_fingerprint (const std::string &path, const symex_target_equationt::SSA_stepst &cone, smt_resultt result, const std::string &loc, const std::string &msg) |
| One line per solved claim, digesting its cone under each normalisation: the instrument for measuring what –proof-cache can reuse. | |
| static void | print_property_rows (const std::vector< property_rowt > &rows, const property_countst &counts, bool is_color) |
| static void | print_property_summary (size_t total, const property_countst &counts, bool is_color) |
| static property_countst | print_property_table (const std::map< std::string, property_resultt > &verdicts, const std::set< std::string > &library_files, bool is_color, bool unchecked_is_unknown, bool decided_only, const std::function< std::string(const expr2tc &)> &render_condition) |
| Build, order and print one 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). | |
Variables | |
| static std::atomic< size_t > | undecided_cov_goals {0} |
| static std::set< std::string > | cov_incomplete_reasons |
| static std::set< std::string > | cov_suppressed_violations |
| static std::mutex | cov_report_mutex |
| static std::atomic< bool > | cov_block_reported {false} |
| static const char *const | weak_invariant_note |
|
static |
Coverage numerator over the branch instrumentation.
reached_claims records every claim symex refuted, including ones outside the instrumentation (an uncaught exception, say), so its raw size can exceed the goal count and report over 100% (#7296). all_claims is the instrumented set.
A dead-code probe is advisory and a non-probe claim in a coverage run is not being reported, so neither prints a per-claim solve (issue #4495).
|
static |
|
static |
One line per solved claim, digesting its cone under each normalisation: the instrument for measuring what –proof-cache can reuse.
No-op when –claim-fingerprint-dump was not given.
Whether this phase is a k-step strategy's base case, which opens and completes a round and discharges a claim only within the current k (withholds_proofs()).
A coverage probe: SAT means "this location is reachable".
It is not a property, so it must not be reported as one (issue #6387).
|
static |
|
static |
|
static |
A warm run solves nothing, so without this the report shows no solver activity at all and gives no sign of where the verdicts came from.
|
static |
Build the cache only where a stored proof would be sound; nullptr disables every cache interaction downstream.
A cached proof is only sound where the claim's sliced cone is everything its verdict depends on. The k-induction phases and –incremental-bmc qualify: each sets its phase flags and unwind on this optionst before running, so both are already part of a claim's key.
| 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.
|
static |
|
static |
|
static |
|
static |
Whether a phase left properties undecided that a later one must not take for proved: it skipped some claim, died before its per-claim loop, or only emitted a formula.
|
static |
A k-step strategy clears the store once, before its first phase, and starts a round at each base case.
|
static |
|
static |
The closing line of a report that does not account for every property.
|
static |
|
static |
|
static |
Build, order and print one property table.
unchecked_is_unknown renames the rows a k-step run never decided: the run did check them, at every k it reached, so "not checked" would understate what was tried.
|
static |
Look the claim's cone up in the cache.
Returns true when the stored proof stands in for solving; cone_key and hit are set for the store step.
|
static |
Which ESBMC this is.
Hashing the executable is the fallback when the build ID does not name one build, so it is computed once and held.
|
static |
Store a fresh proof, or fail the run over a stored one the solver has just refuted.
hit can only be set here under –proof-cache-verify: a hit short-circuits the solve otherwise.
|
static |
|
static |
Record what a solver's UNSAT earned property.
Only a proof needs backing: where withholds_proofs() says the phase cannot make one, the claim stays undecided. A vacuous discharge is not a proof but a diagnosis of the path, which a bounded round establishes as well as a conclusive one, so it is recorded either way – and it has to be, since a k-step run reports the vacuity nowhere else.
| 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
| 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).
|
static |
| 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.
Whether this phase may report a –multi-property result of its own.
Under a k-step strategy it may not: its phases deepen the search rather than conclude it, and the strategy reports for all of them.
Whether the table a k-step run accumulated says the program holds.
The run's verdict follows its table, so a row left undecided – never settled within max-k, or discharged only vacuously – is not a proof, and the phase that closes the search must not call it one. Vacuously true elsewhere: a single run's phase speaks for itself.
Whether the k-step strategy driver owns the run's property table: it clears the store before its first phase, every phase records into it, and it is printed once where the run concludes (W3b of docs/roadmap/multi-property-strategy-plan.md).
|
static |
|
static |
|
static |
|
static |
|
static |
1.15.0