CBMC
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 "irep.h"
18 
19 class namespacet;
20 class source_locationt;
21 class symbolt;
22 class symbol_table_baset;
23 class typet;
24 
25 #if defined(__GNUC__) && __GNUC__ >= 14
26 [[gnu::no_dangling]]
27 #endif
28 symbolt &
29 get_fresh_aux_symbol(
30  const typet &type,
31  const std::string &name_prefix,
32  const std::string &basename_prefix,
33  const source_locationt &source_location,
34  const irep_idt &symbol_mode,
35  symbol_table_baset &symbol_table);
36 
37 #if defined(__GNUC__) && __GNUC__ >= 14
38 [[gnu::no_dangling]]
39 #endif
40 symbolt &
41 get_fresh_aux_symbol(
42  const typet &type,
43  const std::string &name_prefix,
44  const std::string &basename_prefix,
45  const source_locationt &source_location,
46  const irep_idt &symbol_mode,
47  const namespacet &ns,
48  symbol_table_baset &symbol_table);
49 
50 #endif // CPROVER_UTIL_FRESH_SYMBOL_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
source_locationt
Definition: source_location.h:20
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:23
symbolt
Symbol table entry.
Definition: symbol.h:28
typet
The type of an expression, extends irept.
Definition: type.h:29
typet::source_location
const source_locationt & source_location() const
Definition: type.h:72
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 in the given symbol table.
Definition: fresh_symbol.cpp:71