#include <esbmc_parseoptions.h>

Inheritance diagram for esbmc_parseoptionst:

Public Member Functions
int	doit () override
void	help () override
const char *	fatal_signal_advice () const override
	One line naming what this driver offers for a fuller crash report, or null.
	esbmc_parseoptionst (int argc, const char **argv)
	~esbmc_parseoptionst ()
Public Member Functions inherited from parseoptions_baset
	parseoptions_baset (const struct group_opt_templ opts, int argc, const char *argv)
virtual int	main ()
virtual	~parseoptions_baset ()=default
void	set_verbosity_msg (VerbosityLevel def=VerbosityLevel::Status)
Public Member Functions inherited from language_uit
	language_uit ()
virtual	~language_uit () noexcept=default
virtual bool	parse (const cmdlinet &cmdline)
virtual bool	parse (const std::string &filename)
virtual bool	typecheck ()
virtual bool	final ()
virtual void	clear_parse ()
virtual void	show_symbol_table ()
virtual void	show_symbol_table_plain (std::ostream &out)
virtual void	show_symbol_table_xml_ui ()

Public Attributes
goto_functionst	goto_functions
Public Attributes inherited from parseoptions_baset
cmdlinet	cmdline
Public Attributes inherited from language_uit
langmapt	langmap
contextt	context
namespacet	ns

Protected Member Functions
virtual void	get_command_line_options (optionst &options)
virtual int	do_bmc (bmct &bmc)
virtual bool	get_goto_program (optionst &options, goto_functionst &goto_functions)
virtual bool	create_goto_program (optionst &options, goto_functionst &goto_functions)
virtual bool	parse_goto_program (optionst &options, goto_functionst &goto_functions)
virtual bool	process_goto_program (optionst &options, goto_functionst &goto_functions)
bool	wants_loop_invariants () const
	Whether the run needs the loop-invariant machinery.
void	apply_loop_invariants (goto_functionst &goto_functions, contextt &context, const optionst &options, bool k_induction_ran)
	Synthesise the invariants when asked, then run the schema over them.
virtual bool	output_goto_program (optionst &options, goto_functionst &goto_functions)
bool	process_function_contracts (goto_functionst &goto_functions, bool has_replace, bool has_enforce, bool has_enforce_all, bool has_replace_all)
	Process function contracts if enabled.
int	do_bmc_strategy (optionst &options, goto_functionst &goto_functions)
int	do_ts_strategy (optionst &options, goto_functionst &goto_functions)
bool	ts_strategy_requested () const
int	do_context_bound_deepening (optionst &options, goto_functionst &goto_functions)
int	falsify_with_bounded_schedules (optionst &options, goto_functionst &goto_functions)
int	run_chosen_strategy (optionst &options, goto_functionst &goto_functions)
int	doit_k_induction_parallel ()
tvt	is_base_case_violated (optionst &options, goto_functionst &goto_functions, const uint64_t &k_step)
tvt	does_forward_condition_hold (optionst &options, goto_functionst &goto_functions, const uint64_t &k_step)
tvt	is_inductive_step_violated (optionst &options, goto_functionst &goto_functions, const uint64_t &k_step)
void	diagnose_unknown_properties (optionst &options, goto_functionst &goto_functions, uint64_t k_step)
bool	read_goto_binary (goto_functionst &goto_functions)
bool	has_cbmc_binary_input ()
	True if any –binary input is a CBMC goto-binary (magic 0x7f 'G' 'B' 'F').
bool	synthesize_cprover_additions (optionst &options, goto_functionst &goto_functions)
	Synthesises ESBMC's "additions" (the __ESBMC_main entry wrapper and the CPROVER-intrinsic bodies) by compiling a boilerplate translation unit through the C frontend into the given symbol table / goto functions, so a CBMC goto-binary verifies without manually linking a library.goto.
bool	set_claims (goto_functionst &goto_functions)
uint64_t	read_time_spec (std::string_view str)
uint64_t	read_mem_spec (std::string_view str)
void	preprocessing ()
void	add_property_monitors (goto_functionst &goto_functions, namespacet &ns)
expr2tc	calculate_a_property_monitor (const std::string &prefix, std::set< std::string > &used_syms) const
void	add_monitor_exprs (goto_programt::targett insn, goto_programt::instructionst &insn_list, const std::map< std::string, std::pair< std::set< std::string >, expr2tc > > &monitors)
void	print_ileave_points (namespacet &ns, goto_functionst &goto_functions)
Protected Member Functions inherited from language_uit
	language_uit (language_uit &&) noexcept
language_uit &	operator= (language_uit &&) noexcept

Protected Attributes
FILE *	out = stderr
std::vector< std::unique_ptr< goto_functions_algorithm > >	goto_preprocess_algorithms
std::vector< dead_store_advisoryt >	dead_store_advisories
bool	is_coverage
Protected Attributes inherited from parseoptions_baset
boost::filesystem::path	executable_path

Additional Inherited Members
Public Types inherited from language_uit
typedef std::map< language_idt, std::unique_ptr< languaget > >	langmapt

Constructor & Destructor Documentation

◆ esbmc_parseoptionst()

esbmc_parseoptionst::esbmc_parseoptionst	(	int	argc,
		const char **	argv )

inline

◆ ~esbmc_parseoptionst()

esbmc_parseoptionst::~esbmc_parseoptionst ( )

inline

Member Function Documentation

◆ add_monitor_exprs()

void esbmc_parseoptionst::add_monitor_exprs	(	goto_programt::targett	insn,
		goto_programt::instructionst &	insn_list,
		const std::map< std::string, std::pair< std::set< std::string >, expr2tc > > &	monitors )

protected

◆ add_property_monitors()

void esbmc_parseoptionst::add_property_monitors	(	goto_functionst &	goto_functions,
		namespacet &	ns )

protected

◆ apply_loop_invariants()

void esbmc_parseoptionst::apply_loop_invariants	(	goto_functionst &	goto_functions,
		contextt &	context,
		const optionst &	options,
		bool	k_induction_ran )

protected

Synthesise the invariants when asked, then run the schema over them.

Synthesise the invariants when asked, then run the schema that discharges them.

◆ calculate_a_property_monitor()

expr2tc esbmc_parseoptionst::calculate_a_property_monitor	(	const std::string &	prefix,
		std::set< std::string > &	used_syms ) const

protected

◆ create_goto_program()

bool esbmc_parseoptionst::create_goto_program	(	optionst &	options,
		goto_functionst &	goto_functions )

protectedvirtual

◆ diagnose_unknown_properties()

void esbmc_parseoptionst::diagnose_unknown_properties	(	optionst &	options,
		goto_functionst &	goto_functions,
		uint64_t	k_step )

protected

◆ do_bmc()

int esbmc_parseoptionst::do_bmc ( bmct & bmc )

protectedvirtual

◆ do_bmc_strategy()

int esbmc_parseoptionst::do_bmc_strategy	(	optionst &	options,
		goto_functionst &	goto_functions )

protected

◆ do_context_bound_deepening()

int esbmc_parseoptionst::do_context_bound_deepening	(	optionst &	options,
		goto_functionst &	goto_functions )

protected

◆ do_ts_strategy()

int esbmc_parseoptionst::do_ts_strategy	(	optionst &	options,
		goto_functionst &	goto_functions )

protected

◆ does_forward_condition_hold()

tvt esbmc_parseoptionst::does_forward_condition_hold	(	optionst &	options,
		goto_functionst &	goto_functions,
		const uint64_t &	k_step )

protected

◆ doit()

int esbmc_parseoptionst::doit ( )

overridevirtual

Implements parseoptions_baset.

◆ doit_k_induction_parallel()

int esbmc_parseoptionst::doit_k_induction_parallel ( )

protected

◆ falsify_with_bounded_schedules()

int esbmc_parseoptionst::falsify_with_bounded_schedules	(	optionst &	options,
		goto_functionst &	goto_functions )

protected

◆ fatal_signal_advice()

const char * esbmc_parseoptionst::fatal_signal_advice ( ) const

inlineoverridevirtual

One line naming what this driver offers for a fuller crash report, or null.

Only the driver knows which options it accepts.

Reimplemented from parseoptions_baset.

◆ get_command_line_options()

void esbmc_parseoptionst::get_command_line_options ( optionst & options )

protectedvirtual

◆ get_goto_program()

bool esbmc_parseoptionst::get_goto_program	(	optionst &	options,
		goto_functionst &	goto_functions )

protectedvirtual

◆ has_cbmc_binary_input()

bool esbmc_parseoptionst::has_cbmc_binary_input ( )

protected

True if any –binary input is a CBMC goto-binary (magic 0x7f 'G' 'B' 'F').

◆ help()

void esbmc_parseoptionst::help ( )

overridevirtual

Reimplemented from parseoptions_baset.

◆ is_base_case_violated()

tvt esbmc_parseoptionst::is_base_case_violated	(	optionst &	options,
		goto_functionst &	goto_functions,
		const uint64_t &	k_step )

protected

◆ is_inductive_step_violated()

tvt esbmc_parseoptionst::is_inductive_step_violated	(	optionst &	options,
		goto_functionst &	goto_functions,
		const uint64_t &	k_step )

protected

◆ output_goto_program()

bool esbmc_parseoptionst::output_goto_program	(	optionst &	options,
		goto_functionst &	goto_functions )

protectedvirtual

◆ parse_goto_program()

bool esbmc_parseoptionst::parse_goto_program	(	optionst &	options,
		goto_functionst &	goto_functions )

protectedvirtual

◆ preprocessing()

void esbmc_parseoptionst::preprocessing ( )

protected

◆ print_ileave_points()

void esbmc_parseoptionst::print_ileave_points	(	namespacet &	ns,
		goto_functionst &	goto_functions )

protected

◆ process_function_contracts()

bool esbmc_parseoptionst::process_function_contracts	(	goto_functionst &	goto_functions,
		bool	has_replace,
		bool	has_enforce,
		bool	has_enforce_all,
		bool	has_replace_all )

protected

Process function contracts if enabled.

Parameters

goto_functions	GOTO functions
has_replace	Whether to replace calls with contracts
has_enforce	Whether to enforce contracts
has_enforce_all	Whether to enforce contracts for all annotated functions
has_replace_all	Whether to replace calls for all annotated functions

Returns: True on a usage error, e.g. a named function that nothing acted on

◆ process_goto_program()

bool esbmc_parseoptionst::process_goto_program	(	optionst &	options,
		goto_functionst &	goto_functions )

protectedvirtual

goto-cov will also mutate the asserts added by esbmc (e.g. goto-check)

◆ read_goto_binary()

bool esbmc_parseoptionst::read_goto_binary ( goto_functionst & goto_functions )

protected

◆ read_mem_spec()

uint64_t esbmc_parseoptionst::read_mem_spec ( std::string_view str )

protected

◆ read_time_spec()

uint64_t esbmc_parseoptionst::read_time_spec ( std::string_view str )

protected

◆ run_chosen_strategy()

int esbmc_parseoptionst::run_chosen_strategy	(	optionst &	options,
		goto_functionst &	goto_functions )

protected

◆ set_claims()

bool esbmc_parseoptionst::set_claims ( goto_functionst & goto_functions )

protected

◆ synthesize_cprover_additions()

bool esbmc_parseoptionst::synthesize_cprover_additions	(	optionst &	options,
		goto_functionst &	goto_functions )

protected

Synthesises ESBMC's "additions" (the __ESBMC_main entry wrapper and the CPROVER-intrinsic bodies) by compiling a boilerplate translation unit through the C frontend into the given symbol table / goto functions, so a CBMC goto-binary verifies without manually linking a library.goto.

Returns true on error.

◆ ts_strategy_requested()

bool esbmc_parseoptionst::ts_strategy_requested ( ) const

protected

◆ wants_loop_invariants()

bool esbmc_parseoptionst::wants_loop_invariants ( ) const

protected

Whether the run needs the loop-invariant machinery.

–synthesise-loop-invariants supplies the invariants that –loop-invariant-check discharges, so it implies that mode.

Member Data Documentation

◆ dead_store_advisories

std::vector<dead_store_advisoryt> esbmc_parseoptionst::dead_store_advisories

protected

◆ goto_functions

goto_functionst esbmc_parseoptionst::goto_functions

◆ goto_preprocess_algorithms

std::vector<std::unique_ptr<goto_functions_algorithm> > esbmc_parseoptionst::goto_preprocess_algorithms

protected

◆ is_coverage

bool esbmc_parseoptionst::is_coverage

protected

◆ out

FILE* esbmc_parseoptionst::out = stderr

protected

The documentation for this class was generated from the following files:

src/esbmc/esbmc_parseoptions.h
src/esbmc/parseoptions/bmc_strategy.cpp
src/esbmc/parseoptions/command_line_options.cpp
src/esbmc/parseoptions/driver.cpp
src/esbmc/parseoptions/function_contracts.cpp
src/esbmc/parseoptions/goto_program.cpp
src/esbmc/parseoptions/k_induction.cpp
src/esbmc/parseoptions/process_goto_program.cpp
src/esbmc/parseoptions/property_monitors.cpp
src/esbmc/parseoptions/ts_strategy.cpp

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Additional Inherited Members

Constructor & Destructor Documentation

◆ esbmc_parseoptionst()

◆ ~esbmc_parseoptionst()

Member Function Documentation

◆ add_monitor_exprs()

◆ add_property_monitors()

◆ apply_loop_invariants()

◆ calculate_a_property_monitor()

◆ create_goto_program()

◆ diagnose_unknown_properties()

◆ do_bmc()

◆ do_bmc_strategy()

◆ do_context_bound_deepening()

◆ do_ts_strategy()

◆ does_forward_condition_hold()

◆ doit()

◆ doit_k_induction_parallel()

◆ falsify_with_bounded_schedules()

◆ fatal_signal_advice()

◆ get_command_line_options()

◆ get_goto_program()

◆ has_cbmc_binary_input()

◆ help()

◆ is_base_case_violated()

◆ is_inductive_step_violated()

◆ output_goto_program()

◆ parse_goto_program()

◆ preprocessing()

◆ print_ileave_points()

◆ process_function_contracts()

◆ process_goto_program()

◆ read_goto_binary()

◆ read_mem_spec()

◆ read_time_spec()

◆ run_chosen_strategy()

◆ set_claims()

◆ synthesize_cprover_additions()

◆ ts_strategy_requested()

◆ wants_loop_invariants()

Member Data Documentation

◆ dead_store_advisories

◆ goto_functions

◆ goto_preprocess_algorithms

◆ is_coverage

◆ out