I've tried this change and it seems simpler.

diff --git a/src/clang-c-frontend/clang_c_convert.cpp b/src/clang-c-frontend/clang_c_convert.cpp
index ae85035ba..bba58abb0 100644
--- a/src/clang-c-frontend/clang_c_convert.cpp
+++ b/src/clang-c-frontend/clang_c_convert.cpp
@@ -3408,6 +3408,7 @@ void clang_c_convertert::get_decl_name(
     return;
   }
 
+  case clang::Decl::CXXConstructor:
   case clang::Decl::Var:
     if (name.empty())
     {

This change is also fixed:

- regression/esbmc-cpp/cpp/ch20_7
- regression/esbmc-cpp/gcc-template-tests/union1

@intrigus-lgtm: we have open positions within our research group. Please do get in touch if you're looking for a research position in software verification ;-) Here is my email address: lucas.cordeiro@manchester.ac.uk

I've tried this change and it seems simpler.

diff --git a/src/clang-c-frontend/clang_c_convert.cpp b/src/clang-c-frontend/clang_c_convert.cpp
index ae85035ba..bba58abb0 100644
--- a/src/clang-c-frontend/clang_c_convert.cpp
+++ b/src/clang-c-frontend/clang_c_convert.cpp
@@ -3408,6 +3408,7 @@ void clang_c_convertert::get_decl_name(
     return;
   }
 
+  case clang::Decl::CXXConstructor:
   case clang::Decl::Var:
     if (name.empty())
     {

This change is also fixed:

- regression/esbmc-cpp/cpp/ch20_7
- regression/esbmc-cpp/gcc-template-tests/union1

That change appears wrong to me.
First, casting to VarDecl here (https://github.com/esbmc/esbmc/pull/1753/files#diff-77a14a166a14947af9a9605e058ed20d935cf5200891234187cf015166925590R3416) is UB as CXXConstructorDecl does not have VarDecl as one of its bases.
This can be fixed by casting to DeclaratorDecl instead (common base).
However, this brings us to the second problem:
getFullyQualifiedName (https://github.com/esbmc/esbmc/pull/1753/files#diff-77a14a166a14947af9a9605e058ed20d935cf5200891234187cf015166925590R3425) simply returns "void () noexcept".
So two anonymous (struct) constructors would have the same id, which I would assume is bad?

So two anonymous (struct) constructors would have the same id, which I would assume is bad?

Yes, definitely bad. ESBMC maintains a set of symbols whose id should be unique in the so-called context. Symbols with the same id in different translation units are allowed (and handled by c_link()), but they better have the same definition (ODR). Within a single context, as is built by the frontend, the id must be unique.

simply returns "void () noexcept".
So two anonymous (struct) constructors would have the same id, which I would assume is bad?

Yes, you are right. For reference, you can also verify that the constructor is valid using the following code, there doesn't seem to be a constructor call in your TCs.

main (c:@F@main#):
        // 20 file main9.cpp line 6 column 3 function main
        struct __anon_struct_at_main9_cpp_main_6_3 unnamed_struct;
        // 21 file main9.cpp line 6 column 3 function main
        unnamed_struct={ .field1=10, .field2=2.050000e+1f };

#include <cassert>

int main()
{
  // Define and initialize an unnamed struct
  struct
  {
    int field1 = 10;
    float field2 = 20.5;
  } unnamed_struct;

  // Access and verify the fields of the unnamed struct
  assert(unnamed_struct.field1 == 10);
  assert(unnamed_struct.field2 == 20.5f);

  return 0;
}

So two anonymous (struct) constructors would have the same id, which I would assume is bad?

Yes, definitely bad. ESBMC maintains a set of symbols whose id should be unique in the so-called context. Symbols with the same id in different translation units are allowed (and handled by c_link()), but they better have the same definition (ODR). Within a single context, as is built by the frontend, the id must be unique.

Well, I just learned this the hard way 😆
I had a very weird "function call: not enough arguments" error, because there were two functions with the same id and one function had an extra argument and so the functions got mixed up...

I added a testcase where the anon constructor is actually used.
So this should (hopefully) be ready for merging.

Well, I just learned this the hard way 😆
I had a very weird "function call: not enough arguments" error, because there were two functions with the same id and one function had an extra argument and so the functions got mixed up...

I believe there should've been some c_link warnings in the log at least. It's not ideal, but I don't have a good solution right now except for just rejecting the input. Though I'm pretty sure that would break things elsewhere (e.g. one TU declaring int f(void) and another one int f()). Better leave c_link adjustments for another PR.

Fixed the two known-bug cases.
Now I just have to move it to cpp_converter.

Well, I just learned this the hard way 😆
I had a very weird "function call: not enough arguments" error, because there were two functions with the same id and one function had an extra argument and so the functions got mixed up...

I believe there should've been some c_link warnings in the log at least. It's not ideal, but I don't have a good solution right now except for just rejecting the input. Though I'm pretty sure that would break things elsewhere (e.g. one TU declaring int f(void) and another one int f()). Better leave c_link adjustments for another PR.

The ids were in the same TU and at the very same position. The only difference were the arguments to the constructor calls. (I initially ignored the arguments and only generated an id based on the name of the type. Therefore conflating constructors with different arguments)

I see a lot of duplicated code in this function, can you unify the naming generation of these switch cases?

I have created #1762 for that as well as the wrong comment.
(All existing comments in that method are wrong)

I don't have time to work on this right now and I don't think that any of that should really block this pr.

It's a very small request and I prefer we don't add any more duplicated code when we can easily not do it.
…
On Wed, 27 Mar 2024, 16:50 intrigus-lgtm, @.> wrote: I see a lot of duplicated code in this function, can you unify the naming generation of these switch cases? I have created #1762 <#1762> for that as well as the wrong comment. (All existing comments in that method are wrong) I don't have time to work on this right now and I don't think that any of that should really block this pr. — Reply to this email directly, view it on GitHub <#1753 (comment)>, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKEJHZWW4LYMIUKQX43WT3Y2MIINAVCNFSM6AAAAABE4IXZDKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDAMRTHA2DGMRSGY . You are receiving this because you commented.Message ID: @.>

I'm really sorry, but I really don't know how to merge the switch cases.
The cases are pretty different, and there are some subtle differences between the cases regarding ids and so on.
I don't have the time to investigate whether I will break anything when changing that.

Also, instead of generating the id manually, it could be possible to always just use generateUSRForDecl.
But again, I don't want to risk breaking anything and don't have time to investigate any potential fallout of these potential changes.
If you can tell me in sufficient detail how you'd want to merge the switch cases I'm more than happy to apply that.
(You should also be able to just push any changes you want to my branch considering that you are afaik a maintainer)