diff --git a/regression/cpp/enum7/test.desc b/regression/cpp/enum7/test.desc index 5893356edf6..a003b07b93c 100644 --- a/regression/cpp/enum7/test.desc +++ b/regression/cpp/enum7/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.cpp ^EXIT=0$ diff --git a/src/cpp/cpp_typecheck_enum_type.cpp b/src/cpp/cpp_typecheck_enum_type.cpp index e4481866b12..c3c1130102d 100644 --- a/src/cpp/cpp_typecheck_enum_type.cpp +++ b/src/cpp/cpp_typecheck_enum_type.cpp @@ -12,9 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "cpp_typecheck.h" #include +#include +#include #include -#include #include "cpp_enum_type.h" @@ -140,7 +141,9 @@ void cpp_typecheckt::typecheck_enum_type(typet &type) throw 0; } } - else if(has_body) + else if( + has_body || + config.ansi_c.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO) { std::string pretty_name= cpp_scopes.current_scope().prefix+id2string(base_name); @@ -200,7 +203,8 @@ void cpp_typecheckt::typecheck_enum_type(typet &type) if(new_symbol->type.get_bool(ID_C_class)) cpp_scopes.go_to(scope_identifier); - typecheck_enum_body(*new_symbol); + if(has_body) + typecheck_enum_body(*new_symbol); } else {