aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* x86 branchless implementation of float -> unsigned int32 conversionfloatofintuXavier Leroy2019-06-072-30/+31
* x86: operators Ointoffloat and Ointofsingle are totalXavier Leroy2019-06-075-16/+47
* x86 branchless implementation of unsigned int32 -> float conversionXavier Leroy2019-06-074-8/+70
* If-conversion optimizationXavier Leroy2019-06-0610-75/+751
* Type inference and type checking for CminorXavier Leroy2019-06-062-1/+798
* Additional simulation diagrams for determinate source languagesXavier Leroy2019-06-061-0/+173
* ARM: select is not supported at type TlongXavier Leroy2019-06-062-2/+11
* New additional check for void parameters. (#174)Bernhard Schommer2019-06-031-3/+5
* Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-3121-31/+31
* Provide a float select operation for PowerPC. (#173)Bernhard Schommer2019-05-289-7/+101
* PowerPC: add SelectOp.select functionXavier Leroy2019-05-262-0/+31
* ARM: Fix expansion of FP conditional moveXavier Leroy2019-05-261-2/+2
* Coq 8.9.1 supportXavier Leroy2019-05-211-3/+3
* Csyntax.v: Fix a typo in a documentation comment (#292)Bart Jacobs2019-05-211-1/+1
* Add a check for the args of unprototyped calls.Bernhard Schommer2019-05-201-3/+8
* Provide a default "select" operation for the RiscV portXavier Leroy2019-05-202-0/+20
* Implement a `Osel` operation for ARMXavier Leroy2019-05-2012-7/+115
* Implement a `Osel` operation for x86Xavier Leroy2019-05-2011-38/+298
* Emulate the "isel" instruction on non-EREF PPC processorsXavier Leroy2019-05-203-22/+42
* Implement a `Osel` operation for PowerPCXavier Leroy2019-05-207-9/+106
* Give a semantics to the Pisel instructionXavier Leroy2019-05-201-1/+7
* Support a "select" operation between two valuesXavier Leroy2019-05-203-0/+212
* PowerPC: make sure evaluation of conditions do not destroy any registerXavier Leroy2019-05-204-54/+155
* Prepend $(DESTDIR) to the installation target (#169)Bernhard Schommer2019-05-172-16/+16
* Reworked elaboration of declarations/definitions.Bernhard Schommer2019-05-101-140/+138
* Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-108-15/+41
* Change to AbsInt version string.Bernhard Schommer2019-05-105-6/+6
* Check for reserved keywords.Bernhard Schommer2019-05-101-1/+8
* Fix various scoping issues (#163)Bernhard Schommer2019-05-101-51/+56
* Ensure flushing of the error formatter.Bernhard Schommer2019-05-101-0/+4
* Expand the responsefiles earlierBernhard Schommer2019-05-105-17/+17
* Check for alignment of command-line switches.Bernhard Schommer2019-05-102-6/+10
* More efficient test for powers of twoXavier Leroy2019-05-092-26/+105
* Make scripts compatible with new behavior of field_simplify (#291)Vincent Laporte2019-05-062-3/+3
* Rename Fappli_IEEE_extra.v into IEEE754_extra.vXavier Leroy2019-04-263-2/+2
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-2613-884/+1031
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-2315-135/+52
* Replace nat_of_Z with Z.to_natXavier Leroy2019-04-2311-68/+45
* Problems with Dwarf ranges (#159)Xavier Leroy2019-04-239-56/+96
|\
| * Simplified offset printing.Bernhard Schommer2019-04-161-2/+3
| * Print only debug info for printed functions.Bernhard Schommer2019-04-166-14/+18
| * Reworked range entries.Bernhard Schommer2019-04-163-39/+71
| * Reset scope ids later.Bernhard Schommer2019-04-161-1/+1
| * Avoid generation of empty ranges.Bernhard Schommer2019-04-161-1/+4
| * Relax requirement for ranges for compilation unit.Bernhard Schommer2019-04-161-1/+1
|/
* 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
* Floats.v: remove leftover Print commandsXavier Leroy2019-04-041-5/+1
* Floats.v: avoid using module Zlogarithm in the proofsXavier Leroy2019-04-031-10/+19
* Correct typo in Clightnorm.ml (#285)Alix Trieu2019-03-271-1/+1
generated by cgit (git 2.34.1) at 2024-05-02 20:06:46 +0000