CBMC
dfcc_is_cprover_symbol.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking
4 
5 Author: Remi Delmas, delmasrd@amazon.com
6 
7 Date: March 2023
8 
9 \*******************************************************************/
10 
12 
13 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_IS_CPROVER_SYMBOL_H
14 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_IS_CPROVER_SYMBOL_H
15 
16 #include <util/irep.h>
17 
20 bool dfcc_is_cprover_function_symbol(const irep_idt &id);
21 
25 bool dfcc_is_cprover_static_symbol(const irep_idt &id);
26 
27 #endif
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
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: dfcc_is_cprover_symbol.cpp:138
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...
Definition: dfcc_is_cprover_symbol.cpp:148