Maybe we could replace it with a regex? Something like "alloca$\d+".

Maybe we could replace it with a regex? Something like "alloca$\d+".

@intrigus: could you please try this approach?

Maybe we could replace it with a regex? Something like "alloca$\d+".

@intrigus: could you please try this approach?

I will not try this approach as it's also not complete, i.e. a function called alloca$111 would still fail.
I don't have the time for a complete solution and the alloca handling in esbmc looks pretty broken anyway.

The main motivation for this PR is to unblock my c++ code that uses std::allocator.

Maybe we could replace it with a regex? Something like "alloca$\d+".

@intrigus: could you please try this approach?

I will not try this approach as it's also not complete, i.e. a function called alloca$111 would still fail. I don't have the time for a complete solution and the alloca handling in esbmc looks pretty broken anyway.

That would generate "alloca$111$", no?

The main motivation for this PR is to unblock my c++ code that uses std::allocator.

Thanks, @intrigus.

I have asked Rafael to submit another PR with his proposal.

Thanks for submitting this PR, @intrigus-lgtm.

The main motivation for this PR is to unblock my c++ code that uses std::allocator.

Thanks, @intrigus.

I have asked Rafael to submit another PR with his proposal.

Sorry, for not being more helpful, just pretty busy and keeping my thesis' deadline in mind.