cprover
symex_target_equationt Class Reference

#include <symex_target_equation.h>

Inheritance diagram for symex_target_equationt:
[legend]
Collaboration diagram for symex_target_equationt:
[legend]

Classes

class  SSA_stept
 

Public Types

typedef std::list< SSA_steptSSA_stepst
 
- Public Types inherited from symex_targett
enum  assignment_typet {
  assignment_typet::STATE, assignment_typet::HIDDEN, assignment_typet::VISIBLE_ACTUAL_PARAMETER, assignment_typet::HIDDEN_ACTUAL_PARAMETER,
  assignment_typet::PHI, assignment_typet::GUARD
}
 

Public Member Functions

virtual ~symex_target_equationt ()=default
 
virtual void shared_read (const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
 read from a shared variable More...
 
virtual void shared_write (const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
 write to a sharedvariable More...
 
virtual void assignment (const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)
 write to a variable More...
 
virtual void decl (const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)
 declare a fresh variable More...
 
virtual void dead (const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
 declare a fresh variable More...
 
virtual void function_call (const exprt &guard, const irep_idt &identifier, const sourcet &source)
 just record a location More...
 
virtual void function_return (const exprt &guard, const irep_idt &identifier, const sourcet &source)
 just record a location More...
 
virtual void location (const exprt &guard, const sourcet &source)
 just record a location More...
 
virtual void output (const exprt &guard, const sourcet &source, const irep_idt &fmt, const std::list< exprt > &args)
 just record output More...
 
virtual void output_fmt (const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
 just record formatted output More...
 
virtual void input (const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
 just record input More...
 
virtual void assumption (const exprt &guard, const exprt &cond, const sourcet &source)
 record an assumption More...
 
virtual void assertion (const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
 record an assertion More...
 
virtual void goto_instruction (const exprt &guard, const exprt &cond, const sourcet &source)
 record a goto instruction More...
 
virtual void constraint (const exprt &cond, const std::string &msg, const sourcet &source)
 record a constraint More...
 
virtual void spawn (const exprt &guard, const sourcet &source)
 spawn a new thread More...
 
virtual void memory_barrier (const exprt &guard, const sourcet &source)
 
virtual void atomic_begin (const exprt &guard, unsigned atomic_section_id, const sourcet &source)
 start an atomic section More...
 
virtual void atomic_end (const exprt &guard, unsigned atomic_section_id, const sourcet &source)
 end an atomic section More...
 
void convert (prop_convt &prop_conv)
 
void convert_assignments (decision_proceduret &decision_procedure) const
 converts assignments More...
 
void convert_decls (prop_convt &prop_conv) const
 converts declarations More...
 
void convert_assumptions (prop_convt &prop_conv)
 converts assumptions More...
 
void convert_assertions (prop_convt &prop_conv)
 converts assertions More...
 
void convert_constraints (decision_proceduret &decision_procedure) const
 converts constraints More...
 
void convert_goto_instructions (prop_convt &prop_conv)
 converts goto instructions More...
 
void convert_guards (prop_convt &prop_conv)
 converts guards More...
 
void convert_io (decision_proceduret &decision_procedure)
 converts I/O More...
 
exprt make_expression () const
 
std::size_t count_assertions () const
 
std::size_t count_ignored_SSA_steps () const
 
SSA_stepst::iterator get_SSA_step (std::size_t s)
 
void output (std::ostream &out, const namespacet &ns) const
 
void clear ()
 
bool has_threads () const
 
- Public Member Functions inherited from symex_targett
 symex_targett ()
 
virtual ~symex_targett ()
 

Public Attributes

SSA_stepst SSA_steps
 

Protected Member Functions

void merge_ireps (SSA_stept &SSA_step)
 

Protected Attributes

merge_irept merge_irep
 

Detailed Description

Definition at line 32 of file symex_target_equation.h.

Member Typedef Documentation

◆ SSA_stepst

Definition at line 289 of file symex_target_equation.h.

Constructor & Destructor Documentation

◆ ~symex_target_equationt()

virtual symex_target_equationt::~symex_target_equationt ( )
virtualdefault

Member Function Documentation

◆ assertion()

void symex_target_equationt::assertion ( const exprt guard,
const exprt cond,
const std::string &  msg,
const sourcet source 
)
virtual

◆ assignment()

◆ assumption()

◆ atomic_begin()

void symex_target_equationt::atomic_begin ( const exprt guard,
unsigned  atomic_section_id,
const sourcet source 
)
virtual

◆ atomic_end()

void symex_target_equationt::atomic_end ( const exprt guard,
unsigned  atomic_section_id,
const sourcet source 
)
virtual

◆ clear()

void symex_target_equationt::clear ( void  )
inline

Definition at line 305 of file symex_target_equation.h.

References SSA_steps.

◆ constraint()

◆ convert()

◆ convert_assertions()

void symex_target_equationt::convert_assertions ( prop_convt prop_conv)

◆ convert_assignments()

void symex_target_equationt::convert_assignments ( decision_proceduret decision_procedure) const

converts assignments

parameters: decision procedure
Returns
-

Definition at line 400 of file symex_target_equation.cpp.

References messaget::conditional_output(), messaget::debug(), messaget::eom(), decision_proceduret::set_to_true(), and SSA_steps.

Referenced by convert().

◆ convert_assumptions()

void symex_target_equationt::convert_assumptions ( prop_convt prop_conv)

◆ convert_constraints()

void symex_target_equationt::convert_constraints ( decision_proceduret decision_procedure) const

converts constraints

parameters: decision procedure
Returns
-

Definition at line 553 of file symex_target_equation.cpp.

References messaget::conditional_output(), messaget::debug(), messaget::eom(), decision_proceduret::set_to_true(), SSA_steps, and util_throw_with_nested().

Referenced by convert().

◆ convert_decls()

void symex_target_equationt::convert_decls ( prop_convt prop_conv) const

converts declarations

Returns
-

Definition at line 422 of file symex_target_equation.cpp.

References prop_convt::convert(), SSA_steps, and util_throw_with_nested().

Referenced by convert().

◆ convert_goto_instructions()

void symex_target_equationt::convert_goto_instructions ( prop_convt prop_conv)

converts goto instructions

Returns
-

Definition at line 516 of file symex_target_equation.cpp.

References messaget::conditional_output(), const_literal(), prop_convt::convert(), messaget::debug(), messaget::eom(), SSA_steps, and util_throw_with_nested().

Referenced by convert().

◆ convert_guards()

void symex_target_equationt::convert_guards ( prop_convt prop_conv)

◆ convert_io()

void symex_target_equationt::convert_io ( decision_proceduret dec_proc)

converts I/O

parameters: decision procedure
Returns
-

Definition at line 664 of file symex_target_equation.cpp.

References merge_irep, symbol_exprt::set_identifier(), decision_proceduret::set_to(), SSA_steps, to_string(), and exprt::type().

Referenced by convert().

◆ count_assertions()

std::size_t symex_target_equationt::count_assertions ( ) const
inline

Definition at line 267 of file symex_target_equation.h.

References SSA_steps.

Referenced by scratch_programt::check_sat(), and convert_assertions().

◆ count_ignored_SSA_steps()

std::size_t symex_target_equationt::count_ignored_SSA_steps ( ) const
inline

Definition at line 278 of file symex_target_equation.h.

References SSA_steps.

Referenced by bmct::slice().

◆ dead()

void symex_target_equationt::dead ( const exprt guard,
const ssa_exprt ssa_lhs,
const sourcet source 
)
virtual

declare a fresh variable

Implements symex_targett.

Definition at line 186 of file symex_target_equation.cpp.

◆ decl()

◆ function_call()

void symex_target_equationt::function_call ( const exprt guard,
const irep_idt identifier,
const sourcet source 
)
virtual

◆ function_return()

◆ get_SSA_step()

SSA_stepst::iterator symex_target_equationt::get_SSA_step ( std::size_t  s)
inline

Definition at line 292 of file symex_target_equation.h.

References PRECONDITION, and SSA_steps.

◆ goto_instruction()

void symex_target_equationt::goto_instruction ( const exprt guard,
const exprt cond,
const sourcet source 
)
virtual

◆ has_threads()

bool symex_target_equationt::has_threads ( ) const
inline

◆ input()

void symex_target_equationt::input ( const exprt guard,
const sourcet source,
const irep_idt input_id,
const std::list< exprt > &  args 
)
virtual

◆ location()

◆ make_expression()

exprt symex_target_equationt::make_expression ( ) const

◆ memory_barrier()

void symex_target_equationt::memory_barrier ( const exprt guard,
const sourcet source 
)
virtual

◆ merge_ireps()

◆ output() [1/2]

void symex_target_equationt::output ( const exprt guard,
const sourcet source,
const irep_idt fmt,
const std::list< exprt > &  args 
)
virtual

◆ output() [2/2]

void symex_target_equationt::output ( std::ostream &  out,
const namespacet ns 
) const

Definition at line 711 of file symex_target_equation.cpp.

References SSA_steps.

◆ output_fmt()

◆ shared_read()

void symex_target_equationt::shared_read ( const exprt guard,
const ssa_exprt ssa_object,
unsigned  atomic_section_id,
const sourcet source 
)
virtual

◆ shared_write()

◆ spawn()

void symex_target_equationt::spawn ( const exprt guard,
const sourcet source 
)
virtual

Member Data Documentation

◆ merge_irep

merge_irept symex_target_equationt::merge_irep
protected

Definition at line 323 of file symex_target_equation.h.

Referenced by convert_io(), and merge_ireps().

◆ SSA_steps

SSA_stepst symex_target_equationt::SSA_steps

Definition at line 290 of file symex_target_equation.h.

Referenced by partial_order_concurrencyt::add_init_writes(), assertion(), symex_slice_by_tracet::assign_merges(), assignment(), assumption(), atomic_begin(), atomic_end(), partial_order_concurrencyt::build_event_lists(), build_goto_trace(), memory_model_sct::build_per_thread_map(), clear(), fault_localizationt::collect_guards(), symex_slicet::collect_open_variables(), symex_slice_by_tracet::compute_ts_back(), constraint(), convert_assertions(), convert_assignments(), convert_assumptions(), convert_constraints(), convert_decls(), convert_goto_instructions(), convert_guards(), convert_io(), count_assertions(), count_ignored_SSA_steps(), decl(), bmct::execute(), fault_localizationt::freeze_guards(), function_call(), function_return(), counterexample_beautificationt::get_failed_property(), fault_localizationt::get_failed_property(), counterexample_beautificationt::get_minimization_list(), get_SSA_step(), goto_instruction(), has_threads(), input(), location(), memory_barrier(), counterexample_beautificationt::operator()(), graphml_witnesst::operator()(), bmc_all_propertiest::operator()(), bmc_covert::operator()(), output(), output_fmt(), postcondition(), precondition(), memory_model_sct::program_order(), fault_localizationt::run(), bmc_covert::satisfying_assignment(), shared_read(), shared_write(), bmct::show_program(), bmct::show_vcc_json(), bmct::show_vcc_plain(), simple_slice(), symex_slicet::slice(), symex_slice_by_tracet::slice_by_trace(), symex_slice_by_tracet::slice_SSA_steps(), spawn(), and memory_model_sct::thread_spawn().


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