- 22 Jan, 2022 2 commits
-
-
Sylvain Boulmé authored
-
Sylvain Boulmé authored
-
- 17 Jan, 2022 1 commit
-
-
Sylvain Boulmé authored
-
- 07 Dec, 2020 1 commit
-
-
Sylvain Boulmé authored
-
- 03 Dec, 2020 3 commits
-
-
Sylvain Boulmé authored
-
Sylvain Boulmé authored
-
Sylvain Boulmé authored
-
- 16 Nov, 2020 1 commit
-
-
Xavier Leroy authored
-
- 14 Nov, 2020 2 commits
-
-
Xavier Leroy authored
Stopping on warnings is useful for development builds, but unhelpful for released software.
-
Xavier Leroy authored
-
- 09 Nov, 2020 1 commit
-
-
Xavier Leroy authored
-
- 08 Nov, 2020 1 commit
-
-
Xavier Leroy authored
-
- 07 Nov, 2020 1 commit
-
-
Bernhard Schommer authored
The semantics of the various selection functions are defined analogously to the ones from the type generic sel function. The semantics for the various high word multiplication functions is defined using the Integer functions. Bug 30035
-
- 06 Nov, 2020 2 commits
-
-
Bernhard Schommer authored
These comparisons are supported in the hybrid 64 bit mode. Bug 30035
-
Bernhard Schommer authored
The two built-in function map to the fmax and fmin instruction. Bug 30035
-
- 01 Nov, 2020 1 commit
-
-
Xavier Leroy authored
-
- 30 Oct, 2020 1 commit
-
-
Xavier Leroy authored
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.
-
- 12 Oct, 2020 2 commits
-
-
Xavier Leroy authored
This is the left inverse of `ident_to_string`. Closes: #372
-
Xavier Leroy authored
It is specific to AbsInt's commercial version of CompCert.
-
- 05 Oct, 2020 1 commit
-
-
Xavier Leroy authored
- Add support for the Win64 ABI to the x86_64 port - Update vararg support to handle Win64 conventions - Configure support for x86_64-cygwin64
-
- 22 Sep, 2020 3 commits
-
-
Xavier Leroy authored
Use different combination of options for different test files.
-
Xavier Leroy authored
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).
-
Xavier Leroy authored
Variables were confused for temporaries, causing the temporaries introduced by this pass to be very big integers. Fixes: #370
-
- 21 Sep, 2020 2 commits
-
-
Xavier Leroy authored
configure flags -use-external-Flocq and -use external-MenhirLib.
-
Xavier Leroy authored
-
- 20 Sep, 2020 1 commit
-
-
Bernhard Schommer authored
Also: improve check for ptr - integer. (Added by Xavier Leroy <xavier.leroy@college-de-france.fr>)
-
- 18 Sep, 2020 1 commit
-
-
Maxime Dénès authored
Previous scripts were relying on the order in which apply's HO unification performs reductions, for a goal that could be solved by reflexivity.
-
- 04 Aug, 2020 1 commit
-
-
Michael Schmidt authored
-
- 30 Jul, 2020 2 commits
-
-
Christoph Cullmann authored
-
Christoph Cullmann authored
-
- 29 Jul, 2020 1 commit
-
-
Xavier Leroy authored
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.
-
- 27 Jul, 2020 9 commits
-
-
Bernhard Schommer authored
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.
-
Xavier Leroy authored
-
Xavier Leroy authored
__builtin_sqrt (no "f") is the name used by GCC and Clang.
-
Xavier Leroy authored
Share the testing code for built-in functions that are available on all target platforms. Improve testing of __builtin_clz* and __builtin_ctz*
-
Xavier Leroy authored
These functions are now available on all targets.
-
Xavier Leroy authored
Using the "rbit" instruction (reverse bits).
-
Xavier Leroy authored
Using binary search loops expanded at point of use.
-
Xavier Leroy authored
-
Xavier Leroy authored
__builtin_fabs has already been expanded in backend/Selection.v .
-