process_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/arith/ieee_float.h>
#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_invariant_synthesis.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_library_assertions.h>
#include <goto-programs/remove_exceptions.h>
#include <goto-programs/lower_longjmp.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/andersen.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	set_model_global (goto_functionst &goto_functions, const irep_idt &name, const BigInt &value)
static bool	apply_taylor_terms (goto_functionst &goto_functions, const cmdlinet &cmdline)
static bool	apply_rounding_mode (goto_functionst &goto_functions, const cmdlinet &cmdline)
static void	apply_gcse (goto_functionst &goto_functions, contextt &context, const cmdlinet &cmdline)
static std::set< irep_idt >	unreported_exceptions (const optionst &options)

Function Documentation

apply_gcse()

void apply_gcse ( goto_functionst & goto_functions, contextt & context, const cmdlinet & cmdline )

static

apply_rounding_mode()

bool apply_rounding_mode ( goto_functionst & goto_functions, const cmdlinet & cmdline )

static

apply_taylor_terms()

bool apply_taylor_terms ( goto_functionst & goto_functions, const cmdlinet & cmdline )

static

set_model_global()

bool set_model_global ( goto_functionst & goto_functions, const irep_idt & name, const BigInt & value )

static

unreported_exceptions()

std::set< irep_idt > unreported_exceptions ( const optionst & options )

static