cprover
fresh_symbol.h
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 #ifndef CPROVER_UTIL_FRESH_SYMBOL_H
13 #define CPROVER_UTIL_FRESH_SYMBOL_H
14 
15 #include <string>
16 
17 #include <util/irep.h>
18 #include <util/source_location.h>
19 #include <util/symbol_table.h>
20 #include <util/type.h>
21 
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 #endif // CPROVER_UTIL_FRESH_SYMBOL_H
The type of an expression.
Definition: type.h:20
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.
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
Symbol table.