aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * 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
| | * | standardize semantics, 1David Monniaux2019-05-122-7/+12
| | * | Merge remote-tracking branch 'origin/mppa-work' into mppa-msubDavid Monniaux2019-05-124-67/+88
| | |\ \
| | * | | correct -faddx option and propagate addim over addximDavid Monniaux2019-05-114-10/+21
| | * | | option -faddx (off by default until questions cleared)David Monniaux2019-05-118-29/+97
| | * | | apply .xs onto addx4 etcDavid Monniaux2019-05-1110-27/+180
| | * | | more maddxDavid Monniaux2019-05-112-0/+74
| | * | | maddx ordre opposéDavid Monniaux2019-05-112-0/+6
| | * | | add with shift, beginningDavid Monniaux2019-05-117-13/+86
| | * | | generate multiply-sub longDavid Monniaux2019-05-113-4/+56
| | * | | Pmsub compiledDavid Monniaux2019-05-119-40/+48
| | * | | more gen O -> PDavid Monniaux2019-05-111-0/+9
| | * | | more gen O -> PDavid Monniaux2019-05-111-0/+6
| | * | | Oaddx -> PDavid Monniaux2019-05-115-21/+48
| | * | | begin generating Prevsub etc. from Oxxx to PxxxDavid Monniaux2019-05-118-44/+47
| | * | | use shift 1-4 in backendDavid Monniaux2019-05-105-97/+62
| | * | | more integer OpDavid Monniaux2019-05-104-17/+245
| | * | | new instructions at asm levelDavid Monniaux2019-05-105-9/+157
* | | | | Merge branch 'mppa-cos' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2019-05-301-2/+3
|\ \ \ \ \
| * | | | | make -j20 instead of xargs -P4 + make -j5Cyril SIX2019-05-291-2/+3
* | | | | | take other measurementsDavid Monniaux2019-05-292-2/+2
|/ / / / /
generated by cgit (git 2.34.1) at 2024-07-12 01:27:48 +0000