cbmc/require__symbol_8h_source.html

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


Module: Unit test utilities


Author: Diffblue Limited.


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


#ifndef CPROVER_TESTING_UTILS_REQUIRE_SYMBOL_H

#define CPROVER_TESTING_UTILS_REQUIRE_SYMBOL_H


#include <util/irep.h>


class symbol_tablet;

class symbolt;


// NOLINTNEXTLINE(readability/namespace)


namespace require_symbol

{

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

[[gnu::no_dangling]]

#endif

const symbolt &

require_symbol_exists(

  const symbol_tablet &symbol_table,

  const irep_idt &symbol_identifier);

}

namespace require_symbol {…}


#endif // CPROVER_TESTING_UTILS_REQUIRE_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

symbol_tablet
The symbol table.
Definition symbol_table.h:14

symbolt
Symbol table entry.
Definition symbol.h:28

irep.h

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