cbmc/fresh__symbol_8h_source.html

/*******************************************************************\


Module: Fresh auxiliary symbol creation


Author: Chris Smowton, chris.smowton@diffblue.com


\*******************************************************************/


#ifndef CPROVER_UTIL_FRESH_SYMBOL_H

#define CPROVER_UTIL_FRESH_SYMBOL_H


#include <string>


#include "irep.h"


class namespacet;

class source_locationt;

class symbolt;

class symbol_table_baset;

class typet;


#if defined(__GNUC__) && __GNUC__ >= 14

[[gnu::no_dangling]]

#endif

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);


#if defined(__GNUC__) && __GNUC__ >= 14

[[gnu::no_dangling]]

#endif

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,

  const namespacet &ns,

  symbol_table_baset &symbol_table);


#endif // CPROVER_UTIL_FRESH_SYMBOL_H

ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562

ait::ait
ait()
Definition ai.h:565

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: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.h