When running unit tests with the CompCert reference interpreter, it's nice to be able to start execution at a given test function instead of having to write a main function.

This PR adds a -main command-line option to give the name of the entry point function. The default is still main. Frama-C has a similar option.

The function specified with -main is called with no arguments. If its return type is int, its return value is the exit status of the program. Otherwise, its return value is ignored and the program exits with status 0.

This is the left inverse of `ident_to_string`.

Closes: #372

It is specific to AbsInt's commercial version of CompCert.

- Add support for the Win64 ABI to the x86_64 port
- Update vararg support to handle Win64 conventions
- Configure support for x86_64-cygwin64

Use different combination of options for different test files.

And also for the computations in name_temporary.
Overflowing OCaml's integer types is unlikely in actual use but
happened in the past owing to another mistake (see issue #370).

Variables were confused for temporaries, causing the temporaries introduced
by this pass to be very big integers.

Fixes: #370

configure flags -use-external-Flocq and -use external-MenhirLib.

Also: improve check for ptr - integer.
(Added by Xavier Leroy <xavier.leroy@college-de-france.fr>)

Previous scripts were relying on the order in which apply's HO
unification performs reductions, for a goal that could be solved by
reflexivity.

32-bit executables cannot be built since XCode 10.0 (sep 2018).
32-bit executables cannot be executed since MacOS 10.15 (oct 2019).
Better remove x86-32 support and fail at configuration time instead of
at the end of the build.

Not all pre-processors concatenate string literal lists, however they
are allowed in _Static_assert. This is similar to the rules for inline
assembly etc.

__builtin_sqrt (no "f") is the name used by GCC and Clang.

Share the testing code for built-in functions that are available on
all target platforms.
Improve testing of __builtin_clz* and __builtin_ctz*

These functions are now available on all targets.

Using the "rbit" instruction (reverse bits).

Using binary search loops expanded at point of use.

__builtin_fabs has already been expanded in backend/Selection.v .

We check that this builtin function is only called from within a variadic
function and has the correct number of arguments.

Added error descriptions for the new syntax errors introduced by
'_Static_assert'.

Returns 1 if the argument is a constant expression, 0 otherwise.

Closes: #366

We check in the initial environment if a function is already defined to
avoid redefinition of functions that are part of the builtin
environment.

If ocamlopt is not available, use ocamlc instead of ocamlopt to build
auxiliary tools (tools/modorder, tools/ndfun).

This is a follow-up to commit 9af28924.

This is a follow-up to commit 3b1f3dd5, which was wrong in that
errors in a shell pipeline were not correctly detected.

Fixes: #363

This reverts commit 1a01ad62.

The version string dumped in the file should be the same as the version
string printed by `-version`. The option is also not printed by `-help`
since it is for internal use only.