File tree Expand file tree Collapse file tree 1 file changed +20
-0
lines changed Expand file tree Collapse file tree 1 file changed +20
-0
lines changed Original file line number Diff line number Diff line change @@ -64,6 +64,18 @@ static bool have_to_remove_vector(const typet &type)
64
64
if (have_to_remove_vector (c.type ()))
65
65
return true ;
66
66
}
67
+ else if (type.id () == ID_code)
68
+ {
69
+ const code_typet &code_type = to_code_type (type);
70
+
71
+ if (have_to_remove_vector (code_type.return_type ()))
72
+ return true ;
73
+ for (auto ¶meter : code_type.parameters ())
74
+ {
75
+ if (have_to_remove_vector (parameter.type ()))
76
+ return true ;
77
+ }
78
+ }
67
79
else if (type.id ()==ID_pointer ||
68
80
type.id ()==ID_complex ||
69
81
type.id ()==ID_array)
@@ -256,6 +268,14 @@ static void remove_vector(typet &type)
256
268
remove_vector (it->type ());
257
269
}
258
270
}
271
+ else if (type.id () == ID_code)
272
+ {
273
+ code_typet &code_type = to_code_type (type);
274
+
275
+ remove_vector (code_type.return_type ());
276
+ for (auto ¶meter : code_type.parameters ())
277
+ remove_vector (parameter.type ());
278
+ }
259
279
else if (type.id ()==ID_pointer ||
260
280
type.id ()==ID_complex ||
261
281
type.id ()==ID_array)
You can’t perform that action at this time.
0 commit comments