cprover
Loading...
Searching...
No Matches
dfcc_is_cprover_symbol.cpp
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#include <util/cprover_prefix.h>
14#include <util/prefix.h>
15#include <util/suffix.h>
16
17#include <unordered_set>
18
19static void
20init_function_symbols(std::unordered_set<irep_idt> &function_symbols)
21{
22 // the set of all CPROVER symbols that we know of
23 if(function_symbols.empty())
24 {
25 function_symbols.insert(CPROVER_PREFIX "_start");
26 function_symbols.insert(CPROVER_PREFIX "array_copy");
27 function_symbols.insert(CPROVER_PREFIX "array_replace");
28 function_symbols.insert(CPROVER_PREFIX "array_set");
29 function_symbols.insert(CPROVER_PREFIX "assert");
30 function_symbols.insert(CPROVER_PREFIX "assignable");
31 function_symbols.insert(CPROVER_PREFIX "assume");
32 function_symbols.insert(CPROVER_PREFIX "contracts_car_create");
33 function_symbols.insert(CPROVER_PREFIX "contracts_car_set_contains");
34 function_symbols.insert(CPROVER_PREFIX "contracts_car_set_create");
35 function_symbols.insert(CPROVER_PREFIX "contracts_car_set_insert");
36 function_symbols.insert(CPROVER_PREFIX "contracts_car_set_remove");
37 function_symbols.insert(
38 CPROVER_PREFIX "contracts_check_replace_ensures_was_freed_preconditions");
39 function_symbols.insert(CPROVER_PREFIX "contracts_free");
40 function_symbols.insert(CPROVER_PREFIX "contracts_is_freeable");
41 function_symbols.insert(CPROVER_PREFIX "contracts_is_fresh");
42 function_symbols.insert(CPROVER_PREFIX "contracts_link_allocated");
43 function_symbols.insert(CPROVER_PREFIX "contracts_link_deallocated");
44 function_symbols.insert(CPROVER_PREFIX "contracts_link_is_fresh");
45 function_symbols.insert(CPROVER_PREFIX "contracts_obeys_contract");
46 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_add");
47 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_append");
48 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_contains_exact");
49 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_contains");
50 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_create_append");
52 "contracts_obj_set_create_indexed_by_object_id");
53 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_release");
54 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_remove");
55 function_symbols.insert(CPROVER_PREFIX "contracts_pointer_in_range_dfcc");
56 function_symbols.insert(CPROVER_PREFIX "contracts_was_freed");
57 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_allocated");
58 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_decl");
59 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_freeable");
60 function_symbols.insert(
62 "contracts_write_set_check_allocated_deallocated_is_empty");
64 "contracts_write_set_check_array_copy");
66 "contracts_write_set_check_array_replace");
68 "contracts_write_set_check_array_set");
70 "contracts_write_set_check_assignment");
71 function_symbols.insert(
72 CPROVER_PREFIX "contracts_write_set_check_assigns_clause_inclusion");
74 "contracts_write_set_check_deallocate");
76 "contracts_write_set_check_frees_clause_inclusion");
78 "contracts_write_set_check_havoc_object");
79 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_create");
81 "contracts_write_set_deallocate_freeable");
83 "contracts_write_set_havoc_get_assignable_target");
85 "contracts_write_set_havoc_object_whole");
86 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_havoc_slice");
88 "contracts_write_set_insert_assignable");
90 "contracts_write_set_insert_object_from");
92 "contracts_write_set_insert_object_upto");
94 "contracts_write_set_insert_object_whole");
95 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_record_dead");
97 "contracts_write_set_record_deallocated");
98 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_release");
99 function_symbols.insert(CPROVER_PREFIX "deallocate");
100 function_symbols.insert(CPROVER_PREFIX "freeable");
101 function_symbols.insert(CPROVER_PREFIX "havoc_object");
102 function_symbols.insert(CPROVER_PREFIX "havoc_slice");
103 function_symbols.insert(CPROVER_PREFIX "initialize");
104 function_symbols.insert(CPROVER_PREFIX "is_freeable");
105 function_symbols.insert(CPROVER_PREFIX "is_fresh");
106 function_symbols.insert(CPROVER_PREFIX "obeys_contract");
107 function_symbols.insert(CPROVER_PREFIX "object_from");
108 function_symbols.insert(CPROVER_PREFIX "object_upto");
109 function_symbols.insert(CPROVER_PREFIX "object_whole");
110 function_symbols.insert(CPROVER_PREFIX "pointer_in_range_dfcc");
111 function_symbols.insert(CPROVER_PREFIX "precondition");
112 function_symbols.insert(CPROVER_PREFIX "printf");
113 function_symbols.insert(CPROVER_PREFIX "was_freed");
114 }
115}
116
117static void init_static_symbols(std::unordered_set<irep_idt> &static_symbols)
118{
119 if(static_symbols.empty())
120 {
121 static_symbols.insert(CPROVER_PREFIX "dead_object");
122 static_symbols.insert(CPROVER_PREFIX "deallocated");
123 static_symbols.insert(CPROVER_PREFIX "fpu_control_word");
124 static_symbols.insert(CPROVER_PREFIX "jsa_jump_buffer");
125 static_symbols.insert(CPROVER_PREFIX "malloc_failure_mode_return_null");
127 "malloc_failure_mode_assert_then_assume");
128 static_symbols.insert(CPROVER_PREFIX "malloc_is_new_array");
129 static_symbols.insert(CPROVER_PREFIX "max_malloc_size");
130 static_symbols.insert(CPROVER_PREFIX "memory_leak");
131 static_symbols.insert(CPROVER_PREFIX "pipe_offset");
132 static_symbols.insert(CPROVER_PREFIX "pipes");
133 static_symbols.insert(CPROVER_PREFIX "rounding_mode");
134 }
135}
136
138{
139 std::unordered_set<irep_idt> function_symbols;
141 std::string str = id2string(id);
142 return function_symbols.find(id) != function_symbols.end() ||
143 // nondet functions
144 has_prefix(str, "__VERIFIER") || has_prefix(str, "nondet");
145}
146
148{
149 std::unordered_set<irep_idt> static_symbols;
151 return static_symbols.find(id) != static_symbols.end() ||
152 // auto objects from pointer derefs
153 has_suffix(id2string(id), "$object");
154}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_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_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)
Definition irep.h:47
bool has_suffix(const std::string &s, const std::string &suffix)
Definition suffix.h:17