k_induction.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 <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/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>

Classes
struct	resultt

Enumerations
enum	PROCESS_TYPE {   BASE_CASE , FORWARD_CONDITION , INDUCTIVE_STEP , NUM_CHILD_PROCESSES ,   PARENT = NUM_CHILD_PROCESSES }

Functions
static void	report_no_answer (int pipe_fd, resultt &r, uint64_t max_k_step)
	Tell the parent this child reached no answer.
static bool	base_case_found_bug (smt_resultt res, const bmct &bmc, bool &unknown_base_case)
	Whether a base-case run found a bug.
static void	report_base_case_end (int pipe_fd, resultt &r, uint64_t no_answer_k, bool unknown_base_case)
	Tell the parent the base case found no bug, or no answer if one k left it unknown.

Enumeration Type Documentation

PROCESS_TYPE

enum PROCESS_TYPE

Enumerator
BASE_CASE
FORWARD_CONDITION
INDUCTIVE_STEP
NUM_CHILD_PROCESSES
PARENT

Function Documentation

base_case_found_bug()

bool base_case_found_bug ( smt_resultt res, const bmct & bmc, bool & unknown_base_case )

static

Whether a base-case run found a bug.

A run that only refutes the loop-invariant abstraction found none, but leaves the base case unknown while a larger k may still find a real bug (#7516).

report_base_case_end()

void report_base_case_end ( int pipe_fd, resultt & r, uint64_t no_answer_k, bool unknown_base_case )

static

Tell the parent the base case found no bug, or no answer if one k left it unknown.

report_no_answer()

void report_no_answer ( int pipe_fd, resultt & r, uint64_t max_k_step )

static

Tell the parent this child reached no answer.

max_k_step is the sentinel the parent initialises solution[] with and tests for a crashed child, so reporting it keeps a failed run from being read as a completed one.