diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 80b5515dd0f..3a0a0ba2f84 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -30,6 +30,27 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_qualifiers.h" #include "expr2c_class.h" +// clang-format off + +expr2c_configurationt expr2c_configurationt::default_configuration +{ + true, + true, + true, + "TRUE", + "FALSE" +}; + +expr2c_configurationt expr2c_configurationt::clean_configuration +{ + false, + false, + false, + "1", + "0" +}; + +// clang-format on /* Precedences are as follows. Higher values mean higher precedence. @@ -661,7 +682,12 @@ std::string expr2ct::convert_struct_type( const std::string &qualifiers_str, const std::string &declarator_str) { - return convert_struct_type(src, qualifiers_str, declarator_str, true, true); + return convert_struct_type( + src, + qualifiers_str, + declarator_str, + configuration.print_struct_body_in_type, + configuration.include_struct_padding_components); } /// To generate C-like string for declaring (or defining) the given struct @@ -734,7 +760,8 @@ std::string expr2ct::convert_array_type( const qualifierst &qualifiers, const std::string &declarator_str) { - return convert_array_type(src, qualifiers, declarator_str, true); + return convert_array_type( + src, qualifiers, declarator_str, configuration.include_array_size); } /// To generate a C-like type declaration of an array. Optionally can include or @@ -1996,18 +2023,18 @@ std::string expr2ct::convert_constant( /// FALSE. std::string expr2ct::convert_constant_bool(bool boolean_value) { - // C doesn't really have these if(boolean_value) - return "TRUE"; + return configuration.true_string; else - return "FALSE"; + return configuration.false_string; } std::string expr2ct::convert_struct( const exprt &src, unsigned &precedence) { - return convert_struct(src, precedence, true); + return convert_struct( + src, precedence, configuration.include_struct_padding_components); } /// To generate a C-like string representing a struct. Can optionally include @@ -3947,17 +3974,55 @@ std::string expr2ct::convert(const exprt &src) return convert_with_precedence(src, precedence); } -std::string expr2c(const exprt &expr, const namespacet &ns) +/// Build a declaration string, which requires converting both a type and +/// putting an identifier in the syntactically correct position. +/// \param src: the type to convert +/// \param identifier: the identifier to use as the type +/// \return A C declaration of the given type with the right identifier. +std::string expr2ct::convert_with_identifier( + const typet &src, + const std::string &identifier) +{ + return convert_rec(src, c_qualifierst(), identifier); +} + +std::string expr2c( + const exprt &expr, + const namespacet &ns, + const expr2c_configurationt &configuration) { std::string code; - expr2ct expr2c(ns); + expr2ct expr2c(ns, configuration); expr2c.get_shorthands(expr); return expr2c.convert(expr); } -std::string type2c(const typet &type, const namespacet &ns) +std::string expr2c(const exprt &expr, const namespacet &ns) +{ + return expr2c(expr, ns, expr2c_configurationt::default_configuration); +} + +std::string type2c( + const typet &type, + const namespacet &ns, + const expr2c_configurationt &configuration) { - expr2ct expr2c(ns); + expr2ct expr2c(ns, configuration); // expr2c.get_shorthands(expr); return expr2c.convert(type); } + +std::string type2c(const typet &type, const namespacet &ns) +{ + return type2c(type, ns, expr2c_configurationt::default_configuration); +} + +std::string type2c( + const typet &type, + const std::string &identifier, + const namespacet &ns, + const expr2c_configurationt &configuration) +{ + expr2ct expr2c(ns, configuration); + return expr2c.convert_with_identifier(type, identifier); +} diff --git a/src/ansi-c/expr2c.h b/src/ansi-c/expr2c.h index 2bbcad3832e..3689c5478bb 100644 --- a/src/ansi-c/expr2c.h +++ b/src/ansi-c/expr2c.h @@ -16,7 +16,67 @@ class exprt; class namespacet; class typet; +/// Used for configuring the behaviour of expr2c and type2c +struct expr2c_configurationt final +{ + /// When printing struct_typet or struct_exprt, include the artificial padding + /// components introduced to keep the struct aligned. + bool include_struct_padding_components; + + /// When printing a struct_typet, should the components of the struct be + /// printed inline. + bool print_struct_body_in_type; + + /// When printing array_typet, should the size of the array be printed + bool include_array_size; + + /// This is the string that will be printed for the true boolean expression + std::string true_string; + + /// This is the string that will be printed for the false boolean expression + std::string false_string; + + expr2c_configurationt( + const bool include_struct_padding_components, + const bool print_struct_body_in_type, + const bool include_array_size, + std::string true_string, + std::string false_string) + : include_struct_padding_components(include_struct_padding_components), + print_struct_body_in_type(print_struct_body_in_type), + include_array_size(include_array_size), + true_string(std::move(true_string)), + false_string(std::move(false_string)) + { + } + + /// This prints a human readable C like syntax that closely mirrors the + /// internals of the GOTO program + static expr2c_configurationt default_configuration; + + /// This prints compilable C that loses some of the internal details of the + /// GOTO program + static expr2c_configurationt clean_configuration; +}; + std::string expr2c(const exprt &expr, const namespacet &ns); + +std::string expr2c( + const exprt &expr, + const namespacet &ns, + const expr2c_configurationt &configuration); + std::string type2c(const typet &type, const namespacet &ns); +std::string type2c( + const typet &type, + const namespacet &ns, + const expr2c_configurationt &configuration); + +std::string type2c( + const typet &type, + const std::string &identifier, + const namespacet &ns, + const expr2c_configurationt &configuration); + #endif // CPROVER_ANSI_C_EXPR2C_H diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h index a2424b8e5e3..e705260cc01 100644 --- a/src/ansi-c/expr2c_class.h +++ b/src/ansi-c/expr2c_class.h @@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_ANSI_C_EXPR2C_CLASS_H #define CPROVER_ANSI_C_EXPR2C_CLASS_H +#include "expr2c.h" + #include #include #include @@ -23,7 +25,13 @@ class namespacet; class expr2ct { public: - explicit expr2ct(const namespacet &_ns):ns(_ns), sizeof_nesting(0) { } + explicit expr2ct( + const namespacet &_ns, + const expr2c_configurationt &configuration = + expr2c_configurationt::default_configuration) + : ns(_ns), configuration(configuration), sizeof_nesting(0) + { + } virtual ~expr2ct() { } virtual std::string convert(const typet &src); @@ -31,8 +39,12 @@ class expr2ct void get_shorthands(const exprt &expr); + std::string + convert_with_identifier(const typet &src, const std::string &identifier); + protected: const namespacet &ns; + const expr2c_configurationt &configuration; virtual std::string convert_rec( const typet &src,