CBMC
goto_symex_statet Member List

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

a_s_r_entryt typedefgoto_symex_statet
a_s_w_entryt typedefgoto_symex_statet
add_object(const symbol_exprt &expr, std::function< std::size_t(const irep_idt &)> index_generator, const namespacet &ns)goto_symex_statet
apply_condition(const exprt &condition, const goto_symex_statet &previous_state, const namespacet &ns)goto_statet
assignment(ssa_exprt lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)goto_symex_statet
atomic_section_idgoto_statet
call_stack()goto_symex_statetinline
call_stack() constgoto_symex_statetinline
declare(ssa_exprt ssa, const namespacet &ns)goto_symex_statet
depthgoto_statet
dereference_cachegoto_statet
dirtygoto_symex_statet
drop_existing_l1_name(const irep_idt &l1_identifier)goto_symex_statetinline
drop_l1_name(const irep_idt &l1_identifier)goto_symex_statetinline
field_sensitivitygoto_symex_statet
fresh_l2_name_providergoto_symex_statetprivate
get_l2_name_provider() constgoto_symex_statetinline
get_level2() constgoto_statetinline
goto_statet()=deletegoto_statet
goto_statet(const goto_statet &other)=defaultgoto_statet
goto_statet(goto_statet &&other)=defaultgoto_statet
goto_statet(guard_managert &guard_manager)goto_statetinlineexplicit
goto_symex_statet(const symex_targett::sourcet &, std::size_t max_field_sensitive_array_size, bool should_simplify, guard_managert &manager, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)goto_symex_statet
goto_symex_statet(const goto_symex_statet &other, symex_target_equationt *const target)goto_symex_statetinlineexplicit
goto_symex_statet(const goto_symex_statet &other)=defaultgoto_symex_statetprivate
guardgoto_statet
guard_identifier()goto_symex_statetinlinestatic
guard_managergoto_symex_statet
has_saved_jump_targetgoto_symex_statet
has_saved_next_instructiongoto_symex_statet
is_read_only_object(const exprt &lvalue)goto_symex_statetinlinestatic
l1_typesgoto_symex_statetprotected
l1_typest typedefgoto_symex_statetprotected
l2_rename_rvalues(exprt lvalue, const namespacet &ns)goto_symex_statet
l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)goto_symex_statet
l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns)goto_symex_statet
level1goto_symex_statet
level2goto_statetprotected
operator=(const goto_statet &other)=deletegoto_statet
operator=(goto_statet &&other)=defaultgoto_statet
output_propagation_map(std::ostream &)goto_statet
print_backtrace(std::ostream &) constgoto_symex_statet
propagationgoto_statet
reachablegoto_statet
read_in_atomic_sectiongoto_symex_statet
record_eventsgoto_symex_statet
remaining_vccsgoto_symex_statet
rename(exprt expr, const namespacet &ns)goto_symex_statet
rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns)goto_symex_statet
rename_address(exprt &expr, const namespacet &ns)goto_symex_statetprotected
rename_ssa(ssa_exprt ssa, const namespacet &ns)goto_symex_statet
run_validation_checksgoto_symex_statet
saved_targetgoto_symex_statet
set_indices(ssa_exprt expr, const namespacet &ns)goto_symex_statetprotected
set_indices(ssa_exprt ssa_expr, const namespacet &ns)goto_symex_statetprotected
set_indices(ssa_exprt ssa_expr, const namespacet &ns)goto_symex_statetprotected
set_indices(ssa_exprt ssa_expr, const namespacet &ns)goto_symex_statetprotected
shadow_memorygoto_symex_statet
sourcegoto_symex_statet
symbol_tablegoto_symex_statet
symex_targetgoto_symex_statet
threadsgoto_symex_statet
total_vccsgoto_symex_statet
value_setgoto_statet
write_is_shared(const ssa_exprt &expr, const namespacet &ns) constgoto_symex_statet
write_is_shared_resultt enum namegoto_symex_statet
written_in_atomic_sectiongoto_symex_statet
~goto_symex_statet()goto_symex_statet