[Don't merge] Add cron jobs for sanitizers and libc++ debug mode

[reuk]

This PR adds stages for address and undefined-behavior sanitizer, and for the libc++ debug mode. These stages should only run during a cron job.

Obviously don't merge this until we know that the stages work properly...

I think the input of @chrisr-diffblue, @owen-jones-diffblue, @zemanlx would be especially useful on this PR.

[owen-mc-diffblue]

How about one with USE_DSTRING set to false? Or is that not working at the moment?

[reuk]

I tried this out the other day and I couldn't get it working completely. @thk123 might have continued working on this though.

[chrisr-diffblue]

You can probably run ctest with -j2 to get a bit of parallelisation of tests.

[reuk]

@zemanlx Could you enable a nightly run of CBMC's CI?
I'm going to push a commit which removes the if: type = cron lines so that we can check the builds actually work, but I'll drop the commit once the builds work, the cron job is enabled, and this is ready to merge.

[chrisr-diffblue]

Is sudo really required? I don't see what you are doing that does need that, and I think adding the requirement for sudo means we get slower job startup? (i.e. sudo requires a full VM that travis estimate as a 30-50 second startup, where as sudo not required just means firing up a container which is 1-6s). Only other consideration is that sudo-required machines get more RAM allocation, according to: https://docs.travis-ci.com/user/reference/overview/

[reuk]

I'll try without sudo and see how it goes

[chrisr-diffblue]

Same query regarding sudo here.

[chrisr-diffblue]

Would it be possible to add an additional CMakeFiles build configuration (like we have ReleaseWithDebug) for the sanitised builds, and for the libcpp debug builds, and then just build/test those targets in these travis jobs? The only reason I ask is that would then give people a (possibly) nicer way to run sanitizer/debug builds locally.

[reuk]

I had a go at this. There's now Sanitized and LibCPPDebug configurations. The sanitized build enables asan and ubsan, while the libcppdebug config passes the debug flags for libc++ and libstdc++. These configs should work on (modern versions of) both g++ and clang++, so we don't lock the configs to specific compilers.

Also worth mentioning: I put the new configurations inside a conditional block, so that superprojects can define their own configurations without having them overridden by CBMC.

[tautschnig]

@reuk is the "Don't merge" in the subject still accurate? Arguably I can't yet be merged as the clang "sanitized" build fails with "argument unused during compilation: ..." -- will you be looking into this?

[tautschnig]

Also, would you mind adding "Fixes: #832" to one of the commit messages (if my assertion that that issue would be fixed is actually true).

[reuk]

"Don't merge" is accurate until I've managed to get the extra checks to pass CI, and the cron job has been enabled in Travis. For the time being, I'm just going to disable the 'unused command line argument' error, as I can't reproduce it locally. The argument could be made for being more conservative with the include paths we use for each library, but I can't fix this unless I can reproduce the build locally.

[owen-mc-diffblue]

I gather this has been superseded by #1642