driver.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 <irep2/simplification_check.h>
#include <solvers/smt/simplification_equivalence.h>
#include <algorithm>
#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/goto_check_excessive_alloc.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 <util/ssa/proof_cache.h>
#include <sys/wait.h>

Macros
#define	CLR_BOLD_CYAN   "\033[1;36m"
#define	CLR_BOLD   "\033[1m"
#define	CLR_RESET   "\033[0m"

Functions
static bool	k_induction_parallel_conflicts (const cmdlinet &cmdline)
	The forked k-induction processes each keep their own property table, and the one that concludes the run reports its base-case bound as PASSED (D4 of docs/roadmap/multi-property-strategy-plan.md).
static bool	incompatible_flags (const cmdlinet &cmdline)
	The flag combinations that cannot produce a sound report, rejected before any work is done.
static bool	proof_cache_flags_usable (const optionst &options)
	The proof cache is wired into the per-claim solve alone, and both its flags are inert without it.
static std::string	colorize_flag_refs (const std::string &text)

Macro Definition Documentation

CLR_BOLD

#define CLR_BOLD   "\033[1m"

CLR_BOLD_CYAN

#define CLR_BOLD_CYAN   "\033[1;36m"

CLR_RESET

#define CLR_RESET   "\033[0m"

Function Documentation

colorize_flag_refs()

std::string colorize_flag_refs ( const std::string & text )

static

incompatible_flags()

bool incompatible_flags ( const cmdlinet & cmdline )

static

The flag combinations that cannot produce a sound report, rejected before any work is done.

Kept out of doit() so every combination check reads in one place.

k_induction_parallel_conflicts()

bool k_induction_parallel_conflicts ( const cmdlinet & cmdline )

static

The forked k-induction processes each keep their own property table, and the one that concludes the run reports its base-case bound as PASSED (D4 of docs/roadmap/multi-property-strategy-plan.md).

The other flags listed turn –multi-property on. –termination runs the sequential driver instead.

proof_cache_flags_usable()

bool proof_cache_flags_usable ( const optionst & options )

static

The proof cache is wired into the per-claim solve alone, and both its flags are inert without it.

Refused rather than accepted, because a run that reuses nothing is indistinguishable from one whose cache is working. The flags are judged on their own terms, so –skip-bmc and the print-and-stop modes are refused too rather than accepting a combination that could never have worked. Called after the GOTO program is built because only by then is the option set final: –multi-property is implied by several flags, the coverage ones not until process_goto_program.