Rafael Sá Menezes

I've looked into it. It seems that the kernel headers uses some compiler builtin functions that we still don't support. They are: - __builtin_types_compatible_p - __builtin_choose_expr - __builtin_offsetof I will...

Partially, the 128bit types were added. However, the intrinsics are still missing

@will-leeson, just add `--verbosity 9`, it should solve it. The issue is that although we should be printing this as STATUS message, it is being printed as a DEBUG. The...

> Which smt solver is your install using by default? If available Boolector. > both fail to output formulas and abort after "Encoding solver time:" is printed That's odd, It...

> gcc-9 has had issues before, maybe we should error in the CMake phase? This happened during the old precompiled irep2. And if you see the message, the optimization will...

@mikhailramalho will https://github.com/esbmc/esbmc/pull/436 solve this?

> I understand that your message_interface_simplify branch converts lots of these to proper output + abort(). I wouldn't like to cause merge conflicts. What are you planning to do with...

@mikhailramalho and @lucasccordeiro Thanks for the reviews! I will actually put it back as a draft, there are 2 features still missing: symbol support and multiple dereference objects. I will...

> we could give it one at the time, then merge them all at the end. I think that a goto-linker would be great.

> I see, can we make ESBMC generate the header instead then? We could, but this is not intended to be complete. It should only expose the functions that users...