CBMC
|
#include "dfcc_is_cprover_symbol.h"
#include <util/cprover_prefix.h>
#include <util/prefix.h>
#include <util/suffix.h>
#include <unordered_set>
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... | |
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.
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.
|
static |
Definition at line 20 of file dfcc_is_cprover_symbol.cpp.
|
static |
Definition at line 118 of file dfcc_is_cprover_symbol.cpp.