C++ front end fixes [blocks: #2554]

regression/cbmc-cpp/CMakeLists.txt

@@ -4,6 +4,6 @@ add_test_pl_tests(
 )
 else()
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc>"
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
 )
 endif()

regression/cbmc-cpp/Makefile

@@ -10,10 +10,10 @@ else
 endif
 
 test:
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(gcc_only)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(gcc_only)
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(gcc_only)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(gcc_only)
 
 show:
 	@for dir in *; do \

regression/goto-cc-cbmc/chain.sh

@@ -6,13 +6,14 @@ is_windows=$3
 
 options=${*:4:$#-4}
 name=${*:$#}
-name=${name%.c}
+base_name=${name%.c}
+base_name=${base_name%.cpp}
 
 if [[ "${is_windows}" == "true" ]]; then
-  "${goto_cc}" "${name}.c"
-  mv "${name}.exe" "${name}.gb"
+  "${goto_cc}" "${name}"
+  mv "${base_name}.exe" "${base_name}.gb"
 else
-  "${goto_cc}" "${name}.c" -o "${name}.gb"
+  "${goto_cc}" "${name}" -o "${base_name}.gb"
 fi
 
-"${cbmc}" "${name}.gb" ${options}
+"${cbmc}" "${base_name}.gb" ${options}

regression/goto-cc-cbmc/cpp/main.cpp

@@ -0,0 +1,4 @@
+int main()
+{
+  return 0;
+}

regression/goto-cc-cbmc/cpp/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/systemc/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc>"
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
 )

regression/systemc/Makefile

@@ -1,10 +1,10 @@
 default: tests.log
 
 test:
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation"
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation"
 
 show:
 	@for dir in *; do \

src/cpp/cpp_declarator_converter.cpp

@@ -302,7 +302,8 @@ void cpp_declarator_convertert::combine_types(
         if(symbol.value.is_nil())
         {
           symbol_parameter.set_base_name(decl_parameter.get_base_name());
-          symbol_parameter.set_identifier(decl_parameter.get_identifier());
+          // set an empty identifier when no body is available
+          symbol_parameter.set_identifier(irep_idt());
           symbol_parameter.add_source_location()=
             decl_parameter.source_location();
         }
@@ -460,11 +461,6 @@ symbolt &cpp_declarator_convertert::convert_new_symbol(
   symbol.is_macro=is_typedef && !is_template_parameter;
   symbol.pretty_name=pretty_name;
 
-  // Constant? These are propagated.
-  if(symbol.type.get_bool(ID_C_constant) &&
-     symbol.value.is_not_nil())
-    symbol.is_macro=true;
-
   if(is_code && !symbol.is_type)
   {
     // it is a function
@@ -475,6 +471,13 @@ symbolt &cpp_declarator_convertert::convert_new_symbol(
 
     if(member_spec.is_inline())
       to_code_type(symbol.type).set_inlined(true);
+
+    if(symbol.value.is_nil())
+    {
+      // we don't need the identifiers
+      for(auto &parameter : to_code_type(symbol.type).parameters())
+        parameter.set_identifier(irep_idt());
+    }
   }
   else
   {

src/cpp/cpp_instantiate_template.cpp

@@ -54,6 +54,16 @@ std::string cpp_typecheckt::template_suffix(
     else // expression
     {
       exprt e=expr;
+
+      if(e.id() == ID_symbol)
+      {
+        const symbol_exprt &s = to_symbol_expr(e);
+        const symbolt &symbol = lookup(s.get_identifier());
+
+        if(cpp_is_pod(symbol.type) && symbol.type.get_bool(ID_C_constant))
+          e = symbol.value;
+      }
+
       make_constant(e);
 
       // this must be a constant, which includes true/false

src/cpp/cpp_language.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/get_base_name.h>
 
 #include <linking/linking.h>
+#include <linking/remove_internal_symbols.h>
 
 #include <ansi-c/ansi_c_entry_point.h>
 #include <ansi-c/c_preprocess.h>
@@ -132,6 +133,8 @@ bool cpp_languaget::typecheck(
       cpp_parse_tree, new_symbol_table, module, get_message_handler()))
     return true;
 
+  remove_internal_symbols(new_symbol_table, get_message_handler(), false);
+
   return linking(symbol_table, new_symbol_table, get_message_handler());
 }
 

src/cpp/cpp_typecheck_compound_type.cpp

@@ -733,13 +733,6 @@ void cpp_typecheckt::typecheck_compound_declarator(
       {
         new_symbol->value.swap(value);
         c_typecheck_baset::do_initializer(*new_symbol);
-
-        // these are macros if they are PODs and come with a (constant) value
-        if(new_symbol->type.get_bool(ID_C_constant))
-        {
-          simplify(new_symbol->value, *this);
-          new_symbol->is_macro=true;
-        }
       }
       else
       {
@@ -771,7 +764,18 @@ void cpp_typecheckt::check_fixed_size_array(typet &type)
     array_typet &array_type=to_array_type(type);
 
     if(array_type.size().is_not_nil())
+    {
+      if(array_type.size().id() == ID_symbol)
+      {
+        const symbol_exprt &s = to_symbol_expr(array_type.size());
+        const symbolt &symbol = lookup(s.get_identifier());
+
+        if(cpp_is_pod(symbol.type) && symbol.type.get_bool(ID_C_constant))
+          array_type.size() = symbol.value;
+      }
+
       make_constant_index(array_type.size());
+    }
 
     // recursive call for multi-dimensional arrays
     check_fixed_size_array(array_type.subtype());

src/cpp/cpp_typecheck_enum_type.cpp

@@ -63,6 +63,8 @@ void cpp_typecheckt::typecheck_enum_body(symbolt &enum_symbol)
     symbol.type=enum_tag_type;
     symbol.is_type=false;
     symbol.is_macro=true;
+    symbol.is_file_local = true;
+    symbol.is_thread_local = true;
 
     symbolt *new_symbol;
     if(symbol_table.move(symbol, new_symbol))

src/cpp/cpp_typecheck_resolve.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/mathematical_types.h>
 #include <util/prefix.h>
+#include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 #include <util/string_constant.h>
@@ -1046,6 +1047,26 @@ struct_tag_typet cpp_typecheck_resolvet::disambiguate_template_classes(
         source_location,
         primary_template_symbol,
         full_template_args);
+
+    for(auto &arg : full_template_args_tc.arguments())
+    {
+      if(arg.id() == ID_type)
+        continue;
+      if(arg.id() == ID_symbol)
+      {
+        const symbol_exprt &s = to_symbol_expr(arg);
+        const symbolt &symbol = cpp_typecheck.lookup(s.get_identifier());
+
+        if(
+          cpp_typecheck.cpp_is_pod(symbol.type) &&
+          symbol.type.get_bool(ID_C_constant))
+        {
+          arg = symbol.value;
+        }
+      }
+      simplify(arg, cpp_typecheck);
+    }
+
     // go back to where we used to be
   }
 

src/linking/remove_internal_symbols.cpp

@@ -95,6 +95,12 @@ void remove_internal_symbols(
   special.insert(CPROVER_PREFIX "deallocated");
   special.insert(CPROVER_PREFIX "dead_object");
   special.insert(CPROVER_PREFIX "rounding_mode");
+  special.insert("__new");
+  special.insert("__new_array");
+  special.insert("__placement_new");
+  special.insert("__placement_new_array");
+  special.insert("__delete");
+  special.insert("__delete_array");
 
   for(symbol_tablet::symbolst::const_iterator
       it=symbol_table.symbols.begin();
@@ -139,8 +145,9 @@ void remove_internal_symbols(
     {
       // body? not local (i.e., "static")?
       if(
-        has_body && (!is_file_local || (config.main.has_value() &&
-                                        symbol.name == config.main.value())))
+        has_body &&
+        (!is_file_local ||
+         (config.main.has_value() && symbol.base_name == config.main.value())))
       {
         get_symbols(ns, symbol, exported);
       }

src/util/config.cpp

@@ -915,6 +915,8 @@ bool configt::set(const cmdlinet &cmdline)
       ansi_c.preprocessor=ansi_ct::preprocessort::GCC;
       ansi_c.mode=ansi_ct::flavourt::VISUAL_STUDIO;
       #endif
+
+      cpp.cpp_standard = cppt::cpp_standardt::CPP14;
     }
   }
   else if(os=="macos")

src/util/symbol.cpp

@@ -142,7 +142,9 @@ bool symbolt::is_well_formed() const
   // Exception: Java symbols' base names do not have type signatures
   // (for example, they can have name "someclass.method:(II)V" and base name
   // "method")
-  if(!has_suffix(id2string(name), id2string(base_name)) && mode != ID_java)
+  if(
+    !has_suffix(id2string(name), id2string(base_name)) && mode != ID_java &&
+    mode != ID_cpp)
   {
     bool criterion_must_hold = true;