goto_program.cpp File Reference

#include <ac_config.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/base/prefix.h>
#include <util/expr/base_type.h>
#include <util/expr/expr_util.h>
#include <util/irep/migrate.h>
#include <set>
#include <unordered_set>
#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/lift_call_expressions.h>
#include <goto-programs/goto_convert_class.h>
#include <goto-programs/goto_convert_functions.h>
#include <goto-programs/exception_typeid.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 <c2goto/cprover_library.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>
#include <fcntl.h>

Functions
static bool	retarget_esbmc_main (goto_functionst &goto_functions, const irep_idt &target, goto_programt init={})
static exprt	cbmc_static_init_value (const symbolt &sym, const namespacet &ns)
static bool	is_cbmc_constructor (const symbolt &sym)
static goto_programt	cbmc_static_init (contextt &context, optionst &options, const std::unordered_set< irep_idt, irep_id_hash > &preexisting)
static bool	bridge_binary_entry_point (const cmdlinet &cmdline, contextt &context, optionst &options, goto_functionst &goto_functions, bool cbmc_additions, const std::unordered_set< irep_idt, irep_id_hash > &preexisting)
static void	link_cbmc_libc_bodies (goto_functionst &goto_functions)
static void	skip_property_classes (const cmdlinet &cmdline, goto_functionst &goto_functions)
static void	warn_undefined_external_symbols (const contextt &context)
static void	expand_no_standard_checks (const cmdlinet &cmdline, optionst &options)
static void	expand_python_check_exceptions (const contextt &context, optionst &options)

Function Documentation

bridge_binary_entry_point()

bool bridge_binary_entry_point ( const cmdlinet & cmdline, contextt & context, optionst & options, goto_functionst & goto_functions, bool cbmc_additions, const std::unordered_set< irep_idt, irep_id_hash > & preexisting )

static

cbmc_static_init()

goto_programt cbmc_static_init ( contextt & context, optionst & options, const std::unordered_set< irep_idt, irep_id_hash > & preexisting )

static

cbmc_static_init_value()

exprt cbmc_static_init_value ( const symbolt & sym, const namespacet & ns )

static

expand_no_standard_checks()

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

static

expand_python_check_exceptions()

void expand_python_check_exceptions ( const contextt & context, optionst & options )

static

is_cbmc_constructor()

bool is_cbmc_constructor ( const symbolt & sym )

static

link_cbmc_libc_bodies()

void link_cbmc_libc_bodies ( goto_functionst & goto_functions )

static

retarget_esbmc_main()

bool retarget_esbmc_main ( goto_functionst & goto_functions, const irep_idt & target, goto_programt init = {} )

static

skip_property_classes()

void skip_property_classes ( const cmdlinet & cmdline, goto_functionst & goto_functions )

static

warn_undefined_external_symbols()

void warn_undefined_external_symbols ( const contextt & context )

static