CBMC
require_symbol.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Unit test utilities
4 
5 Author: Diffblue Limited.
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_TESTING_UTILS_REQUIRE_SYMBOL_H
10 #define CPROVER_TESTING_UTILS_REQUIRE_SYMBOL_H
11 
12 #include <util/irep.h>
13 
14 class symbol_tablet;
15 class symbolt;
16 
19 
20 // NOLINTNEXTLINE(readability/namespace)
21 namespace require_symbol
22 {
23 #if defined(__GNUC__) && __GNUC__ >= 14
24 [[gnu::no_dangling]]
25 #endif
26 const symbolt &
27 require_symbol_exists(
28  const symbol_tablet &symbol_table,
29  const irep_idt &symbol_identifier);
30 }
31 
32 #endif // CPROVER_TESTING_UTILS_REQUIRE_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
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
symbolt
Symbol table entry.
Definition: symbol.h:28
require_symbol
Definition: require_symbol.h:22
require_symbol::require_symbol_exists
const symbolt & require_symbol_exists(const symbol_tablet &symbol_table, const irep_idt &symbol_identifier)
Verify whether a given identifier is found in the symbol table and return it.
Definition: require_symbol.cpp:18