cprover
fresh_symbol.cpp File Reference

Fresh auxiliary symbol creation. More...

#include "fresh_symbol.h"
#include "invariant.h"
#include "namespace.h"
#include "rename.h"
#include "symbol.h"
#include "symbol_table_base.h"
Include dependency graph for fresh_symbol.cpp:

Go to the source code of this file.

Functions

symboltget_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...
 

Detailed Description

Fresh auxiliary symbol creation.

Definition in file fresh_symbol.cpp.

Function Documentation

◆ get_fresh_aux_symbol()

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.

parameters: type: type of new symbol
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_struct(), 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().