aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * 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
| * Ignore more of Coq's cache filesXavier Leroy2019-03-271-1/+4
| * Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-2746-7841/+9954
| * Define macros with CompCert's version number (#284)Xavier Leroy2019-03-271-2/+24
| * Harden configure against weird Menhir installationsXavier Leroy2019-03-251-2/+8
| * RTLgenproof: destruct too deepXavier Leroy2019-03-251-2/+2
| * Integers.v: add modulus_gt_one (#259)Xavier Leroy2019-03-251-1/+7
| * Update the comment of the free operation (#277)chaomaer2019-03-251-1/+1
| * Minor simplifications in two proofs. (#280)Vincent Laporte2019-03-252-3/+3
| * Improve overflow check for integer literals (#157)Michael Schmidt2019-03-201-2/+4
* | use all same exact include filesv3.5_k1c_1.2David Monniaux2019-06-032-26/+15
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cosDavid Monniaux2019-05-3021-53/+891
|\ \
| * \ Merge remote-tracking branch 'origin/mppa-msub' into mppa-workDavid Monniaux2019-05-3022-54/+892
| |\ \
| | * | standardization of expressionsDavid Monniaux2019-05-122-10/+8
generated by cgit (git 2.34.1) at 2024-07-12 01:29:07 +0000