Update to CBMC 5.12

[FrNecas]

There have been a lot of changes in this pull request. Below is just a short overview of the most significant ones and some comments:

• Vast abstract interpretation changes, usually required adding explicit initialization to bottom. I was also a bit struggling with constant propagator throwing failed to find state error but it turned out I had to call it a bit differently to make it initialize states.
• Function identifier was removed from goto instruction ( https://github.com/diffblue/cbmc/pull/3126 ) which caused some problems. I usually ended up using the indentifier stored in SSA and passing it around. One case where it behaves slightly differently is inlining (previously the original function was kept even during inlining). This caused issue in trying to ignore __CPROVER_initialize function (mainly the variables assigned in it), we ended up checking for the CPROVER prefix in the variables rather than looking at the functions.
• Removed property checker (https://github.com/diffblue/2ls/commit/5b05f182b8cd1068d2225f4ccfe95e44160c4cc9) required a lot of changes. We also noticed that new assertion status was added (previously it was unknown - ok - fail, now there is also not checked). We ended up sticking with UNKNOWN for now (for compatibility) but this may be a place for potential refactoring (differentiating between not having checked the property and having checked it but not knowing its correctness).
• Significant solver changes - we ended up using the contexts provided by CBMC rather than the previous implementation. This seems to have also sped up the calculations which is great!
• And a lot of other small API and call changes, too many to list them all
• We agreed with @viktormalik to temporarily disable one test ( https://github.com/diffblue/2ls/commit/80deaffc84781171c6e253f35325d10c8ccaa8cc). I've been trying to find the issue in it for hours, however no luck yet and I'd rather get this going again and fix this one small issue (along with true memsafety tests that we disabled some time ago) once it's all done. The formulae pushed to the solver seem to be the same but in the new version it throws UNSAT, whereas in the old it resulted in SAT. Such issues are almost impossible to debug since the solver is basically a black box.

Looking at the CI failures, I will push one more commit with code style fixes (will squash it at the end). I don't really know why compilation with clang++3.7 is failing but it seems to come from CBMC so probably not much I can do about that...

Related: https://github.com/peterschrammel/cbmc/pull/25

[FrNecas]

Thanks for the review, addressed your comments in a separate commit (since it won't be visible in the final commit after squashing anyway)

[FrNecas]

Thanks for the review, I will address your comments tomorrow. I'd also like to merge the CI PR first. As for the -Werror, I don't think 2LS was ever compilable with it. I remember that every time I wanted to debug (by removing the comment in src/config.inc) I would also have to remove -Werror to compile because there were some warnings coming from CBMC and some others from 2LS. Looking at CBMC compilation now, it looks very clean, no warnings as far as I can tell. My plan is to go through the warnings in 2LS once we finish the rebase and fix them, most of them should be fairly simple (missing cases, etc)

[peterschrammel]

My plan is to go through the warnings in 2LS once we finish the rebase and fix them

Makes sense.

[peterschrammel]

Please rebase on the submodule

[FrNecas]

Done, rebased and squashed

[FrNecas]

Thanks for merging. @peterschrammel could you please create 2ls-prerequisites-cbmc-5.37.0 branch on your CBMC fork? In the meantime, I managed to get the rebase up until the latest release and I will hopefully have a PR with final changes soon (the number of changes was not huge). My intention right now is to have 2 more PRs - one with rebase to 5.37.0 and the other fixing the compilation warnings and ideally also fixing some bugs (we would like to give the new version a try on SVcomp suite).

The only problem with the release right now is a regression in heap domain (occurred first with 5.18) which we are currently trying to debug.

[peterschrammel]

could you please create 2ls-prerequisites-cbmc-5.37.0 branch on your CBMC fork?

Done.