Enable internal validation for C++ regression tests

We should perform as much sanity checking in regression tests as
possible. This required cleaning up unused parameter identifiers and
disabling sanity checking of names as is already done for Java, because
we similarly have name mangling in C++.

Author: tautschnig

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/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();
         }
@@ -470,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/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;