cprover
Loading...
Searching...
No Matches
fresh_symbol.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Fresh auxiliary symbol creation
4
5Author: 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 "irep.h"
18
19class namespacet;
21class symbolt;
23class typet;
24
26 const typet &type,
27 const std::string &name_prefix,
28 const std::string &basename_prefix,
30 const irep_idt &symbol_mode,
31 symbol_table_baset &symbol_table);
32
34 const typet &type,
35 const std::string &name_prefix,
36 const std::string &basename_prefix,
38 const irep_idt &symbol_mode,
39 const namespacet &ns,
40 symbol_table_baset &symbol_table);
41
42#endif // CPROVER_UTIL_FRESH_SYMBOL_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
const source_locationt & source_location() const
Definition type.h:74
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 in the given symbol table.