dfcc_is_cprover_symbol.h File Reference

#include <util/irep.h>

Include dependency graph for dfcc_is_cprover_symbol.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
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.

Function Documentation

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 at line 141 of file dfcc_is_cprover_symbol.cpp.

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 at line 162 of file dfcc_is_cprover_symbol.cpp.

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 $object and represents an auto-generated object following a pointer dereference.

Definition at line 151 of file dfcc_is_cprover_symbol.cpp.