aboutsummaryrefslogtreecommitdiffstats
path: root/backend/PrintLTL.ml
Commit message (Collapse)AuthorAgeFilesLines
* Move shared code in new file.Bernhard Schommer2020-06-281-1/+1
| | | | | The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file.
* Compatibility with OCaml 4.08 (#302)Xavier Leroy2019-07-081-1/+1
| | | | | | | | | | | | | | | | * Do not use `Pervasives.xxx` qualified names Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`, and uses of `Pervasives` cause fatal warnings. This commit uses unqualified names instead, as no ambiguity occurs. * Clarify "open" statements OCaml 4.08.0 has stricter warnings concerning open statements that shadow module names. Closes: #300
* Remove open Locations.Bernhard Schommer2017-02-061-6/+5
| | | | The Locations are only used in one function.
* Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-151-2/+2
| | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* Code cleanup.Bernhard Schommer2016-03-101-4/+3
| | | | | | Removed some unused variables, functions etc. and resolved some problems which occur if all warnings except 3,4,9 and 29 are active. Bug 18394.
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-4/+3
| | | | | | | | | | | | | | | | | | | | | | | | Before, the back-end languages had distinct instructions - Iannot for annotations, taking structured expressions (annot_arg) as arguments, and producing no results' - Ibuiltin for other builtins, using simple pseudoregs/locations/registers as arguments and results. This branch enriches Ibuiltin instructions so that they take structured expressions (builtin_arg and builtin_res) as arguments and results. This way, - Annotations fit the general pattern of builtin functions, so Iannot instructions are removed. - EF_vload_global and EF_vstore_global become useless, as the same optimization can be achieved by EF_vload/vstore taking a structured argument of the "address of global" kind. - Better code can be generated for builtin_memcpy between stack locations, or volatile accesses to stack locations. Finally, this commit also introduces a new kind of external function, EF_debug, which is like EF_annot but produces no observable events. It will be used later to transport debug info through the back-end, without preventing optimizations.
* Updated the Caml part. Added some more tests in annot1.c.Xavier Leroy2015-03-271-2/+2
|
* Do not use Format for faster printing of RTL, XTL, LTL, Machxleroy2013-09-261-30/+28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2337 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Hunting stack overflows again:xleroy2013-05-271-1/+1
| | | | | | | | PrintLTL: List.map -> List.rev_map IRC: @ -> List.rev_append + don't maintain "extra" lists on precolored nodes. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2262 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-67/+92
| | | | | | | | | 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-181-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of annotation statements, and more generally built-in ↵xleroy2011-06-131-2/+5
| | | | | | functions, and more generally external functions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Pretty-printers for RTL and LTL. Not yet well integrated.xleroy2010-05-021-0/+117
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1332 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-28 19:02:42 +0000