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;
20class source_locationt;
21class symbolt;
22class symbol_table_baset;
23class typet;
24
25#if defined(__GNUC__) && __GNUC__ >= 14
26[[gnu::no_dangling]]
27#endif
28symbolt &
29get_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
40symbolt &
41get_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
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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
irep_idt
dstringt irep_idt
Definition verification_result.h:16