CBMC
dfcc_is_cprover_symbol.h File Reference
#include <util/irep.h>
+ Include dependency graph for dfcc_is_cprover_symbol.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

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.