cprover
|
Fresh auxiliary symbol creation. More...
Go to the source code of this file.
Functions | |
symbolt & | get_fresh_aux_symbol (const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table) |
Installs a fresh-named symbol with the requested name pattern. More... | |
Fresh auxiliary symbol creation.
Definition in file fresh_symbol.h.
symbolt& get_fresh_aux_symbol | ( | const typet & | type, |
const std::string & | name_prefix, | ||
const std::string & | basename_prefix, | ||
const source_locationt & | source_location, | ||
const irep_idt & | symbol_mode, | ||
symbol_table_baset & | symbol_table | ||
) |
Installs a fresh-named symbol with the requested name pattern.
name_prefix
, basename_prefix
: new symbol will be named name_prefix::basename_prefix$num unless name_prefix is empty, in which case the :: prefix is omitted. source_location
: new symbol source loc symbol_mode
: new symbol mode symbol_table
: table to add the new symbol to Definition at line 28 of file fresh_symbol.cpp.
References CHECK_RETURN, get_new_name(), id2string(), symbol_table_baset::insert(), symbolt::location, symbolt::mode, symbolt::name, and dstringt::size().
Referenced by add_array_to_length_association(), add_character_set_constraint(), add_pointer_to_array_association(), allocate_dynamic_object(), java_object_factoryt::allocate_nondet_length_array(), java_object_factoryt::allocate_object(), c_new_tmp_symbol(), java_simple_method_stubst::create_method_stub(), java_string_library_preprocesst::decl_string_expr(), value_set_dereferencet::dereference(), remove_function_pointerst::fix_return_type(), java_string_library_preprocesst::fresh_array(), java_string_library_preprocesst::fresh_string(), java_object_factoryt::gen_nondet_array_init(), java_object_factoryt::gen_nondet_subtype_pointer_init(), java_string_library_preprocesst::get_primitive_value_of_object(), initialize_nondet_string_fields(), insert_nondet_init_code(), instrument_synchronized_code(), remove_instanceoft::lower_instanceof(), remove_java_newt::lower_java_new_array(), java_string_library_preprocesst::make_argument_for_format(), goto_convertt::make_compound_literal(), java_string_library_preprocesst::make_equals_function_code(), make_nondet_infinite_char_array(), java_string_library_preprocesst::make_object_get_class_code(), goto_convertt::new_tmp_symbol(), code_contractst::new_tmp_symbol(), goto_convertt::remove_cpp_new(), goto_convertt::remove_function_call(), goto_convertt::remove_malloc(), java_string_library_preprocesst::replace_char_array(), java_string_library_preprocesst::string_expr_of_function(), and java_bytecode_instrumentt::throw_exception().