CBMC
dfcc_is_cprover_symbol.cpp File Reference
#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:

Go to the source code of this file.

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. More...
 
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. More...
 

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

Definition at line 118 of file dfcc_is_cprover_symbol.cpp.