cprover
|
#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. | |
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. | |
bool | dfcc_is_cprover_pointer_predicate (const irep_idt &id) |
Returns true iff the symbol is one of the CPROVER pointer predicates. |
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 141 of file dfcc_is_cprover_symbol.cpp.
bool dfcc_is_cprover_pointer_predicate | ( | const irep_idt & | id | ) |
Returns true iff the symbol is one of the CPROVER pointer predicates.
Definition at line 162 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 151 of file dfcc_is_cprover_symbol.cpp.
|
static |
Definition at line 20 of file dfcc_is_cprover_symbol.cpp.
|
static |
Definition at line 121 of file dfcc_is_cprover_symbol.cpp.