cprover
symex_target_equationt Member List

This is the complete list of members for symex_target_equationt, including all inherited members.

assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)symex_target_equationtvirtual
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)symex_target_equationtvirtual
assignment_typet enum namesymex_targett
assumption(const exprt &guard, const exprt &cond, const sourcet &source)symex_target_equationtvirtual
atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)symex_target_equationtvirtual
atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)symex_target_equationtvirtual
clear()symex_target_equationtinline
constraint(const exprt &cond, const std::string &msg, const sourcet &source)symex_target_equationtvirtual
convert(prop_convt &prop_conv)symex_target_equationt
convert_assertions(prop_convt &prop_conv)symex_target_equationt
convert_assignments(decision_proceduret &decision_procedure) constsymex_target_equationt
convert_assumptions(prop_convt &prop_conv)symex_target_equationt
convert_constraints(decision_proceduret &decision_procedure) constsymex_target_equationt
convert_decls(prop_convt &prop_conv) constsymex_target_equationt
convert_function_calls(decision_proceduret &decision_procedure)symex_target_equationt
convert_goto_instructions(prop_convt &prop_conv)symex_target_equationt
convert_guards(prop_convt &prop_conv)symex_target_equationt
convert_io(decision_proceduret &decision_procedure)symex_target_equationt
count_assertions() constsymex_target_equationtinline
count_ignored_SSA_steps() constsymex_target_equationtinline
dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)symex_target_equationtvirtual
decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)symex_target_equationtvirtual
function_call(const exprt &guard, const irep_idt &function_identifier, const std::vector< exprt > &ssa_function_arguments, const sourcet &source, bool hidden)symex_target_equationtvirtual
function_return(const exprt &guard, const sourcet &source, bool hidden)symex_target_equationtvirtual
get_SSA_step(std::size_t s)symex_target_equationtinline
goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)symex_target_equationtvirtual
has_threads() constsymex_target_equationtinline
input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)symex_target_equationtvirtual
location(const exprt &guard, const sourcet &source)symex_target_equationtvirtual
make_expression() constsymex_target_equationt
memory_barrier(const exprt &guard, const sourcet &source)symex_target_equationtvirtual
merge_irepsymex_target_equationtprotected
merge_ireps(SSA_stept &SSA_step)symex_target_equationtprotected
output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< exprt > &args)symex_target_equationtvirtual
output(std::ostream &out, const namespacet &ns) constsymex_target_equationt
output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)symex_target_equationtvirtual
shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)symex_target_equationtvirtual
shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)symex_target_equationtvirtual
spawn(const exprt &guard, const sourcet &source)symex_target_equationtvirtual
SSA_stepssymex_target_equationt
SSA_stepst typedefsymex_target_equationt
symex_targett()symex_targettinline
validate(const namespacet &ns, const validation_modet vm) constsymex_target_equationtinline
~symex_target_equationt()=defaultsymex_target_equationtvirtual
~symex_targett()symex_targettinlinevirtual