Failing regression test from #933

Author: tautschnig

regression/cbmc/cpp2/main.cpp

@@ -0,0 +1,47 @@
+#include <cassert>
+#include <stdint.h>
+#include <stdbool.h>
+
+#undef HOTFIX
+
+typedef struct {
+  uint32_t value_31_0 : 32;
+} signal32_t;
+
+typedef struct {
+  uint8_t value_0_0 : 1;
+} signal1_t;
+
+static inline bool yosys_simplec_get_bit_25_of_32(const signal32_t *sig)
+{
+  return (sig->value_31_0 >> 25) & 1;
+}
+
+struct rvfi_insn_srai_state_t
+{
+  signal32_t rvfi_insn;
+  signal32_t rvfi_rs1_rdata;
+  signal1_t _abc_1398_n364;
+  signal1_t _abc_1398_n363;
+};
+
+void test(rvfi_insn_srai_state_t state, bool valid)
+{
+#ifndef HOTFIX
+  state._abc_1398_n364.value_0_0 = yosys_simplec_get_bit_25_of_32(&state.rvfi_insn) ?
+      yosys_simplec_get_bit_25_of_32(&state.rvfi_rs1_rdata) : state._abc_1398_n363.value_0_0;
+#else
+  state._abc_1398_n364.value_0_0 = yosys_simplec_get_bit_25_of_32(&state.rvfi_insn) ?
+      yosys_simplec_get_bit_25_of_32(&state.rvfi_rs1_rdata) : (bool)state._abc_1398_n363.value_0_0;
+#endif
+
+  assert(valid);
+}
+
+int main(int argc, char* argv[])
+{
+	rvfi_insn_srai_state_t state;
+  bool valid;
+  test(state, valid);
+  return 0;
+}

regression/cbmc/cpp2/test.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^equality without matching types
+--
+This has been reported as #933.

src/cpp/cpp_declarator_converter.cpp

@@ -68,7 +68,7 @@ symbolt &cpp_declarator_convertert::convert(
     scope=&cpp_typecheck.cpp_scopes.current_scope();
 
     // check the declarator-part of the type, in that scope
-    //TODO: if it is a friend declaration we have to type-check it
+    // TODO: if it is a friend declaration we have to type-check it
     //      in our current scope to have access to the correct
     //      template parameters, although the symbol finally resides
     //      in the resolved scope (actually it should be sufficient
@@ -77,7 +77,7 @@ symbolt &cpp_declarator_convertert::convert(
     if(!is_friend)
       cpp_typecheck.typecheck_type(final_type);
   }
-  //TODO: see comment above
+  // TODO: see comment above
   if(is_friend)
     cpp_typecheck.typecheck_type(final_type);
 

src/cpp/cpp_instantiate_template.cpp

@@ -458,8 +458,8 @@ const symbolt &cpp_typecheckt::instantiate_template(
     const irep_idt& new_symb_id = new_decl.type().get(ID_identifier);
     symbolt &new_symb = symbol_table.get_writeable_ref(new_symb_id);
 
-    //add template arguments to type in order to retrieve template map
-    //  when typechecking function body
+    // add template arguments to type in order to retrieve template map
+    // when typechecking function body
     new_symb.type.set(ID_C_template, template_type);
     new_symb.type.set(ID_C_template_arguments, specialization_template_args);
 

src/cpp/cpp_typecheck_compound_type.cpp

@@ -894,7 +894,7 @@ void cpp_typecheckt::typecheck_friend_declaration(
   {
 #ifdef DEBUG
     std::cout << "decl: " << sub_it->pretty() << "\n with value "
-	            << sub_it->value().pretty() << '\n';
+              << sub_it->value().pretty() << '\n';
     std::cout << "  scope: " << cpp_scopes.current_scope().prefix << '\n';
 #endif
     // In which scope are we going to typecheck this?

src/cpp/cpp_typecheck_expr.cpp

@@ -433,7 +433,7 @@ bool cpp_typecheckt::overloadable(const exprt &expr)
       t=t.subtype();
 
     if(t.id()==ID_struct ||
-       //this might be an incomplete struct (template) here
+       // this might be an incomplete struct (template) here
        t.id()==ID_incomplete_struct ||
        t.id()==ID_union ||
        t.id()==ID_c_enum)
@@ -605,7 +605,7 @@ bool cpp_typecheckt::operator_is_overloaded(exprt &expr)
       // We try and fail silently, maybe conversions will work
       // instead.
 
-      //TODO: need to resolve an incomplete struct (template) here
+      // TODO: need to resolve an incomplete struct (template) here
       // go into scope of first operand
       if(expr.op0().type().id()==ID_symbol &&
          follow(expr.op0().type()).id()==ID_struct)
@@ -2394,8 +2394,9 @@ void cpp_typecheckt::typecheck_method_application(
     cpp_saved_template_mapt saved_map(template_map);
     const irept &template_type=tag_symbol.type.find(ID_C_template);
     const irept &template_args=tag_symbol.type.find(ID_C_template_arguments);
-    template_map.build(static_cast<const template_typet &>(template_type),
-		       static_cast<const cpp_template_args_tct &>(template_args));
+    template_map.build(
+      static_cast<const template_typet &>(template_type),
+      static_cast<const cpp_template_args_tct &>(template_args));
     add_method_body(&method_symbol);
 #ifdef DEBUG
     std::cout << "MAP for " << symbol << ":" << std::endl;

src/cpp/cpp_typecheck_method_bodies.cpp

@@ -70,7 +70,7 @@ void cpp_typecheckt::add_method_body(symbolt *_method_symbol)
     return;
   }
   method_bodies.push_back(method_bodyt(
-			      _method_symbol, template_map, instantiation_stack));
+    _method_symbol, template_map, instantiation_stack));
 
   // Converting a method body might add method bodies for methods
   // that we have already analyzed. Hence, we have to keep track.

src/cpp/cpp_typecheck_resolve.cpp

@@ -28,7 +28,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <ansi-c/anonymous_member.h>
 
 #include "cpp_typecheck.h"
-#include "cpp_typecheck_resolve.h"
 #include "cpp_template_type.h"
 #include "cpp_type2name.h"
 #include "cpp_util.h"
@@ -683,9 +682,9 @@ void cpp_typecheck_resolvet::resolve_argument(
   exprt &argument,
   const cpp_typecheck_fargst &fargs)
 {
-  if(argument.id()=="ambiguous") //could come from a template parameter
+  if(argument.id()=="ambiguous") // could come from a template parameter
   {
-    //this must be resolved in the template scope
+    // this must be resolved in the template scope
     cpp_save_scopet save_scope(cpp_typecheck.cpp_scopes);
     cpp_typecheck.cpp_scopes.go_to(*original_scope);
 
@@ -934,7 +933,7 @@ cpp_scopet &cpp_typecheck_resolvet::resolve_scope(
 #ifdef DEBUG
         std::cout << "S: "
                   << cpp_typecheck.cpp_scopes.current_scope().identifier
-                  << std::endl;
+                  << "\n";
         cpp_typecheck.cpp_scopes.current_scope().print(std::cout);
         std::cout << "X: " << id_set.size() <<std::endl;
 #endif