17#include <unordered_set>
23 if(function_symbols.empty())
33 function_symbols.insert(
CPROVER_PREFIX "contracts_ptr_pred_ctx_init");
34 function_symbols.insert(
CPROVER_PREFIX "contracts_ptr_pred_ctx_reset");
36 function_symbols.insert(
CPROVER_PREFIX "contracts_car_set_contains");
37 function_symbols.insert(
CPROVER_PREFIX "contracts_car_set_create");
38 function_symbols.insert(
CPROVER_PREFIX "contracts_car_set_insert");
39 function_symbols.insert(
CPROVER_PREFIX "contracts_car_set_remove");
40 function_symbols.insert(
41 CPROVER_PREFIX "contracts_check_replace_ensures_was_freed_preconditions");
45 function_symbols.insert(
CPROVER_PREFIX "contracts_link_allocated");
46 function_symbols.insert(
CPROVER_PREFIX "contracts_link_deallocated");
47 function_symbols.insert(
CPROVER_PREFIX "contracts_link_ptr_pred_ctx");
48 function_symbols.insert(
CPROVER_PREFIX "contracts_obeys_contract");
50 function_symbols.insert(
CPROVER_PREFIX "contracts_obj_set_append");
51 function_symbols.insert(
CPROVER_PREFIX "contracts_obj_set_contains_exact");
52 function_symbols.insert(
CPROVER_PREFIX "contracts_obj_set_contains");
53 function_symbols.insert(
CPROVER_PREFIX "contracts_obj_set_create_append");
55 "contracts_obj_set_create_indexed_by_object_id");
56 function_symbols.insert(
CPROVER_PREFIX "contracts_obj_set_release");
57 function_symbols.insert(
CPROVER_PREFIX "contracts_obj_set_remove");
58 function_symbols.insert(
CPROVER_PREFIX "contracts_pointer_equals");
59 function_symbols.insert(
CPROVER_PREFIX "contracts_pointer_in_range_dfcc");
61 function_symbols.insert(
CPROVER_PREFIX "contracts_write_set_add_allocated");
62 function_symbols.insert(
CPROVER_PREFIX "contracts_write_set_add_decl");
63 function_symbols.insert(
CPROVER_PREFIX "contracts_write_set_add_freeable");
64 function_symbols.insert(
66 "contracts_write_set_check_allocated_deallocated_is_empty");
68 "contracts_write_set_check_array_copy");
70 "contracts_write_set_check_array_replace");
72 "contracts_write_set_check_array_set");
74 "contracts_write_set_check_assignment");
75 function_symbols.insert(
76 CPROVER_PREFIX "contracts_write_set_check_assigns_clause_inclusion");
78 "contracts_write_set_check_deallocate");
80 "contracts_write_set_check_frees_clause_inclusion");
82 "contracts_write_set_check_havoc_object");
83 function_symbols.insert(
CPROVER_PREFIX "contracts_write_set_create");
85 "contracts_write_set_deallocate_freeable");
87 "contracts_write_set_havoc_get_assignable_target");
89 "contracts_write_set_havoc_object_whole");
90 function_symbols.insert(
CPROVER_PREFIX "contracts_write_set_havoc_slice");
92 "contracts_write_set_insert_assignable");
94 "contracts_write_set_insert_object_from");
96 "contracts_write_set_insert_object_upto");
98 "contracts_write_set_insert_object_whole");
99 function_symbols.insert(
CPROVER_PREFIX "contracts_write_set_record_dead");
101 "contracts_write_set_record_deallocated");
102 function_symbols.insert(
CPROVER_PREFIX "contracts_write_set_release");
123 if(static_symbols.empty())
129 static_symbols.insert(
CPROVER_PREFIX "malloc_failure_mode_return_null");
131 "malloc_failure_mode_assert_then_assume");
143 std::unordered_set<irep_idt> function_symbols;
146 return function_symbols.find(
id) != function_symbols.end() ||
153 std::unordered_set<irep_idt> static_symbols;
155 return static_symbols.find(
id) != static_symbols.end() ||
bool has_prefix(const std::string &s, const std::string &prefix)
static void init_function_symbols(std::unordered_set< irep_idt > &function_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_pointer_predicate(const irep_idt &id)
Returns true iff the symbol is one of the CPROVER pointer predicates.
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...
static void init_static_symbols(std::unordered_set< irep_idt > &static_symbols)
const std::string & id2string(const irep_idt &d)
bool has_suffix(const std::string &s, const std::string &suffix)