Skip to content

Commit f052eec

Browse files
committed
Filter out illegal characters from identifiers in typecheck_expr.
This change removes some characters, like "*{}", from identifier names that were autogenerated. The reason for this is that these names are now being passed on to other tools, and they cause these to fail with parsing errors.
1 parent f891bc1 commit f052eec

File tree

3 files changed

+36
-3
lines changed

3 files changed

+36
-3
lines changed

src/ansi-c/c_typecheck_expr.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1890,16 +1890,18 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
18901890
INVARIANT(
18911891
!parameters.empty(),
18921892
"GCC polymorphic built-ins should have at least one parameter");
1893+
/// XXX why are we only looking at the type of the first parameter?
18931894
if(parameters.front().type().id() == ID_pointer)
18941895
{
18951896
identifier_with_type =
18961897
id2string(identifier) + "_" +
1897-
type2name(parameters.front().type().subtype(), *this);
1898+
type2identifier(parameters.front().type().subtype(), *this);
18981899
}
18991900
else
19001901
{
1901-
identifier_with_type = id2string(identifier) + "_" +
1902-
type2name(parameters.front().type(), *this);
1902+
identifier_with_type =
1903+
id2string(identifier) + "_" +
1904+
type2identifier(parameters.front().type(), *this);
19031905
}
19041906
gcc_polymorphic->set_identifier(identifier_with_type);
19051907

src/ansi-c/type2name.cpp

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -272,3 +272,32 @@ std::string type2name(const typet &type, const namespacet &ns)
272272
symbol_numbert symbol_number;
273273
return type2name(type, ns, symbol_number);
274274
}
275+
276+
/// type2name generates strings that aren't valid C identifiers
277+
/// If we want utilities like dump_c to work properly identifiers
278+
/// should ideally always be valid C identifiers
279+
/// This replaces some invalid characters that can appear in type2name output.
280+
std::string type2identifier(const typet &type, const namespacet &ns)
281+
{
282+
auto type2name_res = type2name(type, ns);
283+
std::string result{};
284+
for(char c : type2name_res)
285+
{
286+
switch(c)
287+
{
288+
case '*':
289+
result += "_ptr_";
290+
break;
291+
case '{':
292+
result += "_start_sub_";
293+
break;
294+
case '}':
295+
result += "_end_sub_";
296+
break;
297+
default:
298+
result += c;
299+
break;
300+
}
301+
}
302+
return result;
303+
}

src/ansi-c/type2name.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,4 +20,6 @@ class namespacet;
2020

2121
std::string type2name(const typet &type, const namespacet &ns);
2222

23+
std::string type2identifier(const typet &type, const namespacet &ns);
24+
2325
#endif // CPROVER_ANSI_C_TYPE2NAME_H

0 commit comments

Comments
 (0)