aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* with timingDavid Monniaux2019-03-132-2/+7
* Fix for CompCert 3.5Cyril SIX2019-03-131-0/+1
* Merge branch 'master' into mppa_postpassCyril SIX2019-03-1329-290/+564
|\
| * Update version number for 3.5v3.5Xavier Leroy2019-02-281-1/+1
| * Update HTML doc for release 3.5Xavier Leroy2019-02-271-1/+1
| * Update Changelog in preparation for release 3.5Xavier Leroy2019-02-261-1/+1
| * Maximum supported Menhir version (#275)Xavier Leroy2019-02-261-1/+1
| * Update Changelog in preparation for release 3.5Xavier Leroy2019-02-251-0/+35
| * Maximum supported Menhir version (#275)Jacques-Henri Jourdan2019-02-251-2/+3
| * Revised attachment of name attributes to structs, unions, enumsXavier Leroy2019-02-253-6/+29
| * Reject object-related and struct-related attributes on typedefsXavier Leroy2019-02-254-8/+19
| * Add regression test for "aligned" attributeXavier Leroy2019-02-253-1/+120
| * Distinguish object-related and name-related attributesXavier Leroy2019-02-254-13/+24
| * Do not expand type names when floating attributes "up" a declarationXavier Leroy2019-02-253-2/+24
| * Ignore and clean file .lia.cacheXavier Leroy2019-02-122-1/+4
| * Make the checker happy (#272)Vincent Laporte2019-02-123-19/+17
| * Add support for Coq 8.9.0Xavier Leroy2019-02-041-3/+3
| * <stddef.h>: define NULL with type void *Xavier Leroy2019-02-041-1/+1
| * Test for NULL in variable argument listsXavier Leroy2019-02-042-1/+53
| * <stdbool.h>: add missing macro __bool_true_false_are_definedXavier Leroy2019-02-041-0/+1
| * Fix some URLs in the first page of the Coq HTML documentation (#263)Andre2019-01-221-5/+5
| * Use `Program Instance` instead of `Instance` + refine mode (#261)Maxime Dénès2018-12-272-64/+86
| * x86: wrong modeling of ZF flag for FP comparisonsXavier Leroy2018-12-202-130/+66
| * Add functions "ordered" and "compare" to Float and Float32Xavier Leroy2018-12-201-9/+20
| * Fix fixme in PackedStructs.Bernhard Schommer2018-11-201-4/+4
| * Fix typo in asmexpand. Bug 24953Bernhard Schommer2018-11-071-1/+1
| * Use 'gpr_or_zero' for base register of indexed load/stores, bug 24776Michael Schmidt2018-10-202-5/+10
| * Catch exception from elab_attr_arg.Bernhard Schommer2018-10-181-1/+4
| * Switch conditions for eref plattforms.Bernhard Schommer2018-09-191-4/+4
| * Support __builtin_isel64 for non-EREF PPC64 platforms (#141)Xavier Leroy2018-09-181-22/+28
| * Add builtin isel (conditional move) for int64, uint64 and _Bool (#140)Bernhard Schommer2018-09-182-1/+16
| * Bug 24518Bernhard Schommer2018-09-170-0/+0
* | Enlevé la dépendance mémoire de PcbuCyril SIX2019-03-133-25/+25
* | for scipDavid Monniaux2019-03-131-0/+11
* | for using CPlexDavid Monniaux2019-03-132-5/+19
* | scripts for using Gurobi and Cplex for ILP solvingDavid Monniaux2019-03-132-2/+2
* | attempt at parser for cplexDavid Monniaux2019-03-131-0/+7
* | -fpostpass-ilpDavid Monniaux2019-03-125-16/+3
* | script for using Gurobi with -fpostpass-ilpDavid Monniaux2019-03-121-0/+3
* | Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-03-125-110/+141
|\ \
| * | Added cascaded_scheduler but the flag does not workCyril SIX2019-03-122-3/+4
| * | Added a flag for changing the scheduler (not any choice available right now)Cyril SIX2019-03-125-3/+12
| * | Proof of exec_trans_pcincr solvedCyril SIX2019-03-121-7/+31
| * | Merge remote-tracking branch 'origin/mppa_parcheck' into mppa_parcheckCyril SIX2019-03-121-12/+12
| |\ \
| | * | fix trans_pcincr for parcheck. (Proof is broken. cf FIXME)Sylvain Boulmé2019-03-121-12/+12
| * | | Simplification des preuves "de discrimination" dans AsmblockdepsCyril SIX2019-03-121-94/+77
| |/ /
| * | [BROKEN] Added parallelizability check - breaks all the conditional jumpsCyril SIX2019-03-122-1/+19
* | | -fpostpass-ilpDavid Monniaux2019-03-123-2/+7
* | | better tracing for ILP + make cleanDavid Monniaux2019-03-123-3/+12
* | | Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-03-121-5/+10
|\| |