aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * | why doesn't it work?David Monniaux2019-06-042-7/+265
| * | little restructuringDavid Monniaux2019-06-041-3/+4
| * | keep the .s filesDavid Monniaux2019-06-041-0/+2
| * | remove old "ternary" stuffDavid Monniaux2019-06-045-47/+10
| * | start to have whole path if-conversion?David Monniaux2019-06-043-3/+18
| * | Osel -> assembleurDavid Monniaux2019-06-043-104/+112
| * | Osel is output = 1st inputDavid Monniaux2019-06-041-0/+1
| * | Osel operation (not yet compiled)David Monniaux2019-06-043-31/+39
| * | rm old select/selectl/selectf/selectfsDavid Monniaux2019-06-0314-914/+47
| * | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...David Monniaux2019-06-03158-9521/+14486
| |\ \
| | * | ARM: select is not supported at type TlongXavier Leroy2019-06-013-4/+14
| | * | If-conversion optimizationXavier Leroy2019-05-3110-75/+746
| | * | Type inference and type checking for CminorXavier Leroy2019-05-312-1/+799
| | * | Additional simulation diagrams for determinate source languagesXavier Leroy2019-05-311-0/+173
| | |/
| | * 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