Add Makefile build system. This will be used to test that the

[delcypher]

Add Makefile build system. This will be used to test that the sources files can actually be built by clang and/or gcc.

See Makefile-README.md for documentation.

The warning flags passed to the compiler are based on the
check script which we can probably remove as the build
system superseeds that script.

Note WARNINGS_AS_ERRORS is set to off by default because
a lot of the benchmarks would fail to compile otherwise.

This work addresses the first point is #37

[delcypher]

Please note I haven't finished testing if everything builds yet but I wanted to show my work to you all as soon as possible so that I can get early feedback.

@tautschnig
I'd appreciate if you could take a look at this as this work is based off your script. The build system mostly supersedes your script but it doesn't have the automatic "blacklisting" functionality. The build system supports blacklisting benchmarks (IGNORE_SRCS variable) but this must be done by hand currently. If this gets merged in what would you like to do with your script.

@zvonimir
You might find the clang support useful here, especially the EMIT_LLVM option.

[delcypher]

@dbeyer
Oh, you merged that quickly. I was hoping for some feedback first :)

I'll carry on hacking. I need to check that with gcc the whole build succeeds. With clang I already found a bunch of issues so expect a bunch of PRs or issues to be raised soon.

[dbeyer]

@dan: Isn't a merge the best feedback you can get? ;-)

[zvonimir]

Hi Dan,
This is great and would certainly be helpful to have!
Btw, are you trying to compile all benchmarks, or just the ones actually used in the competition?
We have noticed some benchmarks used in the competition that clang cannot compile. We'll submit patches for those this week. However, if I remember correctly, there are benchmarks in the repo that are actually not used in the competition, and if I remember correctly form last year, a bunch of those cannot compile. I suggest you focus only on the benchmarks that are actually used in the competition. Thanks!

[delcypher]

Btw, are you trying to compile all benchmarks, or just the ones actually used in the competition?

I'm trying to compile pretty much everything (*.i files supersede *.c files though). After quite a bit of work I've managed to get everything to build with gcc.

@dbeyer Why are there sources files left lying around that aren't used in the competition? We have version control so I would recommend just deleting source files that aren't used in the competition or moving them into a directory(ies) that won't be traversed by the build system (you could create a old/ directory that mirrors the structure of the existing, e.g. old/array-examples/ old/ldv-memsafety)

[PhilippWendler]

The .c files are valuable when one needs to look at the source for example to identify where a given counterexample is real or not, because these files are often better readable than the corresponding .i file. The .set files contain the exact information which files are part of SV-Comp and which are not, thus no need to move the other files out of the way.

Furthermore, the repository is not exclusively for SV-Comp only, but a more general repository of benchmarks (for example, there are also the repositories in the clauses repository).