aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* Cleanupxleroy2008-12-311-105/+0
* Continuation of PowerPC/EABI portxleroy2008-12-314-149/+375
* Turn off generation of libcil.a, which is not correct with OCaml 3.11xleroy2008-12-311-2/+11
* Removed vfprintf, because it was causing portability problemsxleroy2008-12-312-6/+0
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-3066-1221/+12137
* Extract Coq lists to Caml lists.xleroy2008-12-2913-146/+112
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.xleroy2008-12-2915-367/+844
* Revised back-end so that only 2 integer registers are reserved for reloading.xleroy2008-12-2122-421/+795
* Clight: ajout Econdition, suppression Eindex.xleroy2008-09-278-47/+160
* Update for release 1.3xleroy2008-08-111-1/+2
* New filexleroy2008-08-111-0/+25
* Updatev1.3xleroy2008-08-091-2/+2
* Changes 1.2 -> 1.3xleroy2008-08-091-0/+42
* Ajout nouveaux testsxleroy2008-08-0952-0/+8446
* Plus besoin de rectifier les URL invalidesxleroy2008-08-011-0/+2
* Flag to turn on/off the recognition of fused multiply-add and multiply-subxleroy2008-07-317-61/+69
* Added Slabel, Sgotoxleroy2008-07-311-0/+4
* Update test resultsxleroy2008-07-311-1/+1
* MAJ documentationxleroy2008-07-277-362/+111
* Simplification de la semantique de LTL et LTLin. Les details lies aux conven...xleroy2008-07-258-523/+538
* Augmenter le temps d'execution par defautxleroy2008-07-252-2/+2
* Fusion partielle de la branche contsem: xleroy2008-07-0811-1789/+1778
* Nettoyage du traitement des signatures au return dans LTL et LTLinxleroy2008-07-076-107/+96
* Utilisation de intoffloatu. Ajout du cas int + ptr.xleroy2008-05-314-15/+42
* Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs v...xleroy2008-05-307-80/+138
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...xleroy2008-05-3019-10/+449
* Suppression de 'exten', inutilisexleroy2008-05-301-6/+0
* Compilo C, preprocesseur, assembleur sont determines par configure et mis dan...xleroy2008-04-196-12/+25
* Erreur dans la traduction d'un for lorsque la condition est complexexleroy2008-04-191-22/+24
* Impression des 'for'xleroy2008-04-191-1/+1
* Detecter __builtin_xxxxleroy2008-04-191-2/+11
* Amelioration compilation des switchxleroy2008-04-173-42/+96
* Camlcoq.ml: interpret Caml's int32 as unsigned when converting to Integers.intxleroy2008-04-162-5/+8
* Ajout du test vmachxleroy2008-04-153-1/+219
* MAJxleroy2008-04-152-147/+133
* Alignement de la pile dans PrintPPCxleroy2008-04-132-12/+16
* Revu le traitement de la 'red zone' en bas de la pilexleroy2008-04-128-58/+65
* Revu gestion retaddr et link dans Stackingxleroy2008-04-1217-934/+1032
* Meilleure selection pour if ((a && b) != 0), etcxleroy2008-03-272-27/+277
* Revu removeproofxleroy2008-03-194-26/+50
* Nettoyages docxleroy2008-03-192-15/+6
* Probleme echo -ne sur MacOS 10.5v1.2xleroy2008-03-041-0/+14
* Datesxleroy2008-01-281-1/+1
* Ajout license, README, copyright noticesxleroy2008-01-27110-4/+2027
* Function -> Definition (probleme de performance avec Coq8.1pl3)xleroy2008-01-071-1/+1
* Ajout corollaires et overlap pour le papier JAR (pas encore utilises dans Com...xleroy2007-12-081-6/+363
* Ajout find_symbol_not_nullptr; nettoyagesxleroy2007-12-061-39/+71
* In Clight, revised handling of comparisons between pointers and 0xleroy2007-11-134-39/+39
* Ajout de global_addresses_distinctxleroy2007-11-031-16/+75
* Problemes d'alignement des variables globales et a l'interieur de leurs initi...xleroy2007-10-317-166/+234