CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
require_symbol.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Unit test utilities
4
5Author: Diffblue Limited.
6
7\*******************************************************************/
8
9#include "require_symbol.h"
10
11#include <util/symbol_table.h>
12
13#include <testing-utils/use_catch.h>
14
18const symbolt &require_symbol::require_symbol_exists(
19 const symbol_tablet &symbol_table,
20 const irep_idt &symbol_identifier)
21{
22 const symbolt *found_symbol = symbol_table.lookup(symbol_identifier);
23 INFO("Looking for symbol: " + id2string(symbol_identifier));
24 REQUIRE(found_symbol != nullptr);
25 return *found_symbol;
26}
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition symbol_table_base.h:96
symbol_tablet
The symbol table.
Definition symbol_table.h:14
symbolt
Symbol table entry.
Definition symbol.h:28
id2string
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
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
require_symbol.h
Helper functions for getting symbols from the symbol table during unit tests.
symbol_table.h
Author: Diffblue Ltd.
use_catch.h