cprover
Loading...
Searching...
No Matches
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
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
irep.h
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
goto-instrument
contracts
dynamic-frames
dfcc_is_cprover_symbol.h
Generated by
1.13.1