Include git revision in version output

[tautschnig]

Replaces #668.

[kroening]

Does the build still work with a tarball?

[tautschnig]

Does the build still work with a tarball?

Yes, it would still work, it would just say "n/a" in place of the git revision.

[mgudemann]

won't this stop the build in case of no git ? If I understand correctly the make build would use n/a as version string in that case.

[tautschnig]

I might have done too much of a copy&paste :-) I'll take another look.

[kroening]

Is the extra header needed?

[tautschnig]

My apologies, that was a left-over that I had forgotten to clean up. It's gone now.

[kroening]

I am somewhat sad that the "X-bit version" output is gone. There are so many support enquiries where someone runs 32-bit and then runs out of memory.

[tautschnig]

I am somewhat sad that the "X-bit version" output is gone.

It isn't! The first line of the banner now says (via the new banner_string function):

* *         CBMC 5.8 (cbmc-5.8-4073-gcc8a7cb) 64-bit        * *

[tautschnig]

Maybe it just needs a bit more spacing? It's easy to fix now, just requires edits in a single place.

[allredj]

Passed Diffblue compatibility checks (cbmc commit: c3e96eb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76907598

[mgudemann]

LGTM now

[chrisr-diffblue]

Looks great in general, and I'd be really pleased to get this in to the code base but I have two queries - one on the CMake builds (commented at the specific location) and a more general comment on the Makefile builds - instead of modifying all the src/*/Makefile files to include the same lines modification of CP_CXXFLAGS, would it be possible to do that in a single place in src/common ?

[chrisr-diffblue]

Does this actually happen on every build? I thought this would only happen on the initial CMake build directory setup operation, but not on subsequent cmake --build operations, which would mean it wouldn't pickup new commits/dirty working directory, etc.... I've not actually tried this though, so I may well be misunderstanding CMake here.

[tautschnig]

I believe you are right. Let me try to figure out how to do it as needed, as is done for Makefiles.

[tautschnig]

I'm actually out of ideas how to accomplish this, or at least how to do so in a portable fashion. I could invoke git via add_custom_command, but then the output needs to be written to a file. The contents of that file must be added to the compiler command line, which seems to be impossible. That leaves as workaround the non-portable option of adding -include some-generated-file to the compiler command-line. I might try this anyhow.

[chrisr-diffblue]

Yeah, it seems Cmake is really unhelpful here :-( I guess another option is to use cmake's 'configure_file' in someway, but even that I think would somehow need to invoke a cmake configure.

[tautschnig]

@chrisr-diffblue I have now cleaned up the Makefile side. I'll take a look at how to sort out the CMake bit.

[chrisr-diffblue]

Very minor nits - would it be any cleaner (no pun intended...) if you just do a CLEANFILES += .release_info somewhere around line 233 instead? Also, is there any milage in using a variable to hold the name of .release_info, as that file name is used in a number of different places in the previous patch hunk? Personally I'm not sure, but thought I'd float the idea anyway.

[tautschnig]

I have introduced a variable instead of the literal file name, but I've refrained from adding it to CLEANFILES as that would have seemed to be just additional code (with the risk of fiddling with a variable that other Makefiles may set).

[chrisr-diffblue]

Rather than setting this on a per target basis in all the CMakeLists.txt files, could it be set once as additional CMAKE_CXX_FLAGS values in the top level CMakeLists.txt ?

[allredj]

Passed Diffblue compatibility checks (cbmc commit: f8096c4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76960554

[tautschnig]

@chrisr-diffblue I have now implemented the CMake side of this, with the inconvenience that those files depending on CBMC_VERSION will be re-buillt every time.

[chrisr-diffblue]

Thanks for working on the CMake problem. I've got a couple of ideas to improve that further (using a combination of CMake in script mode, configure_file, and add_custom_target) but I'll need to have a play around to see if it'll work... One bigger concern though that has just come to my mind is that by adding -D options to the compiler command lines, isn't that going to potentially play badly with ccache? I assume ccache is going to see different values of the git hash and make the assumption it's cached build is invalid. So I think the correct approach should be to generate an actual header file that gets included just like any normal header file.

[tautschnig]

[...] One bigger concern though that has just come to my mind is that by adding -D options to the compiler command lines, isn't that going to potentially play badly with ccache? [...]

Yes, I figured that could be a problem. Hence those flags are now only added very selectively: to exactly those files that really need it. (Both for standard Makefiles and CMake.) I think that should address your concern?

[chrisr-diffblue]

Ah, I missed that change :-) I'll approve now, and if I manage to find a cleaner cmake method, I'll do a separate PR for that.

[allredj]

Passed Diffblue compatibility checks (cbmc commit: 4b124c8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76968515