cprover
fresh_symbol.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Fresh auxiliary symbol creation
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #include "fresh_symbol.h"
13 
23  const typet &type,
24  const std::string &name_prefix,
25  const std::string &basename_prefix,
26  const source_locationt &source_location,
27  const irep_idt &symbol_mode,
28  symbol_tablet &symbol_table)
29 {
30  static size_t temporary_counter=0;
31  auxiliary_symbolt new_symbol;
32  symbolt *symbol_ptr;
33 
34  do
35  {
36  // Distinguish local variables with the same name
37  new_symbol.base_name=
38  basename_prefix+
39  "$"+
40  std::to_string(++temporary_counter);
41  if(name_prefix.empty())
42  new_symbol.name=new_symbol.base_name;
43  else
44  new_symbol.name=
45  name_prefix+
46  "::"+
47  id2string(new_symbol.base_name);
48  new_symbol.type=type;
49  new_symbol.location=source_location;
50  new_symbol.mode=symbol_mode;
51  }
52  while(symbol_table.move(new_symbol, symbol_ptr));
53 
54  return *symbol_ptr;
55 }
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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_tablet &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
irep_idt mode
Language mode.
Definition: symbol.h:55
Fresh auxiliary symbol creation.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
The symbol table.
Definition: symbol_table.h:52
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:137
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52