diff --git a/regression/goto-instrument/dump-non-tag-struct/main.c b/regression/goto-instrument/dump-non-tag-struct/main.c new file mode 100644 index 00000000000..d31c7fe6e87 --- /dev/null +++ b/regression/goto-instrument/dump-non-tag-struct/main.c @@ -0,0 +1,9 @@ +#include + +int main() +{ + // CBMC's model of calloc includes an overflow check, which in turn creates a + // struct that holds both the arithmetic result and the overflow information. + // dump-c did not support this struct defined in place. + calloc(10, 1); +} diff --git a/regression/goto-instrument/dump-non-tag-struct/test.desc b/regression/goto-instrument/dump-non-tag-struct/test.desc new file mode 100644 index 00000000000..9448476c58f --- /dev/null +++ b/regression/goto-instrument/dump-non-tag-struct/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--dump-c +VERIFICATION SUCCESSFUL +^EXIT=0$ +^SIGNAL=0$ +-- +^Invariant check failed +^warning: ignoring +irep +-- +This test must pass compiling the output generated using dump-c, which implies +that dump-c succeeded and that all struct declarations are present. diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index bda434baf3d..06b3e22ca8f 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -25,11 +25,35 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include #include #include #include "goto_program2code.h" +static std::string clean_identifier(const irep_idt &id) +{ + std::string result; + result.reserve(id2string(id).size()); + + for(auto c : id2string(id)) + { + if(c >= '0' && c <= '9') + result += c; + else if(c >= 'A' && c <= 'Z') + result += c; + else if(c >= 'a' && c <= 'z') + result += c; + else if(c == '_' || c == '$') + result += c; + else + result += "_" + std::to_string(c); + } + + return result; +} + dump_c_configurationt dump_c_configurationt::default_configuration = dump_c_configurationt(); @@ -58,11 +82,32 @@ void dump_ct::operator()(std::ostream &os) // add copies of struct types when ID_C_transparent_union is only // annotated to parameter - symbol_tablet symbols_transparent; + symbol_tablet additional_symbols; for(const auto &named_symbol : copied_symbol_table.symbols) { const symbolt &symbol=named_symbol.second; + if( + (symbol.type.id() == ID_union || symbol.type.id() == ID_struct) && + !symbol.is_type) + { + type_symbolt ts{symbol.type}; + ts.mode = symbol.mode; + if(mode == ID_C) + ts.name = "tag-" + type2name(symbol.type, ns); + else if(mode == ID_cpp) + ts.name = "tag-" + cpp_type2name(symbol.type); + else + UNREACHABLE; + typet &type = + copied_symbol_table.get_writeable_ref(named_symbol.first).type; + if(ts.type.id() == ID_union) + type = union_tag_typet{ts.name}; + else + type = struct_tag_typet{ts.name}; + additional_symbols.add(ts); + } + if(symbol.type.id()!=ID_code) continue; @@ -86,14 +131,14 @@ void dump_ct::operator()(std::ostream &os) new_type_sym.type.set(ID_C_transparent_union, true); // we might have it already, in which case this has no effect - symbols_transparent.add(new_type_sym); + additional_symbols.add(new_type_sym); to_union_tag_type(type).set_identifier(new_type_sym.name); type.remove(ID_C_transparent_union); } } } - for(const auto &symbol_pair : symbols_transparent.symbols) + for(const auto &symbol_pair : additional_symbols.symbols) { copied_symbol_table.add(symbol_pair.second); } @@ -509,11 +554,11 @@ void dump_ct::convert_compound( collect_typedefs(comp.type(), true); } - irep_idt comp_name=comp.get_name(); - - struct_body << indent(1) << "// " << comp_name << '\n'; + struct_body << indent(1) << "// " << comp.get_name() << '\n'; struct_body << indent(1); + irep_idt comp_name = clean_identifier(comp.get_name()); + // component names such as "main" would collide with other objects in the // namespace std::string fake_unique_name="NO/SUCH/NS::"+id2string(comp_name); @@ -1519,6 +1564,12 @@ void dump_ct::cleanup_expr(exprt &expr) expr = unary_exprt{ID_initializer_list, bu.value()}; } } + else if(expr.id() == ID_member) + { + member_exprt &member_expr = to_member_expr(expr); + member_expr.set_component_name( + clean_identifier(member_expr.get_component_name())); + } } void dump_ct::cleanup_type(typet &type)