docs/api/goto__symex_8h_source.html

#ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_H

#define CPROVER_GOTO_SYMEX_GOTO_SYMEX_H


#include <goto-programs/goto_functions.h>

#include <util/base/threeval.h>

#include <goto-programs/abstract-interpretation/interval_domain.h>

#include <goto-symex/state/goto_symex_state.h>

#include <goto-symex/equation/symex_target.h>

#include <functional>

#include <map>

#include <optional>

#include <pointer-analysis/dereference.h>

#include <util/base/i2string.h>

#include <irep2/irep2.h>

#include <util/config/options.h>

#include <util/irep/std_types.h>


class reachability_treet; // Forward dec

class execution_statet;   // Forward dec

class printf_formattert;


// Thrown by symex when the inductive step encounters a construct it cannot

// soundly encode (recursion, threads, function-pointer calls). The thrower

// also sets `disable-inductive-step` so the strategy layer downgrades the

// result to UNKNOWN; the throw short-circuits the rest of symex.


class inductive_step_disabled_exceptiont

{

public:


  explicit inductive_step_disabled_exceptiont(std::string r)

    : reason(std::move(r))

  {

  }


  std::string reason;

};


class goto_symext

{

public:

  goto_symext(

    const namespacet &_ns,

    contextt &_new_context,

    const goto_functionst &goto_functions,

    std::shared_ptr<symex_targett> _target,

    optionst &opts);

  goto_symext(const goto_symext &sym);

  goto_symext &operator=(const goto_symext &sym);


  // Types


public:


  class allocated_obj

  {

  public:


    allocated_obj(

      const expr2tc &s,

      const guard2tc &g,

      const bool a,

      const std::string n)

      : obj(s), alloc_guard(g), auto_deallocd(a), name(n)

    {

    }


    expr2tc obj;

    guard2tc alloc_guard;

    bool auto_deallocd;

    std::string name;

  };


  friend class symex_dereference_statet;

  friend class bmct;

  friend class reachability_treet;


  typedef goto_symex_statet statet;


  class symex_resultt

  {

  public:


    symex_resultt(

      std::shared_ptr<symex_targett> t,

      unsigned int claims,

      unsigned int remain,

      unsigned int simplified,

      unsigned int truncations = 0)

      : target(std::move(t)),

        total_claims(claims),

        remaining_claims(remain),

        simplified_claims(simplified),

        bounded_loop_truncations(truncations) {};


    std::shared_ptr<symex_targett> target;

    unsigned int total_claims;

    unsigned int remaining_claims;

    unsigned int simplified_claims;

    unsigned int bounded_loop_truncations;

  };


  expr2tc guard_identifier()

  {

    return symbol2tc(

      get_bool_type(),

      id2string(guard_identifier_s),

      symbol_renaming_level::level1,

      0,

      0,

      cur_state->top().level1.thread_id,

      0);

  };


  // Methods


  bool chase_copies(expr2tc &expr) const;


  tvt::tv_enumt path_guard_decides(

    const expr2tc &new_guard,

    bool already_false,

    bool already_true);


  void record_guard_definition(const expr2tc &guard_expr, const expr2tc &rhs);


  expr2tc rewrite_conjunct(const expr2tc &conjunct);


  using conjunct_indext = persistent_map<expr2tc, size_t, irep2_hash>;


  conjunct_indext prefix_index(const guard2tc &guard);


  void record_copy_definition(const expr2tc &renamed_lhs, const expr2tc &rhs);


  goto_symext::symex_resultt get_symex_result();


  virtual void symex_step(reachability_treet &art);


  void add_memory_leak_checks();


protected:

  virtual void do_simplify(expr2tc &expr);


  expr2tc branch_decision_guard(const expr2tc &guard) const;


  void dereference(

    expr2tc &expr,

    dereferencet::modet mode,

    bool block_assertions = false);


  // symex


  virtual void symex_goto(const expr2tc &old_guard);


  virtual void record_parked_path(

    goto_programt::const_targett /*target*/,

    statet::merge_state_listt::iterator /*parked*/)

  {

  }


  void symex_return(const expr2tc &code);

  void

  symex_witness_function_return(expr2tc ret_val, const irep_idt &call_line);

  bool symex_witness_function_enter(const irep_idt &call_line);

  void symex_witness_branching(

    const expr2tc &old_guard,

    const expr2tc &new_guard,

    bool forward,

    bool &new_guard_true,

    bool &new_guard_false,

    const goto_programt::instructiont &instruction);

  void symex_witness_assert(expr2tc &new_expr, const std::string &msg);


  void symex_other(const expr2tc &code);


  void symex_decl(const expr2tc &code);


  void symex_dead(const expr2tc &code);


  bool stack_checks_enabled() const

  {

    return stack_limit > 0 || total_stack_limit > 0;

  }


  void check_stack_size(const expr2tc &expr, const std::string &subject = "");


  void symex_assume();


  void symex_assert();


public:

  static std::string

  assertion_message(const namespacet &ns, const goto_programt::instructiont &i);


  void release_symex_caches()

  {

    guard_prefix_index.clear();

  }


protected:

  bool check_incremental(const expr2tc &expr, const std::string &msg);


  virtual void claim(const expr2tc &expr, const std::string &msg);


  void record_property_verdict(

    const std::string &msg,

    property_verdictt verdict,

    const std::string &note = "");


  virtual void assertion(const expr2tc &assertion, const std::string &msg);


  void propagate_assume_equality(const expr2tc &the_assumption);


  virtual void assume(const expr2tc &assumption);


  virtual void defer_assumption(const expr2tc &assumption);


  void flush_deferred_assumptions();


  // gotos

  void merge_gotos();


  void merge_value_sets(const statet::merge_statet &merge_state);


  void merge_locality(const statet::merge_statet &merge_state);


  void snapshot_interval_domain(statet::merge_statet &merge_state);


  void assume_loop_continues(

    const goto_programt::instructiont &instruction,

    const expr2tc &guard,

    bool forward,

    bool always_jumps);


  void merge_interval_domain(const statet::merge_statet &merge_state);


  void phi_function(const statet::merge_statet &merge_state);


  bool get_unwind(const symex_targett::sourcet &source, const BigInt &unwind);


  void loop_bound_exceeded(const expr2tc &guard);


  virtual void note_bounded_loop_truncation()

  {

    ++bounded_loop_truncations;

  }


  // function calls


  void pop_frame();


  bool is_python_gc_object(const symbolt *base) const;


  bool make_return_assignment(expr2tc &assign, const expr2tc &code_return);


  void symex_function_call(const expr2tc &call);


  void symex_end_of_function();


  virtual void symex_function_call_deref(const expr2tc &call);


  virtual void symex_function_call_code(const expr2tc &call);


  bool symex_uninterpreted_function(

    const code_function_call2t &call,

    const irep_idt &identifier);


  bool get_unwind_recursion(const irep_idt &identifier, BigInt unwind);


  expr2tc argument_value(

    const type2tc &arg_type,

    const expr2tc &rhs,

    const irep_idt &identifier);


  unsigned int argument_assignments(

    const irep_idt &function_identifier,

    const code_type2t &function_type,

    const std::vector<expr2tc> &arguments);


  bool run_next_function_ptr_target(bool first);


  void run_intrinsic(

    const code_function_call2t &call,

    reachability_treet &art,

    const std::string &symname);


  bool

  run_builtin(const code_function_call2t &call, const std::string &symname);


  void symex_bounded_math(

    const code_function_call2t &call,

    const std::string &function);


  void intrinsic_yield(reachability_treet &arg);

  void

  intrinsic_switch_to(const code_function_call2t &c, reachability_treet &art);

  void intrinsic_switch_from(reachability_treet &arg);

  void intrinsic_get_thread_id(

    const code_function_call2t &call,

    reachability_treet &art);

  void intrinsic_set_thread_data(

    const code_function_call2t &call,

    reachability_treet &art);

  void intrinsic_get_thread_data(

    const code_function_call2t &call,

    reachability_treet &art);

  void intrinsic_spawn_thread(

    const code_function_call2t &call,

    reachability_treet &art);

  void intrinsic_terminate_thread(reachability_treet &art);

  void intrinsic_havoc_object(const code_function_call2t &call);

  void intrinsic_init_thread_local(reachability_treet &art);

  void intrinsic_really_atomic_begin(reachability_treet &art);

  void intrinsic_really_atomic_end(reachability_treet &art);

  void intrinsic_switch_to_monitor(reachability_treet &art);

  void intrinsic_switch_from_monitor(reachability_treet &art);

  void intrinsic_register_monitor(

    const code_function_call2t &call,

    reachability_treet &art);

  void intrinsic_kill_monitor(reachability_treet &art);

  void intrinsic_memset(

    reachability_treet &art,

    const code_function_call2t &func_call);


  void intrinsic_memcpy(

    reachability_treet &art,

    const code_function_call2t &func_call);


  void intrinsic_memchr(

    reachability_treet &art,

    const code_function_call2t &func_call);


  void intrinsic_memcmp(

    reachability_treet &art,

    const code_function_call2t &func_call);


  bool memcpy_symbolic_length(

    const expr2tc &dst_arg,

    const expr2tc &src_arg,

    const expr2tc &n_arg);


  void memcpy_finish(

    const code_function_call2t &func_call,

    const expr2tc &dst_arg,

    const expr2tc &src_arg,

    const expr2tc &n_arg);


  void claim_valid_operand(

    const expr2tc &ptr,

    const expr2tc &n,

    const std::string &func);


  void claim_not_code(const expr2tc &guard);


  bool memcmp_resolve_operand(

    const expr2tc &ptr,

    unsigned long number_of_bytes,

    expr2tc &object,

    uint64_t &offset,

    uint64_t &avail_bytes,

    bool rename_object = true);


  void claim_nonnull_operand(

    const expr2tc &ptr,

    const expr2tc &n,

    const std::string &func);


  void intrinsic_memmove(

    reachability_treet &art,

    const code_function_call2t &func_call);


  void intrinsic_memcpy_impl(

    reachability_treet &art,

    const code_function_call2t &func_call,

    const std::string &bump_name);


  // Function to call a symname function, in case where were not able to

  // optimize it

  void

  bump_call(const code_function_call2t &func_call, const std::string &symname);


  void intrinsic_get_object_size(

    const code_function_call2t &func_call,

    reachability_treet &art);


  void intrinsic_builtin_object_size(

    const code_function_call2t &func_call,

    reachability_treet &art);


  /* Handles dereferencing between threads and is used only in data race checks.

   * **/

  void replace_races_check(expr2tc &expr);


  void simplify_python_builtins(expr2tc &expr);

  void reject_untyped_isinstance(const expr2tc &value);


  void volatile_check(expr2tc &expr);


  void finalize_realloc_result(

    const expr2tc &lhs,

    const expr2tc &result,

    const expr2tc &new_array,

    const guard2tc &guard,

    const expr2tc &realloc_size,

    const expr2tc &alloc_fail);


  void update_pointer_validity(

    const expr2tc &old_ptr,

    const expr2tc &alloc_fail,

    const guard2tc &guard);


  expr2tc model_allocation_failure(

    const expr2tc &result,

    const expr2tc &old_ptr,

    const guard2tc &guard,

    const expr2tc &over_cap,

    expr2tc &alloc_fail);


  void bound_dynamic_object_size(const code_assign2t &code);


  expr2tc

  create_result_pointer(const expr2tc &new_array, const type2tc &lhs_type);


  expr2tc calculate_old_element_count(

    const expr2tc &old_base_array,

    const type2tc &elem_type,

    bool old_is_array);


  expr2tc

  calculate_element_count(const expr2tc &size_bytes, const expr2tc &elem_size);


  type2tc

  determine_fallback_element_type(const sideeffect2t &code, const expr2tc &lhs);


  void analyze_old_object(

    const expr2tc &old_obj,

    type2tc &elem_type,

    expr2tc &old_base_array,

    bool &old_is_array);


  void copy_old_objects(

    const std::list<dereference_callbackt::internal_item> &old_objects,

    const expr2tc &new_array,

    const expr2tc &new_elem_count,

    const type2tc &elem_type,

    const guard2tc &guard);


  bool handle_realloc_zero_size(

    const expr2tc &lhs,

    const sideeffect2t &code,

    const guard2tc &guard,

    const expr2tc &realloc_size);


  void copy_single_element(

    const expr2tc &old_base_array,

    const expr2tc &new_array,

    const expr2tc &idx,

    const type2tc &elem_type,

    const type2tc &new_elem_type,

    bool old_is_array,

    const guard2tc &guard);


  void copy_memory_content(

    const expr2tc &old_base_array,

    const expr2tc &new_array,

    const expr2tc &old_elem_count,

    const expr2tc &new_elem_count,

    const type2tc &elem_type,

    bool old_is_array,

    const guard2tc &guard);


  expr2tc create_dynamic_memory_symbol(

    const type2tc &elem_type,

    const expr2tc &size_expr,

    const std::string &name_prefix);


  bool terminate_handler();


  bool unexpected_handler();


  void replace_dynamic_allocation(expr2tc &expr);


  std::vector<expr2tc> value_set_objects(const expr2tc &ptr, bool &complete);

  expr2tc named_object(const expr2tc &base) const;

  bool resolve_by_value_set(

    expr2tc &expr,

    const expr2tc &ptr,

    const std::function<expr2tc(const expr2tc &)> &resolve);

  bool resolve_valid_object_by_value_set(expr2tc &expr, const expr2tc &obj_ref);

  bool resolve_dynamic_size_by_value_set(expr2tc &expr);

  void replace_valid_object(expr2tc &expr);

  void replace_dynamic_size(expr2tc &expr);

  void default_replace_dynamic_allocation(expr2tc &expr);


  bool is_valid_object(const symbolt &symbol);


  void handle_sideeffect(

    const expr2tc &lhs,

    const sideeffect2t &effect,

    const guard2tc &guard);


  bool handle_conditional(

    const expr2tc &lhs,

    const if2t &if_effect,

    const guard2tc &guard);


  virtual void symex_assign(

    const expr2tc &code,

    const bool hidden = false,

    const guard2tc &guard = guard2tc());


  expr2tc materialise_old_snapshot(const expr2tc &value, const guard2tc &guard);


  void symex_assign_rec(

    const expr2tc &lhs,

    const expr2tc &full_lhs,

    expr2tc &rhs,

    expr2tc full_rhs,

    guard2tc &guard,

    const bool hidden);


  void symex_assign_symbol(

    const expr2tc &lhs,

    const expr2tc &full_lhs,

    expr2tc &rhs,

    expr2tc &full_rhs,

    guard2tc &guard,

    const bool hidden);


  void symex_assign_structure(

    const expr2tc &lhs,

    const expr2tc &full_lhs,

    expr2tc &rhs,

    expr2tc &full_rhs,

    guard2tc &guard,

    const bool hidden);


  void symex_assign_array_structure(

    const expr2tc &lhs,

    const expr2tc &full_lhs,

    expr2tc &rhs,

    expr2tc &full_rhs,

    guard2tc &guard,

    const bool hidden);


  void symex_assign_union(

    const expr2tc &lhs,

    const expr2tc &full_lhs,

    expr2tc &rhs,

    expr2tc &full_rhs,

    guard2tc &guard,

    const bool hidden);


  void symex_assign_extract(

    const expr2tc &lhs,

    const expr2tc &full_lhs,

    expr2tc &rhs,

    expr2tc &full_rhs,

    guard2tc &guard,

    const bool hidden);


  void symex_assign_typecast(

    const expr2tc &lhs,

    const expr2tc &full_lhs,

    expr2tc &rhs,

    expr2tc &full_rhs,

    guard2tc &guard,

    const bool hidden);


  void symex_assign_array(

    const expr2tc &lhs,

    const expr2tc &full_lhs,

    expr2tc &rhs,

    expr2tc &full_rhs,

    guard2tc &guard,

    const bool hidden);


  void symex_assign_member(

    const expr2tc &lhs,

    const expr2tc &full_lhs,

    expr2tc &rhs,

    expr2tc &full_rhs,

    guard2tc &guard,

    const bool hidden);


  void symex_assign_if(

    const expr2tc &lhs,

    const expr2tc &full_lhs,

    expr2tc &rhs,

    expr2tc &full_rhs,

    guard2tc &guard,

    const bool hidden);


  void symex_assign_byte_extract(

    const expr2tc &lhs,

    const expr2tc &full_lhs,

    expr2tc &rhs,

    expr2tc &full_rhs,

    guard2tc &guard,

    const bool hidden);


  void symex_assign_concat(

    const expr2tc &lhs,

    const expr2tc &full_lhs,

    expr2tc &rhs,

    expr2tc &full_rhs,

    guard2tc &guard,

    const bool hidden);


  void symex_assign_bitfield(

    const expr2tc &lhs,

    const expr2tc &full_lhs,

    expr2tc &rhs,

    expr2tc &full_rhs,

    guard2tc &guard,

    const bool hidden);


  expr2tc symex_malloc(

    const expr2tc &lhs,

    const sideeffect2t &code,

    const guard2tc &guard);

  void symex_realloc(

    const expr2tc &lhs,

    const sideeffect2t &code,

    const guard2tc &guard);

  expr2tc symex_alloca(

    const expr2tc &lhs,

    const sideeffect2t &code,

    const guard2tc &guard);

  expr2tc symex_mem(

    const bool is_malloc,

    const expr2tc &lhs,

    const sideeffect2t &code,

    const guard2tc &guard);

  void offer_malloc_zero_null(

    const expr2tc &size,

    expr2tc &rhs,

    guard2tc &alloc_guard);

  expr2tc symex_mem_inf(

    const expr2tc &lhs,

    const type2tc &base_type,

    const guard2tc &guard);


  void track_new_pointer(

    const expr2tc &ptr_obj,

    const type2tc &new_type,

    const guard2tc &guard,

    const expr2tc &size = expr2tc());

  void record_frame_alloca(

    const expr2tc &lhs,

    const expr2tc &object,

    bool is_malloc);

  void symex_free(const expr2tc &expr);

  void invalidate_object(const expr2tc &ptr);

  void symex_cpp_delete(const expr2tc &code);

  void symex_cpp_new(

    const expr2tc &lhs,

    const sideeffect2t &code,

    const guard2tc &guard);

  virtual void symex_printf(const expr2tc &lhs, expr2tc &code);

  expr2tc symex_sprintf_store(const code_printf2t &call);

  expr2tc sprintf_output(

    const code_printf2t &call,

    size_t fmt_idx,

    const type2tc &char_type,

    std::vector<expr2tc> &chars);

  expr2tc printf_output_length(

    const code_printf2t &call,

    size_t fmt_idx,

    size_t &max_len);

  expr2tc string_length(const expr2tc &ptr, size_t &max_len);

  expr2tc printf_return_length(

    const expr2tc &lhs,

    const code_printf2t &call,

    size_t fmt_idx);

  void assume_printf_length(const expr2tc &retval, const expr2tc &len);

  void assume_printf_range(

    const expr2tc &retval,

    const BigInt &lo,

    const BigInt &hi,

    bool may_fail);

  void symex_asprintf_buffer(const expr2tc &strp, const expr2tc &retval);

  bool format_printf_output(

    const code_printf2t &call,

    size_t fmt_idx,

    printf_formattert &formatter,

    bool &constant_args);

  bool recover_va_list_args(

    const code_printf2t &call,

    size_t fmt_idx,

    std::list<expr2tc> &out);

  void symex_input(const code_function_call2t &expr);

  void symex_va_arg(

    const expr2tc &lhs,

    const sideeffect2t &code,

    const guard2tc &guard);

  std::optional<renaming::level2t::name_record>

  va_list_l1_record(const expr2tc &va_list_expr) const;

  std::vector<renaming::level2t::name_record>

  va_list_pointee_records(const expr2tc &va_list_expr) const;

  bool va_list_is_started(const expr2tc &va_list_expr) const;

  void va_list_mark_started(

    const expr2tc &va_list_expr,

    bool started,

    const expr2tc &cursor);

  void va_list_start(const expr2tc &va_list_expr);

  expr2tc va_list_cursor_symbol(const renaming::level2t::name_record &rec);

  expr2tc va_list_cursor(const expr2tc &va_list_expr);

  std::vector<renaming::level2t::name_record>

  va_list_owner_records(const expr2tc &va_list_expr) const;

  void va_list_copy(const expr2tc &dst, const expr2tc &src);

  goto_symex_statet::framet &va_list_frame(const expr2tc &va_list_expr);


  void replace_nondet(expr2tc &expr);


  virtual unsigned int &get_dynamic_counter() = 0;

  virtual unsigned int &get_nondet_counter() = 0;

  bool is_assume_false(const expr2tc &assumption);


  // Members


  optionst &options;

  irep_idt guard_identifier_s;

  static constexpr size_t max_copy_definition_nodes = 64;

  persistent_map<irep_idt, expr2tc, irep_id_hash> guard_definitions;

  persistent_map<irep_idt, expr2tc, irep_id_hash> copy_definitions;

  persistent_map<expr2tc, conjunct_indext, irep2_hash> guard_prefix_index;


  struct deferred_assumptiont

  {

    expr2tc guard;

    expr2tc cond;

    symex_targett::sourcet source;

    unsigned loop_number;

  };


  std::vector<deferred_assumptiont> deferred_assumptions;

  bool claim_skips_deferred = false;


  std::unordered_map<irep_idt, expr2tc> dynamic_object_sizes;


  unsigned first_loop;

  unsigned total_claims;

  unsigned remaining_claims;

  unsigned simplified_claims;

  unsigned bounded_loop_truncations = 0;

  reachability_treet *art1;

  std::map<unsigned, BigInt> unwind_set;

  std::map<std::pair<std::string, unsigned>, BigInt> unwind_func_set;

  std::map<unsigned, std::pair<std::string, unsigned>> loop_id_to_func_index;

  BigInt max_unwind;

  std::optional<interval_domaint> interval_domain_state;

  const namespacet &ns;

  contextt &new_context;

  const goto_functionst &goto_functions;

  std::shared_ptr<symex_targett> target;

  goto_symex_statet *cur_state;

  irep_idt valid_ptr_arr_name, alloc_size_arr_name, dyn_info_arr_name;

  std::list<allocated_obj> dynamic_memory;


  std::map<irep_idt, std::vector<std::pair<std::vector<expr2tc>, expr2tc>>>

    uf_applications;


  void assume_uf_congruence(

    const irep_idt &identifier,

    const irep_idt &name,

    const std::vector<expr2tc> &arguments,

    const expr2tc &result,

    const type2tc &ret_type);


  std::unordered_map<

    renaming::level2t::name_record,

    bool,

    renaming::level2t::name_rec_hash>

    va_started;

  std::unordered_map<

    renaming::level2t::name_record,

    renaming::level2t::name_record,

    renaming::level2t::name_rec_hash>

    va_copied_from;


  bool no_return_value_opt;

  unsigned long stack_limit;

  unsigned long total_stack_limit;

  unsigned long depth_limit;

  unsigned long break_insn;

  bool memory_leak_check;

  bool no_reachable_memleak;

  bool no_assertions;

  bool no_simplify;

  bool no_unwinding_assertions;

  bool partial_loops;

  bool k_induction;

  bool base_case;

  bool forward_condition;

  bool inductive_step;

  bool validate_witness;


  std::list<dereference_callbackt::internal_item> internal_deref_items;

  virtual void analyze_args(const expr2tc &expr) = 0;

  void key_intrinsic_pointer_reads(

    const code_function_call2t &call,

    const irep_idt &id);

  friend void build_goto_symex_classes();

};


class symex_dereference_statet : public dereference_callbackt

{

public:


  symex_dereference_statet(

    goto_symext &_goto_symex,

    goto_symext::statet &_state)

    : goto_symex(_goto_symex), state(_state)

  {

  }


protected:

  goto_symext &goto_symex;

  goto_symext::statet &state;


  void dereference_failure(

    const std::string &property,

    const std::string &msg,

    const guard2tc &guard) override;


  void dereference_assume(const guard2tc &guard) override;


  void

  get_value_set(const expr2tc &expr, value_setst::valuest &value_set) override;


  bool has_failed_symbol(const expr2tc &expr, const symbolt *&symbol) override;


  void rename(expr2tc &expr) override;


  void

  dump_internal_state(const std::list<struct internal_item> &data) override;

  bool is_live_variable(const expr2tc &sym) override;

};


namespace goto_symex_utils

{

expr2tc gen_byte_memcpy(

  const expr2tc &src,

  const expr2tc &dst,

  const size_t num_of_bytes,

  const size_t src_offset,

  const size_t dst_offset);


bool is_alloca_return_value_name(const std::string &name);

} // namespace goto_symex_utils


#endif

base_type
void base_type(type2tc &type, const namespacet &ns)
Definition base_type.cpp:6

base
static const twodig_t base
Definition bigint.cpp:28

get_bool_type
type2tc get_bool_type()
Definition c_types.cpp:418

char_type
typet char_type()
Definition c_types.cpp:166

BigInt
Definition bigint.hh:58

code_assign2t
Definition irep2_expr.h:2007

code_function_call2t
Definition irep2_expr.h:2175

code_printf2t
Definition irep2_expr.h:2034

code_type2t
Type of functions.
Definition irep2_type.h:333

contextt
Definition context.h:57

dereference_callbackt
Class providing interface to value set tracking code.
Definition dereference.h:96

execution_statet
Thread-aware symex state explored by reachability_treet.
Definition execution_state.h:46

formatter
Definition toml.hpp:10247

goto_functionst
Definition goto_functions.h:56

goto_programt::instructiont
Container for an instruction of the goto-program.
Definition goto_program.h:95

goto_programt::const_targett
instructionst::const_iterator const_targett
Definition goto_program.h:591

goto_symex_statet::framet
Stack frame tracking class.
Definition goto_symex_state.h:161

goto_symex_statet
Class for storing a particular threads state.
Definition goto_symex_state.h:36

goto_symext::allocated_obj::allocated_obj
allocated_obj(const expr2tc &s, const guard2tc &g, const bool a, const std::string n)
Definition goto_symex.h:73

goto_symext::allocated_obj::obj
expr2tc obj
Symbol identifying the pointer that was allocated.
Definition goto_symex.h:82

goto_symext::allocated_obj::name
std::string name
The object name.
Definition goto_symex.h:89

goto_symext::allocated_obj::auto_deallocd
bool auto_deallocd
Record if the object is automatically desallocated (allocated with alloca).
Definition goto_symex.h:87

goto_symext::allocated_obj::alloc_guard
guard2tc alloc_guard
Guard when allocation occured.
Definition goto_symex.h:84

goto_symext::symex_resultt
Class recording the outcome of symbolic execution.
Definition goto_symex.h:106

goto_symext::symex_resultt::target
std::shared_ptr< symex_targett > target
Definition goto_symex.h:119

goto_symext::symex_resultt::simplified_claims
unsigned int simplified_claims
Definition goto_symex.h:122

goto_symext::symex_resultt::symex_resultt
symex_resultt(std::shared_ptr< symex_targett > t, unsigned int claims, unsigned int remain, unsigned int simplified, unsigned int truncations=0)
Definition goto_symex.h:108

goto_symext::symex_resultt::bounded_loop_truncations
unsigned int bounded_loop_truncations
Carried out of exploration rather than read back from live state: under –schedule the current frame i...
Definition goto_symex.h:126

goto_symext::symex_resultt::remaining_claims
unsigned int remaining_claims
Definition goto_symex.h:121

goto_symext::symex_resultt::total_claims
unsigned int total_claims
Definition goto_symex.h:120

goto_symext
Primay symbolic execution class.
Definition goto_symex.h:47

goto_symext::intrinsic_get_object_size
void intrinsic_get_object_size(const code_function_call2t &func_call, reachability_treet &art)
Returns the size of the object.
Definition object_size.cpp:204

goto_symext::alloc_size_arr_name
irep_idt alloc_size_arr_name
Definition goto_symex.h:1735

goto_symext::intrinsic_havoc_object
void intrinsic_havoc_object(const code_function_call2t &call)
Perform havoc_object; assign nondet to every object the argument may point to, whole and of any size.
Definition memory_ops.cpp:1845

goto_symext::invalidate_object
void invalidate_object(const expr2tc &ptr)
Clear the valid bit of the object ptr points to, with no free checks.
Definition memory_alloc.cpp:1057

goto_symext::propagate_assume_equality
void propagate_assume_equality(const expr2tc &the_assumption)
Lift var == const from an assume into the level2 constant propagator so subsequent renames of var sub...
Definition symex_main.cpp:220

goto_symext::resolve_dynamic_size_by_value_set
bool resolve_dynamic_size_by_value_set(expr2tc &expr)
Size a heap object by its allocation, and an object with automatic or static storage by its type.
Definition symex_valid_object.cpp:150

goto_symext::forward_condition
bool forward_condition
Flag as to whether we're doing a k-induction forward condition.
Definition goto_symex.h:1823

goto_symext::max_copy_definition_nodes
static constexpr size_t max_copy_definition_nodes
Cap on one recorded copy definition's flattened node count: canonicalization doubles nested arithmeti...
Definition goto_symex.h:1634

goto_symext::release_symex_caches
void release_symex_caches()
Free what only symex reads, once a formula is built: the guard prefix index grows with every branchin...
Definition goto_symex.h:367

goto_symext::max_unwind
BigInt max_unwind
Global maximum number of unwinds.
Definition goto_symex.h:1716

goto_symext::snapshot_interval_domain
void snapshot_interval_domain(statet::merge_statet &merge_state)
Record the online interval domain in a path being parked, so merge_interval_domain can join it back i...
Definition symex_goto.cpp:621

goto_symext::check_stack_size
void check_stack_size(const expr2tc &expr, const std::string &subject="")
Account expr's storage against the current frame and claim that neither –stack-limit nor –total-stack...
Definition symex_stack.cpp:39

goto_symext::record_frame_alloca
void record_frame_alloca(const expr2tc &lhs, const expr2tc &object, bool is_malloc)
Records an alloca'd object on the current frame, to die when it returns.
Definition memory_alloc.cpp:890

goto_symext::intrinsic_switch_from_monitor
void intrinsic_switch_from_monitor(reachability_treet &art)
Context switch from the monitor thread.
Definition threads.cpp:245

goto_symext::intrinsic_really_atomic_end
void intrinsic_really_atomic_end(reachability_treet &art)
Really atomic start/end - atomic blocks that just disable ileaves.
Definition threads.cpp:223

goto_symext::symex_assign_typecast
void symex_assign_typecast(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
Perform assignment to a typecast irep.
Definition symex_assign.cpp:682

goto_symext::va_list_pointee_records
std::vector< renaming::level2t::name_record > va_list_pointee_records(const expr2tc &va_list_expr) const
The l1 identity records of the local va_lists a pointer-valued expression may point to.
Definition va_arg.cpp:61

goto_symext::is_valid_object
bool is_valid_object(const symbolt &symbol)
Decide if symbol is valid or not.
Definition symex_valid_object.cpp:249

goto_symext::get_dynamic_counter
virtual unsigned int & get_dynamic_counter()=0
Fetch reference to global dynamic object counter.

goto_symext::bound_dynamic_object_size
void bound_dynamic_object_size(const code_assign2t &code)
Bound at PTRDIFF_MAX the object size an assignment records, reporting a constant request that exceeds...
Definition memory_alloc.cpp:626

goto_symext::bump_call
void bump_call(const code_function_call2t &func_call, const std::string &symname)
Definition run_builtin.cpp:15

goto_symext::va_list_cursor
expr2tc va_list_cursor(const expr2tc &va_list_expr)
The cursor symbol of a started local va_list; nil when its cursor is not known, and the frame's curso...
Definition va_arg.cpp:96

goto_symext::loop_id_to_func_index
std::map< unsigned, std::pair< std::string, unsigned > > loop_id_to_func_index
Mapping global loop ID -> (function name, per-function loop index).
Definition goto_symex.h:1714

goto_symext::symex_assign_symbol
void symex_assign_symbol(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
Perform assignment to a symbol.
Definition symex_assign.cpp:551

goto_symext::goto_functions
const goto_functionst & goto_functions
GOTO functions that we're operating over.
Definition goto_symex.h:1726

goto_symext::statet
goto_symex_statet statet
Definition goto_symex.h:96

goto_symext::format_printf_output
bool format_printf_output(const code_printf2t &call, size_t fmt_idx, printf_formattert &formatter, bool &constant_args)
Run formatter over an unrenamed printf-family call; false when the format is not a constant.
Definition io.cpp:223

goto_symext::internal_deref_items
std::list< dereference_callbackt::internal_item > internal_deref_items
Set of dereference state records; this field is used as a mailbox between the dereference code and th...
Definition goto_symex.h:1834

goto_symext::symex_input
void symex_input(const code_function_call2t &expr)
Symbolic implementation of scanf and fscanf.
Definition io.cpp:1047

goto_symext::intrinsic_register_monitor
void intrinsic_register_monitor(const code_function_call2t &call, reachability_treet &art)
Register which thread is the monitor thread.
Definition threads.cpp:251

goto_symext::replace_dynamic_size
void replace_dynamic_size(expr2tc &expr)
Size the object DYNAMIC_SIZE names, falling back to the heap-only table.
Definition symex_valid_object.cpp:213

goto_symext::analyze_old_object
void analyze_old_object(const expr2tc &old_obj, type2tc &elem_type, expr2tc &old_base_array, bool &old_is_array)
Analyze an object a reallocated pointer may point to.
Definition memory_alloc.cpp:302

goto_symext::claim_skips_deferred
bool claim_skips_deferred
Set while claim() handles a Python assert's own condition, which needs no deferred assumption.
Definition goto_symex.h:1685

goto_symext::symex_asprintf_buffer
void symex_asprintf_buffer(const expr2tc &strp, const expr2tc &retval)
Point an asprintf/vasprintf call's strp at a fresh heap buffer of retval + 1 bytes,...
Definition io.cpp:607

goto_symext::resolve_by_value_set
bool resolve_by_value_set(expr2tc &expr, const expr2tc &ptr, const std::function< expr2tc(const expr2tc &)> &resolve)
A pointer reaching a check through a parameter or a local variable is a plain symbol,...
Definition symex_valid_object.cpp:84

goto_symext::update_pointer_validity
void update_pointer_validity(const expr2tc &old_ptr, const expr2tc &alloc_fail, const guard2tc &guard)
Update pointer validity information after realloc.
Definition memory_alloc.cpp:477

goto_symext::uf_applications
std::map< irep_idt, std::vector< std::pair< std::vector< expr2tc >, expr2tc > > > uf_applications
Per-callee history of uninterpreted-function applications the SMT backend cannot encode natively,...
Definition goto_symex.h:1747

goto_symext::resolve_valid_object_by_value_set
bool resolve_valid_object_by_value_set(expr2tc &expr, const expr2tc &obj_ref)
Decide VALID_OBJECT from the object the value set names, if it names one.
Definition symex_valid_object.cpp:129

goto_symext::replace_races_check
void replace_races_check(expr2tc &expr)
Definition misc.cpp:12

goto_symext::reachability_treet
friend class reachability_treet
Definition goto_symex.h:94

goto_symext::symex_witness_assert
void symex_witness_assert(expr2tc &new_expr, const std::string &msg)
Definition witness.cpp:197

goto_symext::merge_locality
void merge_locality(const statet::merge_statet &merge_state)
Definition symex_goto.cpp:665

goto_symext::symex_assign_extract
void symex_assign_extract(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
Perform assignment to an extract irep.
Definition symex_assign.cpp:1032

goto_symext::symex_uninterpreted_function
bool symex_uninterpreted_function(const code_function_call2t &call, const irep_idt &identifier)
Model a call to a "__ESBMC_uninterpreted_*" or "__CPROVER_uninterpreted_*" function as a genuine unin...
Definition symex_function.cpp:429

goto_symext::record_parked_path
virtual void record_parked_path(goto_programt::const_targett, statet::merge_state_listt::iterator)
Hook called when a step parks a merge_statet snapshot for a deferred merge — a GOTO forking off its s...
Definition goto_symex.h:285

goto_symext::handle_conditional
bool handle_conditional(const expr2tc &lhs, const if2t &if_effect, const guard2tc &guard)
Handle conditional expressions (if2t) in the symbolic execution.
Definition symex_assign.cpp:337

goto_symext::va_list_is_started
bool va_list_is_started(const expr2tc &va_list_expr) const
Whether the va_list denoted by this expression is known (or assumed) to have been initialised by va_s...
Definition va_arg.cpp:73

goto_symext::symex_assign_union
void symex_assign_union(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
Perform assignment to a union.
Definition symex_assign.cpp:666

goto_symext::symex_function_call_deref
virtual void symex_function_call_deref(const expr2tc &call)
Handle an indirect function call, to a pointer.
Definition symex_function.cpp:801

goto_symext::symex_assign_if
void symex_assign_if(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
Perform assignment to an "if".
Definition symex_assign.cpp:878

goto_symext::finalize_realloc_result
void finalize_realloc_result(const expr2tc &lhs, const expr2tc &result, const expr2tc &new_array, const guard2tc &guard, const expr2tc &realloc_size, const expr2tc &alloc_fail)
Finalize the result of a realloc operation.
Definition memory_alloc.cpp:496

goto_symext::check_incremental
bool check_incremental(const expr2tc &expr, const std::string &msg)
Perform incremental SMT solving for assert and assume statements.
Definition symex_main.cpp:29

goto_symext::default_replace_dynamic_allocation
void default_replace_dynamic_allocation(expr2tc &expr)
Definition dynamic_allocation.cpp:73

goto_symext::recover_va_list_args
bool recover_va_list_args(const code_printf2t &call, size_t fmt_idx, std::list< expr2tc > &out)
Recover the variadic arguments hidden behind a va_list operand of a v*printf-family call (vprintf/vfp...
Definition io.cpp:19

goto_symext::base_case
bool base_case
Flag as to whether we're doing a k-induction base case.
Definition goto_symex.h:1820

goto_symext::chase_copies
bool chase_copies(expr2tc &expr) const
Rewrite an expression onto the canonical basis of its copy chains: every L2 symbol with an entry in c...
Definition symex_goto.cpp:70

goto_symext::intrinsic_switch_to_monitor
void intrinsic_switch_to_monitor(reachability_treet &art)
Context switch to the monitor thread.
Definition threads.cpp:228

goto_symext::flush_deferred_assumptions
void flush_deferred_assumptions()
Before a claim that needs them, emit every deferred assumption into the target equation.
Definition symex_main.cpp:300

goto_symext::total_claims
unsigned total_claims
Number of assertions executed.
Definition goto_symex.h:1695

goto_symext::intrinsic_spawn_thread
void intrinsic_spawn_thread(const code_function_call2t &call, reachability_treet &art)
Perform spawn_thread; Generates a new thread at a named function.
Definition threads.cpp:131

goto_symext::intrinsic_memcmp
void intrinsic_memcmp(reachability_treet &art, const code_function_call2t &func_call)
Models __ESBMC_memcmp(s1, s2, n): for a constant n with both pointers resolving to concrete primitive...
Definition memory_ops.cpp:1291

goto_symext::unwind_set
std::map< unsigned, BigInt > unwind_set
Unwind bounds, loop number -> max unwinds.
Definition goto_symex.h:1709

goto_symext::no_assertions
bool no_assertions
Flag as to whether we're checking user assertions.
Definition goto_symex.h:1805

goto_symext::unwind_func_set
std::map< std::pair< std::string, unsigned >, BigInt > unwind_func_set
Unwind bounds by function name and per-function loop index (0-indexed), (function name,...
Definition goto_symex.h:1712

goto_symext::determine_fallback_element_type
type2tc determine_fallback_element_type(const sideeffect2t &code, const expr2tc &lhs)
Determine fallback element type for realloc.
Definition memory_alloc.cpp:356

goto_symext::intrinsic_terminate_thread
void intrinsic_terminate_thread(reachability_treet &art)
Perform terminate_thread; Record thread as terminated.
Definition threads.cpp:192

goto_symext::calculate_element_count
expr2tc calculate_element_count(const expr2tc &size_bytes, const expr2tc &elem_size)
Calculate number of elements from byte size.
Definition memory_alloc.cpp:373

goto_symext::argument_value
expr2tc argument_value(const type2tc &arg_type, const expr2tc &rhs, const irep_idt &identifier)
Convert an actual argument to its parameter's type, claiming the call undefined when the two are inco...
Definition symex_function.cpp:187

goto_symext::copy_memory_content
void copy_memory_content(const expr2tc &old_base_array, const expr2tc &new_array, const expr2tc &old_elem_count, const expr2tc &new_elem_count, const type2tc &elem_type, bool old_is_array, const guard2tc &guard)
Copy memory content from old to new allocation.
Definition memory_alloc.cpp:119

goto_symext::track_new_pointer
void track_new_pointer(const expr2tc &ptr_obj, const type2tc &new_type, const guard2tc &guard, const expr2tc &size=expr2tc())
Pointer modelling update function.
Definition memory_alloc.cpp:902

goto_symext::intrinsic_memset
void intrinsic_memset(reachability_treet &art, const code_function_call2t &func_call)
Intrinsic call for C memset function call.
Definition memory_ops.cpp:1652

goto_symext::merge_interval_domain
void merge_interval_domain(const statet::merge_statet &merge_state)
Join a parked path's interval domain into the shared one; a path parked without a snapshot sends the ...
Definition symex_goto.cpp:652

goto_symext::va_list_copy
void va_list_copy(const expr2tc &dst, const expr2tc &src)
va_copy: start dst as src is, reading where src reads next.
Definition va_arg.cpp:177

goto_symext::symex_step
virtual void symex_step(reachability_treet &art)
Symbolically execute one instruction.
Definition symex_main.cpp:349

goto_symext::intrinsic_kill_monitor
void intrinsic_kill_monitor(reachability_treet &art)
Terminate the monitor thread.
Definition threads.cpp:282

goto_symext::get_nondet_counter
virtual unsigned int & get_nondet_counter()=0
Fetch reference to global nondet object counter.

goto_symext::symex_assign_member
void symex_assign_member(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
Perform assignment to a struct.
Definition symex_assign.cpp:820

goto_symext::va_list_mark_started
void va_list_mark_started(const expr2tc &va_list_expr, bool started, const expr2tc &cursor)
Record the started-by-va_start state of the va_list denoted by this expression, and the va_arg index ...
Definition va_arg.cpp:110

goto_symext::symex_sprintf_store
expr2tc symex_sprintf_store(const code_printf2t &call)
Store an unrenamed sprintf or snprintf call's output in its destination buffer, when the format bound...
Definition io.cpp:492

goto_symext::build_goto_symex_classes
friend void build_goto_symex_classes()

goto_symext::conjunct_indext
persistent_map< expr2tc, size_t, irep2_hash > conjunct_indext
Rewritten conjunct -> position of the first conjunct rewriting to it.
Definition goto_symex.h:186

goto_symext::symex_assign_array
void symex_assign_array(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
Perform assignment to an array.
Definition symex_assign.cpp:784

goto_symext::path_guard_decides
tvt::tv_enumt path_guard_decides(const expr2tc &new_guard, bool already_false, bool already_true)
Whether the accumulated path guard already decides a branch condition: TV_TRUE when a conjunct matche...
Definition symex_goto.cpp:144

goto_symext::guard_definitions
persistent_map< irep_idt, expr2tc, irep_id_hash > guard_definitions
Defining condition of each L2 guard symbol generation, i.e.
Definition goto_symex.h:1648

goto_symext::record_property_verdict
void record_property_verdict(const std::string &msg, property_verdictt verdict, const std::string &note="")
Record a verdict for the claim being symbolically executed.
Definition symex_main.cpp:148

goto_symext::valid_ptr_arr_name
irep_idt valid_ptr_arr_name
Symbol names for modelling arrays.
Definition goto_symex.h:1735

goto_symext::bounded_loop_truncations
unsigned bounded_loop_truncations
Loops cut off at the unwinding bound with no unwinding assertion to flag it, i.e.
Definition goto_symex.h:1705

goto_symext::symex_free
void symex_free(const expr2tc &expr)
Symbolic implementation of free.
Definition memory_alloc.cpp:953

goto_symext::symex_witness_function_return
void symex_witness_function_return(expr2tc ret_val, const irep_idt &call_line)
Definition witness.cpp:31

goto_symext::simplify_python_builtins
void simplify_python_builtins(expr2tc &expr)
Definition python_builtins.cpp:145

goto_symext::get_unwind
bool get_unwind(const symex_targett::sourcet &source, const BigInt &unwind)
Test whether unwinding bound has been exceeded.
Definition symex_goto.cpp:871

goto_symext::run_next_function_ptr_target
bool run_next_function_ptr_target(bool first)
Setup next function in a chain of func ptr calls.
Definition symex_function.cpp:992

goto_symext::validate_witness
bool validate_witness
Cached from –validate-violation-witness; checked on every branch/intrinsic.
Definition goto_symex.h:1829

goto_symext::symex_assign_structure
void symex_assign_structure(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
Perform assignment to a structure.
Definition symex_assign.cpp:609

goto_symext::va_started
std::unordered_map< renaming::level2t::name_record, bool, renaming::level2t::name_rec_hash > va_started
Level-1 identities (base name, activation, thread) of va_list objects initialised by va_start,...
Definition goto_symex.h:1773

goto_symext::merge_value_sets
void merge_value_sets(const statet::merge_statet &merge_state)
Merge pointer tracking value sets in a phi function.
Definition symex_goto.cpp:688

goto_symext::replace_valid_object
void replace_valid_object(expr2tc &expr)
Decide VALID_OBJECT / DEALLOCATED_OBJ against the object the pointer names.
Definition symex_valid_object.cpp:173

goto_symext::k_induction
bool k_induction
Flag as to whether we're doing a k-induction.
Definition goto_symex.h:1817

goto_symext::assume
virtual void assume(const expr2tc &assumption)
Perform an assumption.
Definition symex_main.cpp:256

goto_symext::symex_decl
void symex_decl(const expr2tc &code)
Interpret an DECL instruction.
Definition symex_other.cpp:72

goto_symext::symex_cpp_delete
void symex_cpp_delete(const expr2tc &code)
Symbolic implementation of c++'s delete.
Definition cpp_memory.cpp:82

goto_symext::prefix_index
conjunct_indext prefix_index(const guard2tc &guard)
The conjunct index of guard, which must not be true.
Definition symex_goto.cpp:167

goto_symext::intrinsic_get_thread_id
void intrinsic_get_thread_id(const code_function_call2t &call, reachability_treet &art)
Perform get_thread_id; return the current thread identifier.
Definition threads.cpp:58

goto_symext::depth_limit
unsigned long depth_limit
Depth limit, as given by the –depth option.
Definition goto_symex.h:1791

goto_symext::no_return_value_opt
bool no_return_value_opt
Disable return value optimization.
Definition goto_symex.h:1783

goto_symext::handle_sideeffect
void handle_sideeffect(const expr2tc &lhs, const sideeffect2t &effect, const guard2tc &guard)
Handle side effects in the symbolic execution.
Definition symex_assign.cpp:267

goto_symext::memory_leak_check
bool memory_leak_check
Flag as to whether we're performing memory leak checks.
Definition goto_symex.h:1798

goto_symext::replace_dynamic_allocation
void replace_dynamic_allocation(expr2tc &expr)
Replace ireps regarding dynamic allocations with code.
Definition symex_valid_object.cpp:219

goto_symext::symex_va_arg
void symex_va_arg(const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)
Symbolic implementation of va_arg.
Definition va_arg.cpp:195

goto_symext::analyze_args
virtual void analyze_args(const expr2tc &expr)=0
Analyze the shared varables in a function call, this is because an argumemt may be renamed to constan...

goto_symext::symex_end_of_function
void symex_end_of_function()
End a functions interpretation.
Definition symex_function.cpp:1141

goto_symext::va_list_frame
goto_symex_statet::framet & va_list_frame(const expr2tc &va_list_expr)
The frame whose variadic arguments a va_list reads: the activation that declared it,...
Definition va_arg.cpp:168

goto_symext::intrinsic_builtin_object_size
void intrinsic_builtin_object_size(const code_function_call2t &func_call, reachability_treet &art)
Implements GCC's __builtin_object_size intrinsic for object size determination.
Definition object_size.cpp:99

goto_symext::claim
virtual void claim(const expr2tc &expr, const std::string &msg)
Perform an assertion.
Definition symex_main.cpp:68

goto_symext::target
std::shared_ptr< symex_targett > target
Target listening to the execution trace.
Definition goto_symex.h:1728

goto_symext::is_python_gc_object
bool is_python_gc_object(const symbolt *base) const
Whether base is a user-defined Python class instance that follows garbage-collected lifetime semantic...
Definition symex_function.cpp:1053

goto_symext::dynamic_object_sizes
std::unordered_map< irep_idt, expr2tc > dynamic_object_sizes
The renamed byte size each heap object was allocated with, by symbol.
Definition goto_symex.h:1690

goto_symext::create_result_pointer
expr2tc create_result_pointer(const expr2tc &new_array, const type2tc &lhs_type)
Create result pointer from newly allocated array.
Definition memory_alloc.cpp:418

goto_symext::symex_witness_function_enter
bool symex_witness_function_enter(const irep_idt &call_line)
Definition witness.cpp:70

goto_symext::va_list_cursor_symbol
expr2tc va_list_cursor_symbol(const renaming::level2t::name_record &rec)
The l1 symbol holding the va_arg index a local va_list reads next.
Definition va_arg.cpp:80

goto_symext::merge_gotos
void merge_gotos()
Merge converging states into current state.
Definition symex_goto.cpp:569

goto_symext::string_length
expr2tc string_length(const expr2tc &ptr, size_t &max_len)
The characters a s conversion prints for the unrenamed char pointer ptr, adding its largest value to ...
Definition io.cpp:338

goto_symext::intrinsic_set_thread_data
void intrinsic_set_thread_data(const code_function_call2t &call, reachability_treet &art)
Perform set_thread_state; store thread startup information.
Definition threads.cpp:74

goto_symext::dyn_info_arr_name
irep_idt dyn_info_arr_name
Definition goto_symex.h:1735

goto_symext::run_builtin
bool run_builtin(const code_function_call2t &call, const std::string &symname)
Run a builtin, something prefixed with __builtin.
Definition run_builtin.cpp:201

goto_symext::options
optionst & options
Options we're working with.
Definition goto_symex.h:1621

goto_symext::symex_assume
void symex_assume()
Interpret an ASSUME instruction.
Definition symex_main.cpp:561

goto_symext::copy_definitions
persistent_map< irep_idt, expr2tc, irep_id_hash > copy_definitions
Copy chains between L2 symbol generations: lhs generation -> the stable value it was unconditionally ...
Definition goto_symex.h:1663

goto_symext::loop_bound_exceeded
void loop_bound_exceeded(const expr2tc &guard)
Encode unwinding assertions and assumption.
Definition symex_goto.cpp:838

goto_symext::remaining_claims
unsigned remaining_claims
Number of assertions remaining to be discharged.
Definition goto_symex.h:1697

goto_symext::stack_limit
unsigned long stack_limit
Limit size, in bits, for a single stack frame.
Definition goto_symex.h:1785

goto_symext::symex_assign_bitfield
void symex_assign_bitfield(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
This method is used when we need to assign a value to a struct bitfield which is obtained via applyin...
Definition symex_assign.cpp:1093

goto_symext::intrinsic_init_thread_local
void intrinsic_init_thread_local(reachability_treet &art)
Perform init_thread_local; seeds each __thread-qualified global to its static initializer in the acti...
Definition threads.cpp:199

goto_symext::symex_assign_rec
void symex_assign_rec(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc full_rhs, guard2tc &guard, const bool hidden)
Recursively perform symex assign.
Definition symex_assign.cpp:484

goto_symext::no_simplify
bool no_simplify
Flag as to whether we're not simplifying exprs.
Definition goto_symex.h:1808

goto_symext::break_insn
unsigned long break_insn
Instruction number we are to break at – that is, trap, to the debugger.
Definition goto_symex.h:1795

goto_symext::symex_cpp_new
void symex_cpp_new(const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)
Symbolic implementation of c++'s new.
Definition cpp_memory.cpp:13

goto_symext::intrinsic_memmove
void intrinsic_memmove(reachability_treet &art, const code_function_call2t &func_call)
Models __ESBMC_memmove.
Definition memory_ops.cpp:1193

goto_symext::stack_checks_enabled
bool stack_checks_enabled() const
True when either stack limit is on.
Definition goto_symex.h:335

goto_symext::memcpy_finish
void memcpy_finish(const code_function_call2t &func_call, const expr2tc &dst_arg, const expr2tc &src_arg, const expr2tc &n_arg)
The NULL checks and return-value assignment shared by both of intrinsic_memcpy_impl's paths.
Definition memory_ops.cpp:859

goto_symext::symex_printf
virtual void symex_printf(const expr2tc &lhs, expr2tc &code)
Symbolic implementation of printf.
Definition io.cpp:650

goto_symext::is_assume_false
bool is_assume_false(const expr2tc &assumption)
Incrementally check the assumption.
Definition symex_main.cpp:192

goto_symext::record_copy_definition
void record_copy_definition(const expr2tc &renamed_lhs, const expr2tc &rhs)
Record a copy chain for chase_copies after an unconditional assignment, when the rhs is a stable valu...
Definition symex_goto.cpp:93

goto_symext::intrinsic_switch_to
void intrinsic_switch_to(const code_function_call2t &c, reachability_treet &art)
Perform switch_to; switches control to explicit thread ID.
Definition threads.cpp:24

goto_symext::pop_frame
void pop_frame()
Pop a stack frame.
Definition symex_function.cpp:1086

goto_symext::guard_prefix_index
persistent_map< expr2tc, conjunct_indext, irep2_hash > guard_prefix_index
prefix_index's result per and-chain node of a path guard.
Definition goto_symex.h:1672

goto_symext::dereference
void dereference(expr2tc &expr, dereferencet::modet mode, bool block_assertions=false)
Dereference an expression.
Definition symex_dereference.cpp:219

goto_symext::deferred_assumptions
std::vector< deferred_assumptiont > deferred_assumptions
Assumptions defer_assumption() holds back, in program order.
Definition goto_symex.h:1682

goto_symext::va_list_owner_records
std::vector< renaming::level2t::name_record > va_list_owner_records(const expr2tc &va_list_expr) const
The records va_list_frame looks for: a va_copy destination's are those of the va_list it was copied f...
Definition va_arg.cpp:156

goto_symext::cur_state
goto_symex_statet * cur_state
Target thread we're currently operating upon.
Definition goto_symex.h:1730

goto_symext::guard_identifier
expr2tc guard_identifier()
Return identifier for goto guards.
Definition goto_symex.h:136

goto_symext::copy_single_element
void copy_single_element(const expr2tc &old_base_array, const expr2tc &new_array, const expr2tc &idx, const type2tc &elem_type, const type2tc &new_elem_type, bool old_is_array, const guard2tc &guard)
Copy a single element between old and new arrays.
Definition memory_alloc.cpp:188

goto_symext::value_set_objects
std::vector< expr2tc > value_set_objects(const expr2tc &ptr, bool &complete)
The objects the value set says ptr may address.
Definition symex_valid_object.cpp:26

goto_symext::create_dynamic_memory_symbol
expr2tc create_dynamic_memory_symbol(const type2tc &elem_type, const expr2tc &size_expr, const std::string &name_prefix)
Create a new dynamic memory symbol.
Definition memory_alloc.cpp:89

goto_symext::art1
reachability_treet * art1
Reachability tree we're working with.
Definition goto_symex.h:1707

goto_symext::total_stack_limit
unsigned long total_stack_limit
Limit size, in bits, for every live stack frame taken together.
Definition goto_symex.h:1789

goto_symext::symex_dereference_statet
friend class symex_dereference_statet
Definition goto_symex.h:92

goto_symext::defer_assumption
virtual void defer_assumption(const expr2tc &assumption)
Hold back the assume that ends a path at a Python assert (#8242).
Definition symex_main.cpp:279

goto_symext::get_symex_result
goto_symext::symex_resultt get_symex_result()
Create a symex result for this run.
Definition symex_main.cpp:312

goto_symext::intrinsic_get_thread_data
void intrinsic_get_thread_data(const code_function_call2t &call, reachability_treet &art)
Perform get_thread_data; get thread startup information.
Definition threads.cpp:100

goto_symext::record_guard_definition
void record_guard_definition(const expr2tc &guard_expr, const expr2tc &rhs)
Remember a guard generation's defining condition for path_guard_decides.
Definition symex_goto.cpp:125

goto_symext::symex_assert
void symex_assert()
Interpret an ASSERT instruction.
Definition symex_main.cpp:594

goto_symext::add_memory_leak_checks
void add_memory_leak_checks()
Perform accounting checks / assertions at end of a program run.
Definition symex_main.cpp:1501

goto_symext::rewrite_conjunct
expr2tc rewrite_conjunct(const expr2tc &conjunct)
A path-guard conjunct rewritten onto the canonical basis path_guard_decides compares on.
Definition symex_goto.cpp:202

goto_symext::symex_assign_array_structure
void symex_assign_array_structure(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
Perform assignment to an array literal.
Definition symex_assign.cpp:634

goto_symext::assume_printf_length
void assume_printf_length(const expr2tc &retval, const expr2tc &len)
Assume a printf-family call's return value equals the length of its output, when both are known.
Definition io.cpp:583

goto_symext::new_context
contextt & new_context
Context we're working with.
Definition goto_symex.h:1724

goto_symext::symex_assign_concat
void symex_assign_concat(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
Assign through a 'concat' operation.
Definition symex_assign.cpp:957

goto_symext::copy_old_objects
void copy_old_objects(const std::list< dereference_callbackt::internal_item > &old_objects, const expr2tc &new_array, const expr2tc &new_elem_count, const type2tc &elem_type, const guard2tc &guard)
Copy each object a reallocated pointer may point to into the new allocation, guarded by the pointer p...
Definition memory_alloc.cpp:324

goto_symext::symex_other
void symex_other(const expr2tc &code)
Interpret an OTHER instruction.
Definition symex_other.cpp:9

goto_symext::handle_realloc_zero_size
bool handle_realloc_zero_size(const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard, const expr2tc &realloc_size)
Handle realloc with zero size parameter.
Definition memory_alloc.cpp:280

goto_symext::branch_decision_guard
expr2tc branch_decision_guard(const expr2tc &guard) const
The guard a branch decision is read from.
Definition symex_assign.cpp:257

goto_symext::no_reachable_memleak
bool no_reachable_memleak
Flag as to whether we're pruning the objects from the memory leak check that are still reachable via ...
Definition goto_symex.h:1802

goto_symext::terminate_handler
bool terminate_handler()
Call terminate function handler when needed.

goto_symext::unexpected_handler
bool unexpected_handler()
Call unexpected function handler when needed.

goto_symext::ns
const namespacet & ns
Namespace we're working in.
Definition goto_symex.h:1722

goto_symext::do_simplify
virtual void do_simplify(expr2tc &expr)
Perform simplification on an expression.
Definition symex_assign.cpp:251

goto_symext::run_intrinsic
void run_intrinsic(const code_function_call2t &call, reachability_treet &art, const std::string &symname)
Run an intrinsic, something prefixed with __ESBMC.
Definition symex_main.cpp:643

goto_symext::interval_domain_state
std::optional< interval_domaint > interval_domain_state
Online interval domain: guard pruning is on by default (disable with –no-interval-symex-guard); asser...
Definition goto_symex.h:1720

goto_symext::guard_identifier_s
irep_idt guard_identifier_s
Symbol prefix for guards.
Definition goto_symex.h:1628

goto_symext::get_unwind_recursion
bool get_unwind_recursion(const irep_idt &identifier, BigInt unwind)
Discover whether recursion bound has been exceeded.
Definition symex_function.cpp:144

goto_symext::symex_alloca
expr2tc symex_alloca(const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)
Symbolic implementation of alloca.
Definition memory_alloc.cpp:81

goto_symext::symex_bounded_math
void symex_bounded_math(const code_function_call2t &call, const std::string &function)
_builtin_bounded<function>(x, exact): the bounded result of a transcendental function,...
Definition bounded_math.cpp:24

goto_symext::reject_untyped_isinstance
void reject_untyped_isinstance(const expr2tc &value)
Definition python_builtins.cpp:115

goto_symext::memcpy_symbolic_length
bool memcpy_symbolic_length(const expr2tc &dst_arg, const expr2tc &src_arg, const expr2tc &n_arg)
Models a memcpy/memmove whose length is not a constant, the case intrinsic_memcpy_impl otherwise defe...
Definition memory_ops.cpp:889

goto_symext::intrinsic_really_atomic_begin
void intrinsic_really_atomic_begin(reachability_treet &art)
Really atomic start/end - atomic blocks that just disable ileaves.
Definition threads.cpp:218

goto_symext::memcmp_resolve_operand
bool memcmp_resolve_operand(const expr2tc &ptr, unsigned long number_of_bytes, expr2tc &object, uint64_t &offset, uint64_t &avail_bytes, bool rename_object=true)
Helper for intrinsic_memcmp: resolve ptr to a single concrete primitive object with a constant offset...
Definition memory_ops.cpp:1207

goto_symext::key_intrinsic_pointer_reads
void key_intrinsic_pointer_reads(const code_function_call2t &call, const irep_idt &id)
Key the reads the memcpy/memmove/memcmp/memchr intrinsics perform, which symex carries out internally...
Definition symex_main.cpp:322

goto_symext::symex_assign_byte_extract
void symex_assign_byte_extract(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)
Perform assignment to a byte extract.
Definition symex_assign.cpp:907

goto_symext::intrinsic_memcpy
void intrinsic_memcpy(reachability_treet &art, const code_function_call2t &func_call)
Intrinsic call for C memcpy function call.
Definition memory_ops.cpp:1186

goto_symext::symex_realloc
void symex_realloc(const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)
Implementation of realloc.
Definition memory_alloc.cpp:205

goto_symext::symex_witness_branching
void symex_witness_branching(const expr2tc &old_guard, const expr2tc &new_guard, bool forward, bool &new_guard_true, bool &new_guard_false, const goto_programt::instructiont &instruction)
Definition witness.cpp:102

goto_symext::argument_assignments
unsigned int argument_assignments(const irep_idt &function_identifier, const code_type2t &function_type, const std::vector< expr2tc > &arguments)
Join up function arguments.
Definition symex_function.cpp:244

goto_symext::simplified_claims
unsigned simplified_claims
Number of assertions that were trivially verified.
Definition goto_symex.h:1699

goto_symext::symex_return
void symex_return(const expr2tc &code)
Perform interpretation of RETURN instruction.
Definition symex_function.cpp:1179

goto_symext::materialise_old_snapshot
expr2tc materialise_old_snapshot(const expr2tc &value, const guard2tc &guard)
Give a value storage of its own, for __ESBMC_old.
Definition symex_assign.cpp:370

goto_symext::first_loop
unsigned first_loop
Loop numbers.
Definition goto_symex.h:1693

goto_symext::intrinsic_switch_from
void intrinsic_switch_from(reachability_treet &arg)
Yield, always switching away from this thread.
Definition threads.cpp:43

goto_symext::intrinsic_yield
void intrinsic_yield(reachability_treet &arg)
Perform yield; forces a context switch point.
Definition threads.cpp:17

goto_symext::named_object
expr2tc named_object(const expr2tc &base) const
base if it is a named object, nil otherwise.
Definition symex_valid_object.cpp:58

goto_symext::symex_mem_inf
expr2tc symex_mem_inf(const expr2tc &lhs, const type2tc &base_type, const guard2tc &guard)
Wrapper around for infinite array allocation.
Definition memory_alloc.cpp:527

goto_symext::assume_printf_range
void assume_printf_range(const expr2tc &retval, const BigInt &lo, const BigInt &hi, bool may_fail)
Assume a printf-family call's return value lies in [lo, hi], or is -1 when may_fail.
Definition io.cpp:591

goto_symext::model_allocation_failure
expr2tc model_allocation_failure(const expr2tc &result, const expr2tc &old_ptr, const guard2tc &guard, const expr2tc &over_cap, expr2tc &alloc_fail)
Model allocation failure behavior for realloc.
Definition memory_alloc.cpp:434

goto_symext::calculate_old_element_count
expr2tc calculate_old_element_count(const expr2tc &old_base_array, const type2tc &elem_type, bool old_is_array)
Calculate the number of elements in the old memory object.
Definition memory_alloc.cpp:389

goto_symext::goto_symext
goto_symext(const namespacet &_ns, contextt &_new_context, const goto_functionst &goto_functions, std::shared_ptr< symex_targett > _target, optionst &opts)
Default constructor.
Definition symex_assign.cpp:32

goto_symext::partial_loops
bool partial_loops
Flag as to whether we're not enabling partial loops.
Definition goto_symex.h:1814

goto_symext::offer_malloc_zero_null
void offer_malloc_zero_null(const expr2tc &size, expr2tc &rhs, guard2tc &alloc_guard)
Offer both outcomes C17 7.22.3p1 permits for a zero-sized malloc, under –malloc-zero-is-null.
Definition memory_alloc.cpp:599

goto_symext::assume_uf_congruence
void assume_uf_congruence(const irep_idt &identifier, const irep_idt &name, const std::vector< expr2tc > &arguments, const expr2tc &result, const type2tc &ret_type)
Assume equal arguments imply an equal result against every earlier application of identifier,...
Definition symex_function.cpp:392

goto_symext::inductive_step
bool inductive_step
Flag as to whether we're doing a k-induction inductive step.
Definition goto_symex.h:1826

goto_symext::symex_function_call
void symex_function_call(const expr2tc &call)
Perform function call.
Definition symex_function.cpp:376

goto_symext::printf_return_length
expr2tc printf_return_length(const expr2tc &lhs, const code_printf2t &call, size_t fmt_idx)
Store an unrenamed sprintf-family call's output and return the length that call returns: the stored l...
Definition io.cpp:553

goto_symext::claim_nonnull_operand
void claim_nonnull_operand(const expr2tc &ptr, const expr2tc &n, const std::string &func)
Claims ptr is not NULL unless n is zero.
Definition memory_ops.cpp:1276

goto_symext::dynamic_memory
std::list< allocated_obj > dynamic_memory
List of all allocated objects.
Definition goto_symex.h:1739

goto_symext::symex_mem
expr2tc symex_mem(const bool is_malloc, const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)
Wrapper around for alloca and malloc.
Definition memory_alloc.cpp:665

goto_symext::assertion_message
static std::string assertion_message(const namespacet &ns, const goto_programt::instructiont &i)
The message of the claim an ASSERT instruction raises for itself, as opposed to a check symex raises ...
Definition symex_main.cpp:584

goto_symext::make_return_assignment
bool make_return_assignment(expr2tc &assign, const expr2tc &code_return)
Create assignment for return statement.
Definition symex_function.cpp:1146

goto_symext::va_copied_from
std::unordered_map< renaming::level2t::name_record, renaming::level2t::name_record, renaming::level2t::name_rec_hash > va_copied_from
For each va_copy destination, the local va_list whose frame's variadic arguments it reads,...
Definition goto_symex.h:1780

goto_symext::assertion
virtual void assertion(const expr2tc &assertion, const std::string &msg)
Perform an assertion.
Definition symex_main.cpp:171

goto_symext::symex_goto
virtual void symex_goto(const expr2tc &old_guard)
Perform GOTO jump using current instruction.
Definition symex_goto.cpp:236

goto_symext::intrinsic_memcpy_impl
void intrinsic_memcpy_impl(reachability_treet &art, const code_function_call2t &func_call, const std::string &bump_name)
Shared core for intrinsic_memcpy / intrinsic_memmove; bump_name is the C fallback (__memcpy_impl / __...
Definition memory_ops.cpp:949

goto_symext::operator=
goto_symext & operator=(const goto_symext &sym)
Definition symex_assign.cpp:194

goto_symext::printf_output_length
expr2tc printf_output_length(const code_printf2t &call, size_t fmt_idx, size_t &max_len)
The length of an unrenamed printf-family call's output whose constant format holds only text and d,...
Definition io.cpp:375

goto_symext::symex_dead
void symex_dead(const expr2tc &code)
Interpret an DEAD instruction.
Definition symex_other.cpp:137

goto_symext::claim_not_code
void claim_not_code(const expr2tc &guard)
Claim that a memory builtin's operand, on the path guard selects, is not a code object; nothing under...
Definition memory_ops.cpp:819

goto_symext::replace_nondet
void replace_nondet(expr2tc &expr)
Replace nondet func calls with nondeterminism.
Definition symex_assign.cpp:1146

goto_symext::intrinsic_memchr
void intrinsic_memchr(reachability_treet &art, const code_function_call2t &func_call)
Intrinsic call for C memchr function call.
Definition memory_ops.cpp:1451

goto_symext::claim_valid_operand
void claim_valid_operand(const expr2tc &ptr, const expr2tc &n, const std::string &func)
An INTERNAL dereference drops an unknown or invalid target without a claim, so the memory builtins cl...
Definition memory_ops.cpp:830

goto_symext::symex_malloc
expr2tc symex_malloc(const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)
Symbolic implementation of malloc.
Definition memory_alloc.cpp:73

goto_symext::bmct
friend class bmct
Definition goto_symex.h:93

goto_symext::phi_function
void phi_function(const statet::merge_statet &merge_state)
Join a previous jump's merge snapshot into the active thread state.
Definition symex_goto.cpp:744

goto_symext::volatile_check
void volatile_check(expr2tc &expr)
Definition misc.cpp:73

goto_symext::sprintf_output
expr2tc sprintf_output(const code_printf2t &call, size_t fmt_idx, const type2tc &char_type, std::vector< expr2tc > &chars)
The output of an unrenamed sprintf or snprintf call: its characters before the NUL in chars,...
Definition io.cpp:434

goto_symext::symex_assign
virtual void symex_assign(const expr2tc &code, const bool hidden=false, const guard2tc &guard=guard2tc())
Make symbolic assignment.
Definition symex_assign.cpp:389

goto_symext::no_unwinding_assertions
bool no_unwinding_assertions
Flag as to whether we're inserting unwinding assertions.
Definition goto_symex.h:1811

goto_symext::assume_loop_continues
void assume_loop_continues(const goto_programt::instructiont &instruction, const expr2tc &guard, bool forward, bool always_jumps)
Narrow the online interval domain by the condition under which a loop GOTO's continuing path proceeds...
Definition symex_goto.cpp:631

goto_symext::note_bounded_loop_truncation
virtual void note_bounded_loop_truncation()
Records that a loop was cut off at the unwinding bound with nothing to flag it.
Definition goto_symex.h:522

goto_symext::va_list_start
void va_list_start(const expr2tc &va_list_expr)
va_start: the va_list reads this frame's first variadic argument next.
Definition va_arg.cpp:143

goto_symext::va_list_l1_record
std::optional< renaming::level2t::name_record > va_list_l1_record(const expr2tc &va_list_expr) const
Resolve a va_list expression to the l1 identity record of the local variable backing it; nullopt when...
Definition va_arg.cpp:42

goto_symext::symex_function_call_code
virtual void symex_function_call_code(const expr2tc &call)
Handle a call to a statically-known function: checks recursion bounds, sets up the new frame,...
Definition symex_function.cpp:534

guard2tc
Path-condition guard container.
Definition irep2_guard.h:32

if2t
If-then-else expression.
Definition irep2_expr.h:842

inductive_step_disabled_exceptiont::inductive_step_disabled_exceptiont
inductive_step_disabled_exceptiont(std::string r)
Definition goto_symex.h:29

inductive_step_disabled_exceptiont::reason
std::string reason
Definition goto_symex.h:33

irep_idt
Definition irep_idt.h:12

namespacet
Definition namespace.h:10

optionst
Definition options.h:11

persistent_map
Persistent (structurally shared) map with O(1) copy.
Definition persistent_map.h:31

printf_formattert
Definition printf_formatter.h:12

reachability_treet
Class to explore states reachable through threading.
Definition reachability_tree.h:65

renaming::level2t::name_record
Definition renaming.h:147

sideeffect2t
Irep for various side effects.
Definition irep2_expr.h:1906

symbolt
Definition symbol.h:12

symex_dereference_statet::dump_internal_state
void dump_internal_state(const std::list< struct internal_item > &data) override
Definition symex_dereference.cpp:148

symex_dereference_statet::get_value_set
void get_value_set(const expr2tc &expr, value_setst::valuest &value_set) override
Fetch the set of values that the given pointer variable can point at.
Definition symex_dereference.cpp:57

symex_dereference_statet::symex_dereference_statet
symex_dereference_statet(goto_symext &_goto_symex, goto_symext::statet &_state)
Definition goto_symex.h:1850

symex_dereference_statet::state
goto_symext::statet & state
Definition goto_symex.h:1859

symex_dereference_statet::dereference_assume
void dereference_assume(const guard2tc &guard) override
Definition symex_dereference.cpp:19

symex_dereference_statet::dereference_failure
void dereference_failure(const std::string &property, const std::string &msg, const guard2tc &guard) override
Encode a dereference failure assertion.
Definition symex_dereference.cpp:8

symex_dereference_statet::has_failed_symbol
bool has_failed_symbol(const expr2tc &expr, const symbolt *&symbol) override
Check whether a failed symbol already exists for the given symbol.
Definition symex_dereference.cpp:27

symex_dereference_statet::is_live_variable
bool is_live_variable(const expr2tc &sym) override
Determine whether variable is "alive".
Definition symex_dereference.cpp:155

symex_dereference_statet::rename
void rename(expr2tc &expr) override
Rename the given expression into the callback's current execution context.
Definition symex_dereference.cpp:143

symex_dereference_statet::goto_symex
goto_symext & goto_symex
Definition goto_symex.h:1858

tvt::tv_enumt
tv_enumt
Definition threeval.h:13

value_setst::valuest
std::list< expr2tc > valuest
Definition value_sets.h:15

value
Definition toml.hpp:1531

dereference.h
The dereferencing code's purpose is to take a symbol with pointer type that is being dereferenced,...

goto_functions.h

goto_symex_state.h

i2string.h

interval_domain.h
Interval Domain.

irep2.h
Classes and definitions for non-stringy internal representation.

type2tc
irep_container< type2t > type2tc
Definition irep2.h:430

expr2tc
irep_container< expr2t > expr2tc
Definition irep2.h:431

symbol_renaming_level::level1
@ level1
Definition irep2_expr.h:56

id2string
const std::string & id2string(const irep_idt &d)
Definition irep.h:1405

goto_symex_utils
Definition goto_symex.h:1881

goto_symex_utils::gen_byte_memcpy
expr2tc gen_byte_memcpy(const expr2tc &src, const expr2tc &dst, const size_t num_of_bytes, const size_t src_offset, const size_t dst_offset)
Computes the equivalent object value when considering a memcpy operation on it.
Definition memory_ops.cpp:435

goto_symex_utils::is_alloca_return_value_name
bool is_alloca_return_value_name(const std::string &name)
Returns true iff name is the goto-program return-value temp for an alloca / __builtin_alloca call,...
Definition symex_function.cpp:19

std
Definition exception.cpp:51

tok_kind::identifier
@ identifier
Definition nested_func_transform.cpp:62

options.h

property_verdictt
property_verdictt
Outcome of checking one property.
Definition property_verdict.h:25

std_types.h

bool
#define bool
Definition stdbool.h:9

dereferencet::modet
The different ways in which a pointer may be accessed.
Definition dereference.h:202

function
Definition module.h:12

goto_symext::deferred_assumptiont
Definition goto_symex.h:1675

goto_symext::deferred_assumptiont::loop_number
unsigned loop_number
Definition goto_symex.h:1679

goto_symext::deferred_assumptiont::source
symex_targett::sourcet source
Definition goto_symex.h:1678

goto_symext::deferred_assumptiont::cond
expr2tc cond
Definition goto_symex.h:1677

goto_symext::deferred_assumptiont::guard
expr2tc guard
Definition goto_symex.h:1676

renaming::level2t::name_rec_hash
Definition renaming.h:230

symex_targett::sourcet
Definition symex_target.h:31

symex_target.h

threeval.h