Mikhail R. Gadelha

Indeed, it just might be a bit tricky to implement... A couple of questions: 1. Are we disabling constant propagation for that variable? For instance, do we expect to see...

Oh, I see, so we only care about assignments where the lhs is marked as no_slice. That should be simple to implement, I guess another attribute in symbolt does the...

> @fbrausse, @mikhailramalho and @rafaelsamenezes: do you still have comments for this PR? > > @rafaelsamenezes: could you please run this PR over the SV-COMP benchmarks? Yes, there are still...

__VERIFIER_assert is actually a function in SV-COMP that eventually calls abort, e.g., https://github.com/sosy-lab/sv-benchmarks/blob/master/c/verifythis/elimination_max.c#L10 __ESBMC_assert should generate an assertion at goto level, if it isn't, that's probably a bug. The conversion...

Can you upload the goto program of the program you're using?

I will again vote against introducing more complexity to the frontend :) Can we fix that on the linking stage? `c_linkt` goes through all symbols, so we could improve it...

Cool, I'll take a look. I was also thinking about another solution (which was the previous approach before I wrote the clang frontend): instead of adding the full struct/union/class type,...

> @mikhailramalho Yes, I was also thinking about exactly that! Have all types symbolically in the beginning from the frontend and the the linker will have a much easier time...

Keeping the symbols around would also simplify the frontend slightly, as in we could remove https://github.com/esbmc/esbmc/blob/master/src/clang-c-frontend/clang_c_convert.cpp#L985. I remember having a terrible time making it work consistently a few years ago...

Yeah, I got that, but `goto_convert_functionst::thrash_type_symbols()` already does number 2: https://github.com/esbmc/esbmc/blob/master/src/goto-programs/goto_convert_functions.cpp#L377