#include "dfcc_is_cprover_symbol.h"
#include <util/cprover_prefix.h>
#include <util/prefix.h>
#include <util/suffix.h>
#include <unordered_set>

Include dependency graph for dfcc_is_cprover_symbol.cpp:

Functions
static void	init_function_symbols (std::unordered_set< irep_idt > &function_symbols)

static void	init_static_symbols (std::unordered_set< irep_idt > &static_symbols)

bool	dfcc_is_cprover_function_symbol (const irep_idt &id)
	Returns `true` iff id is one of the known CPROVER functions or starts with `__VERIFIER` or `nondet`.

bool	dfcc_is_cprover_static_symbol (const irep_idt &id)
	Returns `true` iff the symbol is one of the known CPROVER static instrumentation variables or ends with `$object` and represents an auto-generated object following a pointer dereference.

Function Documentation

◆ dfcc_is_cprover_function_symbol()

bool dfcc_is_cprover_function_symbol ( const irep_idt & id )

Returns true iff id is one of the known CPROVER functions or starts with __VERIFIER or nondet.

Definition at line 138 of file dfcc_is_cprover_symbol.cpp.

◆ dfcc_is_cprover_static_symbol()

bool dfcc_is_cprover_static_symbol ( const irep_idt & id )

Returns true iff the symbol is one of the known CPROVER static instrumentation variables or ends with $object and represents an auto-generated object following a pointer dereference.

Definition at line 148 of file dfcc_is_cprover_symbol.cpp.

◆ init_function_symbols()

static void init_function_symbols ( std::unordered_set< irep_idt > & function_symbols )

static

Definition at line 20 of file dfcc_is_cprover_symbol.cpp.

◆ init_static_symbols()

static void init_static_symbols ( std::unordered_set< irep_idt > & static_symbols )