c2goto
------
This directory contains three related things:

1. The sources of the `c2goto` compiler, which translates C sources into a
   binary representation of the GOTO language used internally by ESBMC to
   represent programs in imperative languages.

2. The support code for loading the GOTO binaries and providing their contents
   to the rest of ESBMC. Together with item 1. these provide methods to embed
   and use pre-compiled versions of operational models in ESBMC to
   support programs using libraries.

3. In the `library` subdirectory, some (but not all; see
   `src/goto-programs/builtin_functions.cpp` for more details) operational models
   of functions from the C standard library and pthreads. These models make use
   of specialized type and function prototype definitions that are located in
   the `headers` subdirectory. The sources in the `library` subdirectory are
   translated by the `c2goto` compiler for some architectures into GOTO
   binaries, which are then bundled with the ESBMC binary.
   They are also bundled verbatim (i.e., as text) and used to provide models
   on architectures for which no GOTO binary representation has been generated
   at compile time.

   The `headers` are also bundled with ESBMC and used to pre-process the
   to-be-verified programs. That means any header and any type therein that
   overrides those provided by the operating system ESBMC is running on will
   be used instead. E.g., `headers/pthread.h` defines a type `pthread_t`, which
   differs from those types provided by Glibc, MinGW, or on MacOS. This ESBMC
   specific type will be used when running ESBMC on programs like this:
   ```c
   #include <pthread.h>

   void *job(void *);

   int main()
   {
     pthread_t t;
     pthread_create(&t, NULL, job, NULL);
   }
   ```

   The same holds for all other types and prototypes defined in `headers`.

   These headers in plain text are bundled with the ESBMC executable and
   extracted into a temporary directory before the given program is
   preprocessed. The list of included paths for this preprocessing is constructed
   such that they are processed in the following order:
   1. any `-I` paths from the ESBMC invocation,
   2. the temporary directory containing all from `headers`,
   3. Clang's bundled headers (such as `stddef.h`, etc.),
   4. the default system include paths, such as `/usr/local/include` and
      `/usr/include`, and finally
   6. any `--idirafter` paths from the invocation.

   Depending on compile- and/or runtime options, there may be additional paths
   inserted into a specific step, usually just the first.

   Since the contents of `headers` are used before the standard paths of the
   system's includes, this allows the above mentioned overriding of system
   headers (but not of those given by the user via `-I`, only `--idirafter`).
   This is why the concrete paths of header files in this subdirectory
   matters. The `CMakeLists.txt` therein contains specifics about which system
   header gets overwritten.
