- w -

• w_guardst() : w_guardst
• w_ok_exprt() : w_ok_exprt
• wait_receivable() : piped_processt
• wait_receive() : piped_processt
• walk_array_tree() : smt2_convt
• wallace_tree() : bv_utilst
• warning() : linking_diagnosticst , messaget
• was_command_accepted() : gdb_apit
• weak_memory() : shared_bufferst::cfg_visitort , shared_bufferst
• weaken() : postconditiont
• what() : array_of_exprt , cprover_exception_baset , incorrect_goto_program_exceptiont , invalid_command_line_argument_exceptiont , invalid_function_contract_pair_exceptiont , invalid_restriction_exceptiont , invalid_source_file_exceptiont , invariant_failedt , invariant_with_diagnostics_failedt , require_goto_statements::no_decl_found_exceptiont , smt2_tokenizert::smt2_errort , typecheckt::errort
• where() : binding_exprt , let_exprt , with_exprt
• widen_lower_bound() : widened_ranget
• widen_upper_bound() : widened_ranget
• widened_ranget() : widened_ranget
• width() : bitvector_typet , consolet , ieee_float_spect
• with_exprt() : with_exprt
• with_location() : typecheckt::errort
• with_source_location() : array_exprt , exprt , symbol_exprt , typet
• with_state() : allocate_exprt , evaluate_exprt , state_cstrlen_exprt , state_is_cstring_exprt , state_is_dynamic_object_exprt , state_is_sentinel_dll_exprt , state_live_object_exprt , state_object_size_exprt , state_ok_exprt , state_type_compatible_exprt , update_state_exprt
• workt() : workt
• wrap() : journalling_symbol_tablet , symbol_table_buildert
• wrap_checked_function() : dfcct
• wrap_discovered_function_pointer_contracts() : dfcct
• wrap_function() : dfcc_utilst
• wrap_replaced_functions() : dfcct
• wrap_with_context() : variable_sensitivity_object_factoryt
• wrapper_goto_modelt() : wrapper_goto_modelt
• write() : _rw_set_loct , abstract_aggregate_objectt< aggregate_typet, aggregate_traitst > , abstract_environmentt , abstract_objectt , abstract_pointer_objectt , abstract_value_objectt , ansi_c_convert_typet , c_qualifierst , context_abstract_objectt , copy_on_writet< T > , cpp_convert_typet , data_dependency_contextt , java_qualifierst , liveness_contextt , non_sharing_treet< derivedt, named_subtreest > , reference_counting< T, empty > , shared_bufferst , sharing_treet< derivedt, named_subtreest > , write_location_contextt
• write_bin_object_file() : compilet
• write_clauses() : dimacs_cnft
• write_cnf_file() : external_satt
• write_component() : abstract_aggregate_objectt< aggregate_typet, aggregate_traitst > , full_array_abstract_objectt , full_struct_abstract_objectt
• write_container() : sharing_nodet< keyT, valueT, equalT >
• write_dereference() : abstract_pointer_objectt , constant_pointer_abstract_objectt , two_value_pointer_abstract_objectt , value_set_pointer_abstract_objectt
• write_dimacs() : bv_dimacst
• write_dimacs_clause() : dimacs_cnft
• write_dimacs_cnf() : dimacs_cnft
• write_dimacs_pb() : pbs_dimacs_cnft
• write_dot_subgraph() : dott
• write_edge() : dott
• write_element() : full_array_abstract_objectt
• write_footer() : smt2_convt
• write_header() : smt2_convt
• write_internal() : sharing_nodet< keyT, valueT, equalT >
• write_irep() : irep_serializationt
• write_is_shared() : goto_symex_statet
• write_leaf_element() : full_array_abstract_objectt
• write_location_context() : abstract_objectt , context_abstract_objectt , full_array_abstract_objectt , full_struct_abstract_objectt
• write_location_contextt() : write_location_contextt
• write_prefix() : qdimacs_cnft
• write_problem_line() : dimacs_cnft
• write_qdimacs_cnf() : qbf_squolem_coret , qdimacs_cnft
• write_serialization_external() : memory_model_sct
• write_set_add_allocated_call() : dfcc_libraryt
• write_set_add_decl_call() : dfcc_libraryt
• write_set_check_allocated_deallocated_is_empty_call() : dfcc_libraryt
• write_set_check_array_copy_call() : dfcc_libraryt
• write_set_check_array_replace_call() : dfcc_libraryt
• write_set_check_array_set_call() : dfcc_libraryt
• write_set_check_assignment_call() : dfcc_libraryt
• write_set_check_assigns_clause_inclusion_call() : dfcc_libraryt
• write_set_check_deallocate_call() : dfcc_libraryt
• write_set_check_frees_clause_inclusion_call() : dfcc_libraryt
• write_set_check_havoc_object_call() : dfcc_libraryt
• write_set_create_call() : dfcc_libraryt
• write_set_deallocate_freeable_call() : dfcc_libraryt
• write_set_record_dead_call() : dfcc_libraryt
• write_set_record_deallocated_call() : dfcc_libraryt
• write_set_release_call() : dfcc_libraryt
• write_stackt() : write_stackt
• write_string_ref() : irep_serializationt
• write_sub_element() : full_array_abstract_objectt
• write_to_file() : function_pointer_restrictionst
• write_to_gdb() : gdb_apit
• writeable_object() : axiomst
• writeable_object_exprt() : writeable_object_exprt
• writeable_object_fc() : axiomst
• wrote_object_files() : compilet