aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
Commit message (Expand)AuthorAgeFilesLines
* Flag to turn on/off the recognition of fused multiply-add and multiply-subxleroy2008-07-313-27/+33
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...xleroy2008-05-302-5/+9
* Compilo C, preprocesseur, assembleur sont determines par configure et mis dan...xleroy2008-04-191-1/+5
* MAJxleroy2008-04-151-123/+121
* Ajout license, README, copyright noticesxleroy2008-01-272-0/+24
* Problemes d'alignement des variables globales et a l'interieur de leurs initi...xleroy2007-10-311-112/+116
* Simplification des Cconst_symbol: seules les versions 'signed' sont conserveesxleroy2007-10-311-4/+2
* Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFGxleroy2007-10-274-35/+19
* MAJxleroy2007-10-171-107/+107
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-282-127/+121
* Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefilesxleroy2007-08-062-114/+138
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-044-165/+233
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...xleroy2007-03-023-137/+145
* 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-112-11/+29
* Encore une eta-expansion intempestivexleroy2006-09-111-4/+23
* MAJxleroy2006-09-081-2/+2
* Integration du front-end CIL developpe par Thomas Moniotxleroy2006-09-072-29/+45
* Ajout de dependances dans extraction/Makefiletristan2006-09-062-23/+31
* Revu la repartition des sources Coq en sous-repertoiresxleroy2006-09-041-1/+1
* Fusion de la branche "traces":xleroy2006-09-043-101/+124
* Ajout d'un type-checker (non certifie) pour Cminorxleroy2006-07-172-15/+20
* Renommage List -> CList lors de l'extractionxleroy2006-03-092-219/+221
* Nettoyagesxleroy2006-02-091-1/+4
* Initial import of compcertxleroy2006-02-096-0/+589
generated by cgit (git 2.34.1) at 2024-06-03 03:02:52 +0000