Add workaround for alpine regression test failure

[hannes-steffenhagen-diffblue]

CBMC doesn't handle assert on alpine-linux correctly.
This works around this issue by using __CPROVER_assert
directly in the tests that were previously failing.

This appears to be fixed already on the develop branch

[tautschnig]

Would it be possible to take a look at #974?

[hannes-steffenhagen-diffblue]

@tautschnig That's probably the right thing to do for develop, but getting that onto goto-analyzer-develop would be quite a bit of a hassle (and might actually cause problems for when we do a merge in the future). This is just a bandaid measure to make travis happy in the meantime.

[tautschnig]

I'm afraid it will be a pain either way, unless you never want to merge into or from develop (but then really this project shouldn't be living here but instead be a proper fork). If you place fixes in goto-analyzer-develop that you don't want to port to develop then you're left with the problem of what (not) to cherry-pick.

Welcome to the beautiful world of "we'll rebase later..."

[thk123]

I don't think this is a case of fixed on develop just that the alpine linux build has been turned off.

I think this is a reasonable approach, but if @tautschnig is concerned about clashing changes when G-A-D is merged into develop, then you could similarly satisfy Travis by just dumping the Alpine build (or even better, cherry pick the PR(s) that modified the travis build).

[tautschnig]

I don't mean to stop you from merging this into G-A-D, but wouldn't want to see it in develop (as I believe #974 is the way to go - but of course I'm biased :-) ).

[hannes-steffenhagen-diffblue]

@tautschnig I don't disagree. #974 is the right thing to do here, once that's merged something like this won't be needed on develop. Though it's a fairly benign change either way. I don't feel too strongly about doing this exact change, but I figured it'd be good to be able to get travis to not fail by default without completely disabling alpine builds or replicating #974 for GOA (which would be more work as the relevant files have diverged between develop and GOA).

[martin-cs]

Just for a sense of completeness. I'm not planning on trying to merge g-a-d into develop. I've been sectioning bits of it up, PRing them and rebasing. The hope is that the distance between them will slowly reduce and eventually g-a-d will be able to rebase-track develop (or, maybe on one bright day in the future, not actually be needed any more!).

[martin-cs]

That said ... I have been moving regression tests over wholesale so ... If @tautschnig doesn't want this in develop at all then I'm mildly reluctant to merge it somewhere I will forget and then attempt to merge it to develop.

Other thoughts : what is actually blocking #974 ? Also, does anyone actually care about Alpine support? Last time I heard, the One Important User who wanted it originally didn't care any more as they'd moved their docker containers to Ubuntu.

[tautschnig]

Other thoughts : what is actually blocking #974 ? Also, does anyone actually care about Alpine support?

From my point of view #974 is just blocked by lack of attention. Indeed the Alpine failure just highlighted more problems that #974 now seeks to address.

[martin-cs]

Not a code owner for #974 I'm afraid but @peterschrammel is and maybe he'll get this message and have time to take action...