aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* Use exact arithmetic for printing positive numbersXavier Leroy2020-09-221-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 modeXavier Leroy2020-09-221-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 librariesXavier Leroy2020-09-2111-67/+82
| | | | configure flags -use-external-Flocq and -use external-MenhirLib.
* No need for -R options, _CoqProject contains them alreadyXavier Leroy2020-09-211-4/+2
|
* Check ptr arithmetic for ++ and --Bernhard Schommer2020-09-201-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ès2020-09-181-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 29273Michael Schmidt2020-08-041-0/+1
|
* Add comments we missed to sync to GitHubChristoph Cullmann2020-07-301-0/+2
|
* Add missing comment for print_version_file_and_exitChristoph Cullmann2020-07-301-0/+1
|
* Remove support for x86-32 under macOSXavier Leroy2020-07-292-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 Schommer2020-07-272-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_fabsfXavier Leroy2020-07-272-0/+7
|
* Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-277-5/+8
| | | | __builtin_sqrt (no "f") is the name used by GCC and Clang.
* Refactor regression testing of built-in functionsXavier Leroy2020-07-2713-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.mlXavier Leroy2020-07-275-46/+12
| | | | These functions are now available on all targets.
* AArch64 implementation of __builtin_ctz*Xavier Leroy2020-07-273-1/+11
| | | | Using the "rbit" instruction (reverse bits).
* RISC-V implementation of __builtin_clz* and __builtin_ctz*Xavier Leroy2020-07-272-0/+134
| | | | Using binary search loops expanded at point of use.
* Add support for __builtin_fabsfXavier Leroy2020-07-274-0/+13
|
* No need to process __builtin_fabs in $ARCH/Asmexpand.mlXavier Leroy2020-07-275-12/+0
| | | | __builtin_fabs has already been expanded in backend/Selection.v .
* More checks for __builtin_va_start (#250)Bernhard Schommer2020-07-211-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 lineXavier Leroy2020-07-211-0/+1
|
* Updated handcrafted.messages.Bernhard Schommer2020-07-211-0/+108
| | | | | Added error descriptions for the new syntax errors introduced by '_Static_assert'.
* Support _Static_assert from C11Xavier Leroy2020-07-217-1060/+1116
|
* Support __builtin_constant_p as in GCC and Clang (#367)Xavier Leroy2020-07-211-0/+10
| | | | | Returns 1 if the argument is a constant expression, 0 otherwise. Closes: #366
* Use the correct location for Slabaled in transform.Bernhard Schommer2020-07-211-2/+2
|
* Added error for redefined builtin.Bernhard Schommer2020-07-203-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 Schommer2020-07-151-1/+1
|
* Bytecode-only build, continuedXavier Leroy2020-07-151-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 Leroy2020-07-151-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 Schommer2020-07-091-1/+1
|
* Fix typo.Bernhard Schommer2020-07-081-1/+1
|
* Revert "Use the same version string."Bernhard Schommer2020-07-081-3/+10
| | | | This reverts commit 1a01ad629109cdb60fddae3787e3a589d20e9790.
* Use the same version string.Bernhard Schommer2020-07-081-10/+3
| | | | | | 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.
* Remove no longer needed option enforce-buildnrBernhard Schommer2020-07-081-10/+1
|
* Introduce additional "branch" build information.Bernhard Schommer2020-07-087-13/+20
|
* Add option to print version information in fileBernhard Schommer2020-07-081-1/+17
|
* Bytecode-only build (#243)Xavier Leroy2020-07-072-4/+29
| | | | | | If ocamlopt (the native-code OCaml compiler) is not available, fall back to building with ocamlc (the bytecode OCaml compiler). Fixes: #359
* Revised detection of menhirLib directory (#248)Xavier Leroy2020-07-071-2/+6
| | | | | Use `ocamlfind query menhirLib` in preference to `menhir --suggest-menhirLib`. Fixes: #363
* Added asserts for constraints of PowerPC builtinsBernhard Schommer2020-07-011-0/+6
|
* Fix typo in name of builtin function.Bernhard Schommer2020-07-011-1/+1
|
* Added missing hint database name.Bernhard Schommer2020-06-301-1/+1
|
* Move shared code in new file.Bernhard Schommer2020-06-2817-96/+46
| | | | | The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file.
* Remove the `can_reserve_register` function.Bernhard Schommer2020-06-2810-19/+1
| | | | | The function is in fact just a call to the function`is_callee_save_register` from `Conventions1.v`.
* Use library function.Bernhard Schommer2020-06-281-4/+1
| | | | | | | The function String.uppercase was deprecated and the replacement function String.upercase_ascii was only available from OCaml 4.03.0. Since the minimal OCaml version is now 4.05.0 we can use the function String.upercase_ascii.
* Use Hashtbl.find_opt.Bernhard Schommer2020-06-288-9/+8
| | | | | Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt.
* Eliminate known builtins whose result is ignoredXavier Leroy2020-06-252-40/+54
| | | | | | | | | | | | | | | A typical example is `(void) __builtin_sel(a, b, c)`. It is safe to generate zero code for these uses of builtins because builtins whose semantics are known to the compiler are pure. Other builtins with side effects (e.g. `__builtin_trap`) are not known and will remain in the compiled code. It is useful to generate zero code for these uses of builtins because some of them (e.g. `__builtin_sel`) must be transformed into proper CminorSel expressions during instruction selection. Otherwise, they propagate all the way to ExpandAsm, causing a "not implemented" error there.
* Improve printing of builtin function invocationsXavier Leroy2020-06-251-0/+3
| | | | In particular __builtin_sel.
* Preliminary support for Coq 8.12Xavier Leroy2020-06-212-4/+4
| | | | | | | Based on testing with beta-1 release. The deprecation warning about the "omega" tactic is ignored while we decide when to switch to "lia" instead.
* Transform non-recursive Fixpoint into DefinitionXavier Leroy2020-06-213-3/+3
| | | | | | | As detected by the new warning in Coq 8.12. The use of Fixpoint here is not warranted and either an oversight or a leftover from an earlier version.
* SimplExpr: remove unused definition "sd_cast_set"Xavier Leroy2020-06-151-2/+0
| | | | Follow-up to commit 070babef.
generated by cgit (git 2.34.1) at 2024-07-03 16:11:29 +0000