aboutsummaryrefslogtreecommitdiffstats
path: root/extraction/.depend
Commit message (Expand)AuthorAgeFilesLines
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-529/+0
* Extract Coq lists to Caml lists.xleroy2008-12-291-2/+2
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.xleroy2008-12-291-3/+9
* Revised back-end so that only 2 integer registers are reserved for reloading.xleroy2008-12-211-4/+0
* Flag to turn on/off the recognition of fused multiply-add and multiply-subxleroy2008-07-311-27/+29
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...xleroy2008-05-301-5/+8
* MAJxleroy2008-04-151-123/+121
* Problemes d'alignement des variables globales et a l'interieur de leurs initi...xleroy2007-10-311-112/+116
* Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFGxleroy2007-10-271-12/+15
* MAJxleroy2007-10-171-107/+107
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-281-125/+119
* Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefilesxleroy2007-08-061-109/+121
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-155/+215
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...xleroy2007-03-021-130/+127
* Lever la restriction sur les fonctions externes, restriction qui exigeait que...xleroy2006-10-221-10/+15
* MAJ suite ajouts dans Kildall. Compiler en code natif par defautxleroy2006-09-111-6/+22
* MAJxleroy2006-09-081-2/+2
* Integration du front-end CIL developpe par Thomas Moniotxleroy2006-09-071-22/+36
* Ajout de dependances dans extraction/Makefiletristan2006-09-061-23/+29
* Fusion de la branche "traces":xleroy2006-09-041-91/+103
* Ajout d'un type-checker (non certifie) pour Cminorxleroy2006-07-171-14/+19
* Renommage List -> CList lors de l'extractionxleroy2006-03-091-213/+214
* Initial import of compcertxleroy2006-02-091-0/+395