command_line_options.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 <esbmc/globals.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 <util/base/signal_catcher.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>

Macros
#define	BT_BUF_SIZE   256

Functions
void	timeout_handler (int)
static void	segfault_handler (int sig)
static void	install_verbose_crash_handler (const cmdlinet &cmdline)
static std::string	format_target ()
static void	set_loop_invariant_options (const cmdlinet &cmdline, optionst &options)
	Option defaults the loop-invariant modes imply.

Macro Definition Documentation

BT_BUF_SIZE

#define BT_BUF_SIZE   256

Function Documentation

format_target()

std::string format_target ( )

static

install_verbose_crash_handler()

void install_verbose_crash_handler ( const cmdlinet & cmdline )

static

segfault_handler()

void segfault_handler ( int sig )

static

set_loop_invariant_options()

void set_loop_invariant_options ( const cmdlinet & cmdline, optionst & options )

static

Option defaults the loop-invariant modes imply.

–synthesise-loop-invariants: the schema emits establishment, preservation and the post-loop use as three independent obligations. Bundling them into one query makes the solver carry every multiplier term at once – on regression/esbmc/synth_loop_invariant_sum each discharges in about a second alone while the bundle does not finish in 120s – so solve them separately. base-case is set alongside multi-property because multi_property_check only runs when both are on.

Vacuity: default-enable the probe under –loop-invariant-check (the standalone Hoare-rewrite mode). A loop invariant that implies the guard makes the post-loop continuation unreachable; without this probe every downstream claim discharges as vacuously true. Deliberately NOT default-enabled for combined mode –loop-invariant: that runs k-induction phases whose UNSAT-on-internal-claims is the success signal, not vacuity. Users can opt in explicitly with –check-vacuity there.

timeout_handler()

void timeout_handler

(

int

)