Skip to content

Commit 1212839

Browse files
author
thk123
committed
Add type2c conversion for specifying a type name
1 parent 000f345 commit 1212839

File tree

3 files changed

+31
-0
lines changed

3 files changed

+31
-0
lines changed

src/ansi-c/expr2c.cpp

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3965,6 +3965,18 @@ std::string expr2ct::convert(const exprt &src)
39653965
return convert_with_precedence(src, precedence);
39663966
}
39673967

3968+
/// Build a declaration string, which requires converting both a type and
3969+
/// putting an identifier in the syntactically correct position.
3970+
/// \param src: the type to convert
3971+
/// \param identifier: the identifier to use as the type
3972+
/// \return A C declaration of the given type with the right identifier.
3973+
std::string expr2ct::convert_with_identifier(
3974+
const typet &src,
3975+
const std::string &identifier)
3976+
{
3977+
return convert_rec(src, c_qualifierst(), identifier);
3978+
}
3979+
39683980
std::string expr2c(
39693981
const exprt &expr,
39703982
const namespacet &ns,
@@ -3995,3 +4007,13 @@ std::string type2c(const typet &type, const namespacet &ns)
39954007
{
39964008
return type2c(type, ns, expr2c_configurationt::default_configuration);
39974009
}
4010+
4011+
std::string type2c(
4012+
const typet &type,
4013+
const std::string &identifier,
4014+
const namespacet &ns,
4015+
const expr2c_configurationt &configuration)
4016+
{
4017+
expr2ct expr2c(ns, configuration);
4018+
return expr2c.convert_with_identifier(type, identifier);
4019+
}

src/ansi-c/expr2c.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -73,4 +73,10 @@ std::string type2c(
7373
const namespacet &ns,
7474
const expr2c_configurationt &configuration);
7575

76+
std::string type2c(
77+
const typet &type,
78+
const std::string &identifier,
79+
const namespacet &ns,
80+
const expr2c_configurationt &configuration);
81+
7682
#endif // CPROVER_ANSI_C_EXPR2C_H

src/ansi-c/expr2c_class.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,9 @@ class expr2ct
4040

4141
void get_shorthands(const exprt &expr);
4242

43+
std::string
44+
convert_with_identifier(const typet &src, const std::string &identifier);
45+
4346
protected:
4447
const namespacet &ns;
4548
const expr2c_configurationt &configuration;

0 commit comments

Comments
 (0)