Skip to content

Commit 87d0586

Browse files
author
thk123
committed
Add type2c conversion for specifying a type name
1 parent 9c266e1 commit 87d0586

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
@@ -3966,6 +3966,18 @@ std::string expr2ct::convert(const exprt &src)
39663966
return convert_with_precedence(src, precedence);
39673967
}
39683968

3969+
/// To convert a type in to ANSI-C but with the identifier in place.
3970+
/// This is useful for array types where the identifier is inside the type
3971+
/// \param src: the type to convert
3972+
/// \param identifier: the identifier to use as the type
3973+
/// \return A C declaration of the given type with the right identifier.
3974+
std::string expr2ct::convert_with_identifier(
3975+
const typet &src,
3976+
const std::string &identifier)
3977+
{
3978+
return convert_rec(src, c_qualifierst(), identifier);
3979+
}
3980+
39693981
std::string expr2c(
39703982
const exprt &expr,
39713983
const namespacet &ns,
@@ -3996,3 +4008,13 @@ std::string type2c(const typet &type, const namespacet &ns)
39964008
{
39974009
return type2c(type, ns, expr2c_configurationt::default_configuration);
39984010
}
4011+
4012+
std::string type2c(
4013+
const typet &type,
4014+
const std::string &identifier,
4015+
const namespacet &ns,
4016+
const expr2c_configurationt &configuration)
4017+
{
4018+
expr2ct expr2c(ns, configuration);
4019+
return expr2c.convert_with_identifier(type, identifier);
4020+
}

src/ansi-c/expr2c.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,4 +56,10 @@ std::string type2c(
5656
const namespacet &ns,
5757
const expr2c_configurationt &configuration);
5858

59+
std::string type2c(
60+
const typet &type,
61+
const std::string &identifier,
62+
const namespacet &ns,
63+
const expr2c_configurationt &configuration);
64+
5965
#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
@@ -37,6 +37,9 @@ class expr2ct
3737

3838
void get_shorthands(const exprt &expr);
3939

40+
std::string
41+
convert_with_identifier(const typet &src, const std::string &identifier);
42+
4043
protected:
4144
const namespacet &ns;
4245
const expr2c_configurationt &configuration;

0 commit comments

Comments
 (0)