CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
dfcc_is_cprover_symbol.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking
4
5Author: Remi Delmas, delmasrd@amazon.com
6
7Date: 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
20bool dfcc_is_cprover_function_symbol(const irep_idt &id);
21
25bool dfcc_is_cprover_static_symbol(const irep_idt &id);
26
28bool dfcc_is_cprover_pointer_predicate(const irep_idt &id);
29
30#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:141
dfcc_is_cprover_pointer_predicate
bool dfcc_is_cprover_pointer_predicate(const irep_idt &id)
Returns true iff the symbol is one of the CPROVER pointer predicates.
Definition dfcc_is_cprover_symbol.cpp:162
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:151