Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Add proof of splitlong_ptr32 | Yann Herklotz | 2020-11-27 | 1 | -0/+3 |
| | |||||
* | Add Verilog backend | Yann Herklotz | 2020-11-27 | 33 | -0/+16929 |
| | |||||
* | Always try inlining functions | Yann Herklotz | 2020-11-27 | 1 | -4/+1 |
| | |||||
* | Ignore unnecessary folders | Yann Herklotz | 2020-11-27 | 2 | -1/+1 |
| | |||||
* | Updates for release 3.8v3.8 | Xavier Leroy | 2020-11-16 | 3 | -5/+10 |
| | |||||
* | Do not use -warn-error when building from a release tarball | Xavier Leroy | 2020-11-14 | 1 | -2/+9 |
| | | | | | Stopping on warnings is useful for development builds, but unhelpful for released software. | ||||
* | Support Coq 8.12.1 | Xavier Leroy | 2020-11-14 | 2 | -3/+3 |
| | |||||
* | Update README | Xavier Leroy | 2020-11-09 | 1 | -4/+4 |
| | |||||
* | Update Changes | Xavier Leroy | 2020-11-08 | 1 | -0/+48 |
| | |||||
* | Added semantics for the PowerPC sel and mulh built-ins | Bernhard Schommer | 2020-11-07 | 1 | -4/+44 |
| | | | | | | | | 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 | ||||
* | Added missing printer for PowerPC 64 bit comparison. | Bernhard Schommer | 2020-11-06 | 1 | -0/+8 |
| | | | | | These comparisons are supported in the hybrid 64 bit mode. Bug 30035 | ||||
* | Added implementation for fmin/fmax for aarch64. | Bernhard Schommer | 2020-11-06 | 3 | -0/+12 |
| | | | | | The two built-in function map to the fmax and fmin instruction. Bug 30035 | ||||
* | Better "make clean" | Xavier Leroy | 2020-11-01 | 1 | -1/+1 |
| | |||||
* | Add -main option to specify entrypoint function in interpreter mode (#374) | Xavier Leroy | 2020-10-30 | 4 | -20/+42 |
| | | | | | | | 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. | ||||
* | Add `string_of_ident` conversion | Xavier Leroy | 2020-10-12 | 1 | -0/+110 |
| | | | | | | This is the left inverse of `ident_to_string`. Closes: #372 | ||||
* | Remove -version-file option | Xavier Leroy | 2020-10-12 | 1 | -19/+2 |
| | | | | It is specific to AbsInt's commercial version of CompCert. | ||||
* | Support Cygwin 64 bits | Xavier Leroy | 2020-10-05 | 17 | -118/+415 |
| | | | | | | - Add support for the Win64 ABI to the x86_64 port - Update vararg support to handle Win64 conventions - Configure support for x86_64-cygwin64 | ||||
* | Test clightgen with -short-idents and -normalize options | Xavier Leroy | 2020-09-22 | 1 | -0/+6 |
| | | | | Use different combination of options for different test files. | ||||
* | Use exact arithmetic for printing positive numbers | Xavier Leroy | 2020-09-22 | 1 | -52/+56 |
| | | | | | | 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). | ||||
* | Fix computation of next temporary in -canonical-idents mode | Xavier Leroy | 2020-09-22 | 1 | -1/+12 |
| | | | | | | | Variables were confused for temporaries, causing the temporaries introduced by this pass to be very big integers. Fixes: #370 | ||||
* | Support the use of already-installed MenhirLib and Flocq libraries | Xavier Leroy | 2020-09-21 | 11 | -67/+82 |
| | | | | configure flags -use-external-Flocq and -use external-MenhirLib. | ||||
* | No need for -R options, _CoqProject contains them already | Xavier Leroy | 2020-09-21 | 1 | -4/+2 |
| | |||||
* | Check ptr arithmetic for ++ and -- | Bernhard Schommer | 2020-09-20 | 1 | -10/+16 |
| | | | | | Also: improve check for ptr - integer. (Added by Xavier Leroy <xavier.leroy@college-de-france.fr>) | ||||
* | Simplify two scripts in Zbits (#369) | Maxime Dénès | 2020-09-18 | 1 | -2/+2 |
| | | | | | Previous scripts were relying on the order in which apply's HO unification performs reductions, for a goal that could be solved by reflexivity. | ||||
* | Add new static-assert token for deLexer utility; bug 29273 | Michael Schmidt | 2020-08-04 | 1 | -0/+1 |
| | |||||
* | Add comments we missed to sync to GitHub | Christoph Cullmann | 2020-07-30 | 1 | -0/+2 |
| | |||||
* | Add missing comment for print_version_file_and_exit | Christoph Cullmann | 2020-07-30 | 1 | -0/+1 |
| | |||||
* | Remove support for x86-32 under macOS | Xavier Leroy | 2020-07-29 | 2 | -45/+3 |
| | | | | | | | 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. | ||||
* | Allow string_literals_list in _Static_assert. | Bernhard Schommer | 2020-07-27 | 2 | -24/+25 |
| | | | | | | 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. | ||||
* | Add test for __builtin_sqrt and __builtin_fabsf | Xavier Leroy | 2020-07-27 | 2 | -0/+7 |
| | |||||
* | Add __builtin_sqrt as synonymous for __builtin_fsqrt | Xavier Leroy | 2020-07-27 | 7 | -5/+8 |
| | | | | __builtin_sqrt (no "f") is the name used by GCC and Clang. | ||||
* | Refactor regression testing of built-in functions | Xavier Leroy | 2020-07-27 | 13 | -110/+447 |
| | | | | | | Share the testing code for built-in functions that are available on all target platforms. Improve testing of __builtin_clz* and __builtin_ctz* | ||||
* | Move declarations of __builtin_clz* and __builtin_ctz* to C2C.ml | Xavier Leroy | 2020-07-27 | 5 | -46/+12 |
| | | | | These functions are now available on all targets. | ||||
* | AArch64 implementation of __builtin_ctz* | Xavier Leroy | 2020-07-27 | 3 | -1/+11 |
| | | | | Using the "rbit" instruction (reverse bits). | ||||
* | RISC-V implementation of __builtin_clz* and __builtin_ctz* | Xavier Leroy | 2020-07-27 | 2 | -0/+134 |
| | | | | Using binary search loops expanded at point of use. | ||||
* | Add support for __builtin_fabsf | Xavier Leroy | 2020-07-27 | 4 | -0/+13 |
| | |||||
* | No need to process __builtin_fabs in $ARCH/Asmexpand.ml | Xavier Leroy | 2020-07-27 | 5 | -12/+0 |
| | | | | __builtin_fabs has already been expanded in backend/Selection.v . | ||||
* | More checks for __builtin_va_start (#250) | Bernhard Schommer | 2020-07-21 | 1 | -6/+10 |
| | | | | We check that this builtin function is only called from within a variadic function and has the correct number of arguments. | ||||
* | cparser/handcrafted.messages: missing blank line | Xavier Leroy | 2020-07-21 | 1 | -0/+1 |
| | |||||
* | Updated handcrafted.messages. | Bernhard Schommer | 2020-07-21 | 1 | -0/+108 |
| | | | | | Added error descriptions for the new syntax errors introduced by '_Static_assert'. | ||||
* | Support _Static_assert from C11 | Xavier Leroy | 2020-07-21 | 7 | -1060/+1116 |
| | |||||
* | Support __builtin_constant_p as in GCC and Clang (#367) | Xavier Leroy | 2020-07-21 | 1 | -0/+10 |
| | | | | | Returns 1 if the argument is a constant expression, 0 otherwise. Closes: #366 | ||||
* | Use the correct location for Slabaled in transform. | Bernhard Schommer | 2020-07-21 | 1 | -2/+2 |
| | |||||
* | Added error for redefined builtin. | Bernhard Schommer | 2020-07-20 | 3 | -0/+6 |
| | | | | | | We check in the initial environment if a function is already defined to avoid redefinition of functions that are part of the builtin environment. | ||||
* | Added missing semicolon. | Bernhard Schommer | 2020-07-15 | 1 | -1/+1 |
| | |||||
* | Bytecode-only build, continued | Xavier Leroy | 2020-07-15 | 1 | -0/+9 |
| | | | | | | | 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. | ||||
* | Revised detection of menhirLib directory, continued (#365) | Xavier Leroy | 2020-07-15 | 1 | -4/+4 |
| | | | | | | | This is a follow-up to commit 3b1f3dd5, which was wrong in that errors in a shell pipeline were not correctly detected. Fixes: #363 | ||||
* | No trailing commas for --version-file option. | Bernhard Schommer | 2020-07-09 | 1 | -1/+1 |
| | |||||
* | Fix typo. | Bernhard Schommer | 2020-07-08 | 1 | -1/+1 |
| | |||||
* | Revert "Use the same version string." | Bernhard Schommer | 2020-07-08 | 1 | -3/+10 |
| | | | | This reverts commit 1a01ad629109cdb60fddae3787e3a589d20e9790. |