Prevent users from misusing CMake

When CMake is invoked from the source directory it will overwrite files
in there. In general CMake expects to be used for out-of-source builds.
Previously it was still possible to get this wrong by accident, this
just adds a check to prevent this from happening and tells people what
to do instead.

Author: Hannes Steffenhagen

CMakeLists.txt

@@ -1,5 +1,13 @@
 cmake_minimum_required(VERSION 3.2)
 
+# If cbmc generates files inside of the cbmc source directory this can lead to important files being overwritten, so we prevent that here
+if("${CMAKE_BINARY_DIR}" STREQUAL "${CMAKE_SOURCE_DIR}")
+  message(FATAL_ERROR
+    "Do not generate CMake files inside of the cbmc source directory."
+    " Please either create a separate build directory and invoke cbmc from there, or specify a build directory with -B."
+    " (see also: COMPILING.md)")
+endif()
+
 # Build a Release version by default (default build flags for each build type
 # are configured below).
 if (NOT EXISTS ${CMAKE_BINARY_DIR}/CMakeCache.txt)
@@ -8,6 +16,7 @@ if (NOT EXISTS ${CMAKE_BINARY_DIR}/CMakeCache.txt)
     endif()
 endif()
 
+
 # Grab the current CBMC version from config.inc
 # We do this so we have a matching cbmc version between the Makefile build and
 # the CMake build. This version info is useful for things like generating