@@ -6,9 +6,11 @@ Author: Daniel Poetzl
6
6
7
7
\*******************************************************************/
8
8
9
+ #include < testing-utils/get_goto_model_from_c.h>
9
10
#include < testing-utils/message.h>
10
11
#include < testing-utils/use_catch.h>
11
12
13
+ #include < goto-programs/label_function_pointer_call_sites.h>
12
14
#include < goto-programs/restrict_function_pointers.h>
13
15
14
16
#include < json/json_parser.h>
@@ -17,6 +19,7 @@ class fp_restrictionst : public function_pointer_restrictionst
17
19
{
18
20
friend void restriction_parsing_test ();
19
21
friend void merge_restrictions_test ();
22
+ friend void get_function_pointer_by_name_restrictions_test ();
20
23
};
21
24
22
25
void restriction_parsing_test ()
@@ -92,6 +95,136 @@ void merge_restrictions_test()
92
95
REQUIRE (fp2_restrictions.count (" func1" ) == 1 );
93
96
}
94
97
98
+ void get_function_pointer_by_name_restrictions_test ()
99
+ {
100
+ SECTION (" Translate parameter restriction to indexed restriction" )
101
+ {
102
+ const std::string code = R"(
103
+ typedef void (*fp_t)(void);
104
+ void f();
105
+
106
+ void func(fp_t fp)
107
+ {
108
+ f(); // ignored
109
+
110
+ fp();
111
+ }
112
+
113
+ void main() {}
114
+ )" ;
115
+
116
+ goto_modelt goto_model = get_goto_model_from_c (code);
117
+ label_function_pointer_call_sites (goto_model);
118
+
119
+ const auto restrictions =
120
+ fp_restrictionst::get_function_pointer_by_name_restrictions (
121
+ {" func::fp/g" }, goto_model);
122
+
123
+ REQUIRE (restrictions.size () == 1 );
124
+
125
+ const auto set = restrictions.at (" func.function_pointer_call.1" );
126
+ REQUIRE (set.size () == 1 );
127
+ REQUIRE (set.count (" g" ) == 1 );
128
+ }
129
+
130
+ SECTION (" Translate local nested variable restriction to indexed restriction" )
131
+ {
132
+ const std::string code = R"(
133
+ typedef void (*fp_t)(void);
134
+ void f();
135
+
136
+ void main()
137
+ {
138
+ f(); // ignored
139
+
140
+ {
141
+ fp_t fp;
142
+ fp();
143
+ }
144
+ }
145
+ )" ;
146
+
147
+ goto_modelt goto_model = get_goto_model_from_c (code);
148
+ label_function_pointer_call_sites (goto_model);
149
+
150
+ const auto restrictions =
151
+ fp_restrictionst::get_function_pointer_by_name_restrictions (
152
+ {" main::1::1::fp/g" }, goto_model);
153
+
154
+ REQUIRE (restrictions.size () == 1 );
155
+
156
+ const auto set = restrictions.at (" main.function_pointer_call.1" );
157
+ REQUIRE (set.size () == 1 );
158
+ REQUIRE (set.count (" g" ) == 1 );
159
+ }
160
+
161
+ SECTION (" Translate global variable restriction to indexed restriction" )
162
+ {
163
+ const std::string code = R"(
164
+ typedef void (*fp_t)(void);
165
+ void f();
166
+
167
+ fp_t fp;
168
+
169
+ void main()
170
+ {
171
+ f(); // ignored
172
+
173
+ fp();
174
+ }
175
+ )" ;
176
+
177
+ goto_modelt goto_model = get_goto_model_from_c (code);
178
+ label_function_pointer_call_sites (goto_model);
179
+
180
+ const auto restrictions =
181
+ fp_restrictionst::get_function_pointer_by_name_restrictions (
182
+ {" fp/g" }, goto_model);
183
+
184
+ REQUIRE (restrictions.size () == 1 );
185
+
186
+ const auto set = restrictions.at (" main.function_pointer_call.1" );
187
+ REQUIRE (set.size () == 1 );
188
+ REQUIRE (set.count (" g" ) == 1 );
189
+ }
190
+
191
+ SECTION (" Translate a variable restriction to indexed restrictions, "
192
+ " for the case when a function pointer is called more than once" )
193
+ {
194
+ const std::string code = R"(
195
+ typedef void (*fp_t)(void);
196
+ void f();
197
+
198
+ fp_t fp;
199
+
200
+ void main()
201
+ {
202
+ f(); // ignored
203
+
204
+ fp();
205
+ fp(); // second call to same function pointer
206
+ }
207
+ )" ;
208
+
209
+ goto_modelt goto_model = get_goto_model_from_c (code);
210
+ label_function_pointer_call_sites (goto_model);
211
+
212
+ const auto restrictions =
213
+ fp_restrictionst::get_function_pointer_by_name_restrictions (
214
+ {" fp/g" }, goto_model);
215
+
216
+ REQUIRE (restrictions.size () == 2 );
217
+
218
+ const auto set1 = restrictions.at (" main.function_pointer_call.1" );
219
+ REQUIRE (set1.size () == 1 );
220
+ REQUIRE (set1.count (" g" ) == 1 );
221
+
222
+ const auto set2 = restrictions.at (" main.function_pointer_call.2" );
223
+ REQUIRE (set2.size () == 1 );
224
+ REQUIRE (set2.count (" g" ) == 1 );
225
+ }
226
+ }
227
+
95
228
TEST_CASE (" Restriction parsing" , " [core]" )
96
229
{
97
230
restriction_parsing_test ();
@@ -152,3 +285,9 @@ TEST_CASE("Json conversion", "[core]")
152
285
function_pointer_restrictions1.restrictions ==
153
286
function_pointer_restrictions2.restrictions );
154
287
}
288
+
289
+ TEST_CASE (" Get function pointer by name restrictions" ,
290
+ " [core][goto-programs][restrict-function-pointers]" )
291
+ {
292
+ get_function_pointer_by_name_restrictions_test ();
293
+ }
0 commit comments