|
CBMC
|
This is the complete list of members for symex_target_equationt, including all inherited members.
| argument_count | symex_target_equationt | protected |
| assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source) | symex_target_equationt | virtual |
| 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_equationt | virtual |
| assignment_typet enum name | symex_targett | |
| assumption(const exprt &guard, const exprt &cond, const sourcet &source) | symex_target_equationt | virtual |
| atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source) | symex_target_equationt | virtual |
| atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source) | symex_target_equationt | virtual |
| clear() | symex_target_equationt | inline |
| constraint(const exprt &cond, const std::string &msg, const sourcet &source) | symex_target_equationt | virtual |
| convert(decision_proceduret &decision_procedure) | symex_target_equationt | |
| convert_assertions(decision_proceduret &decision_procedure, bool optimized_for_single_assertions=true) | symex_target_equationt | |
| convert_assignments(decision_proceduret &decision_procedure) | symex_target_equationt | |
| convert_assumptions(decision_proceduret &decision_procedure) | symex_target_equationt | |
| convert_constraints(decision_proceduret &decision_procedure) | symex_target_equationt | |
| convert_decls(decision_proceduret &decision_procedure) | symex_target_equationt | |
| convert_function_calls(decision_proceduret &decision_procedure) | symex_target_equationt | |
| convert_goto_instructions(decision_proceduret &decision_procedure) | symex_target_equationt | |
| convert_guards(decision_proceduret &decision_procedure) | symex_target_equationt | |
| convert_io(decision_proceduret &decision_procedure) | symex_target_equationt | |
| convert_without_assertions(decision_proceduret &decision_procedure) | symex_target_equationt | |
| count_assertions() const | symex_target_equationt | inline |
| count_ignored_SSA_steps() const | symex_target_equationt | inline |
| dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source) | symex_target_equationt | virtual |
| decl(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &initializer, const sourcet &source, assignment_typet assignment_type) | symex_target_equationt | virtual |
| function_call(const exprt &guard, const irep_idt &function_id, const std::vector< renamedt< exprt, L2 >> &ssa_function_arguments, const sourcet &source, bool hidden) | symex_target_equationt | virtual |
| function_return(const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden) | symex_target_equationt | virtual |
| get_SSA_step(std::size_t s) | symex_target_equationt | inline |
| goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source) | symex_target_equationt | virtual |
| has_threads() const | symex_target_equationt | inline |
| input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args) | symex_target_equationt | virtual |
| io_count | symex_target_equationt | protected |
| location(const exprt &guard, const sourcet &source) | symex_target_equationt | virtual |
| log | symex_target_equationt | protected |
| make_expression() const | symex_target_equationt | |
| memory_barrier(const exprt &guard, const sourcet &source) | symex_target_equationt | virtual |
| merge_irep | symex_target_equationt | protected |
| merge_ireps(SSA_stept &SSA_step) | symex_target_equationt | protected |
| output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 >> &args) | symex_target_equationt | virtual |
| output(std::ostream &out) const | symex_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_equationt | virtual |
| shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source) | symex_target_equationt | virtual |
| shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source) | symex_target_equationt | virtual |
| spawn(const exprt &guard, const sourcet &source) | symex_target_equationt | virtual |
| SSA_steps | symex_target_equationt | |
| SSA_stepst typedef | symex_target_equationt | |
| symex_target_equationt(message_handlert &message_handler) | symex_target_equationt | inlineexplicit |
| symex_targett() | symex_targett | inline |
| validate(const namespacet &ns, const validation_modet vm) const | symex_target_equationt | inline |
| ~symex_target_equationt()=default | symex_target_equationt | virtual |
| ~symex_targett() | symex_targett | inlinevirtual |