aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Reworked json export.Bernhard Schommer2019-09-123-29/+37
* Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-2/+2
* AArch64 portXavier Leroy2019-08-087-37/+97
* Asmgenproof0: add predicate exec_straight0Xavier Leroy2019-08-071-0/+26
* Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-071-2/+0
* Improve CSE for known built-in functionsXavier Leroy2019-07-172-7/+14
* Perform constant propagation for known built-in functionsXavier Leroy2019-07-174-16/+168
* Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-112/+231
* Compatibility with OCaml 4.08 (#302)Xavier Leroy2019-07-086-7/+6
* Rename option `-ffavor-branchless` into `-Obranchless`Xavier Leroy2019-07-051-3/+3
* Extended asm: print register names according to their typesXavier Leroy2019-06-171-9/+14
* Cminortyping: relax typechecking of function callsXavier Leroy2019-06-061-12/+15
* If-conversion optimizationXavier Leroy2019-06-064-72/+584
* Type inference and type checking for CminorXavier Leroy2019-06-061-0/+797
* Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-314-5/+5
* Support a "select" operation between two valuesXavier Leroy2019-05-202-0/+86
* Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-101-0/+8
* Change to AbsInt version string.Bernhard Schommer2019-05-102-2/+2
* Expand the responsefiles earlierBernhard Schommer2019-05-102-4/+4
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-263-20/+21
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-235-20/+22
* Replace nat_of_Z with Z.to_natXavier Leroy2019-04-235-17/+17
* Print only debug info for printed functions.Bernhard Schommer2019-04-161-1/+2
* Typo in comment about Ijumptable in RTL.vAlix Trieu2019-04-151-1/+1
* Fix typo in section name in Selectionproof.v Alix Trieu2019-04-151-2/+2
* RTLgenproof: destruct too deepXavier Leroy2019-03-251-2/+2
* Minor simplifications in two proofs. (#280)Vincent Laporte2019-03-251-2/+2
* Make the checker happy (#272)Vincent Laporte2019-02-121-6/+8
* Simplified code. Bug 24067Bernhard Schommer2018-09-121-8/+8
* Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-122-3/+35
* Various improvements in the wording of diagnostics.Michael Schmidt2018-08-021-4/+4
* Treat Outgoing stack slots as caller-save in LTL/Linear semantics (#237)Xavier Leroy2018-06-176-93/+145
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-018-8/+79
* Add newline directly on list in annot.Bernhard Schommer2018-03-132-4/+7
* Print size argument of Init_space as Z not as int32Xavier Leroy2018-03-131-1/+1
* Introduce more brackets for register annotation.Bernhard Schommer2018-03-121-4/+5
* Do not use "Require" inside sections (#224)Xavier Leroy2018-03-121-3/+1
* Added seperator in warning msg. Bug 23179Bernhard Schommer2018-03-091-1/+1
* Do not use default printer for variable names.Bernhard Schommer2018-03-091-2/+8
* Perform quoting for json.Bernhard Schommer2018-03-081-1/+8
* Print symbols as symbols.Bernhard Schommer2018-03-082-4/+26
* Improve error messages.Bernhard Schommer2018-03-071-16/+14
* Reword error message. Fix 22464Bernhard Schommer2018-03-071-2/+2
* Improve wording.Bernhard Schommer2018-03-071-1/+1
* Improve and simplify error messages.Bernhard Schommer2018-03-072-31/+54
* Reactivated and improved ais annotations.Bernhard Schommer2018-03-064-22/+204
* Change AsmToJson to be similar to other printers.Bernhard Schommer2018-01-052-1/+33
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-053-0/+249
* ValueAnalysis: remove duplicate list_forall2_in_left (#212)Jérémie Koenig2018-01-031-13/+2
* Introduce and use C2C.atom_inline function with 3-valued resultXavier Leroy2017-12-081-3/+6
generated by cgit (git 2.34.1) at 2024-06-02 18:14:08 +0000