summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Elimination of "alloc" instruction in Caml files and test files.Gravatar xleroy2009-01-11
* - Added alignment constraints to memory loads and stores.Gravatar xleroy2009-01-11
* Fixed unary minusGravatar xleroy2009-01-07
* Test for int/float conversionsGravatar xleroy2009-01-07
* UpdatesGravatar xleroy2009-01-05
* Endianness in testsGravatar xleroy2009-01-05
* Cminor, CminorSel: removed useless premises in rules for SreturnGravatar xleroy2009-01-04
* Some cleanupsGravatar xleroy2009-01-02
* Wrong dependenciesGravatar xleroy2009-01-02
* Continuation of ARM port.Gravatar xleroy2009-01-01
* CleanupGravatar xleroy2008-12-31
* Continuation of PowerPC/EABI portGravatar xleroy2008-12-31
* Turn off generation of libcil.a, which is not correct with OCaml 3.11Gravatar xleroy2008-12-31
* Removed vfprintf, because it was causing portability problemsGravatar xleroy2008-12-31
* Reorganized the development, modularizing away machine-dependent parts.Gravatar xleroy2008-12-30
* Extract Coq lists to Caml lists.Gravatar xleroy2008-12-29
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.Gravatar xleroy2008-12-29
* Revised back-end so that only 2 integer registers are reserved for reloading.Gravatar xleroy2008-12-21
* Clight: ajout Econdition, suppression Eindex.Gravatar xleroy2008-09-27
* Update for release 1.3Gravatar xleroy2008-08-11
* New fileGravatar xleroy2008-08-11
* UpdateGravatar xleroy2008-08-09
* Changes 1.2 -> 1.3Gravatar xleroy2008-08-09
* Ajout nouveaux testsGravatar xleroy2008-08-09
* Plus besoin de rectifier les URL invalidesGravatar xleroy2008-08-01
* Flag to turn on/off the recognition of fused multiply-add and multiply-subGravatar xleroy2008-07-31
* Added Slabel, SgotoGravatar xleroy2008-07-31
* Update test resultsGravatar xleroy2008-07-31
* MAJ documentationGravatar xleroy2008-07-27
* Simplification de la semantique de LTL et LTLin. Les details lies aux conven...Gravatar xleroy2008-07-25
* Augmenter le temps d'execution par defautGravatar xleroy2008-07-25
* Fusion partielle de la branche contsem: Gravatar xleroy2008-07-08
* Nettoyage du traitement des signatures au return dans LTL et LTLinGravatar xleroy2008-07-07
* Utilisation de intoffloatu. Ajout du cas int + ptr.Gravatar xleroy2008-05-31
* Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs v...Gravatar xleroy2008-05-30
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...Gravatar xleroy2008-05-30
* Suppression de 'exten', inutiliseGravatar xleroy2008-05-30
* Compilo C, preprocesseur, assembleur sont determines par configure et mis dan...Gravatar xleroy2008-04-19
* Erreur dans la traduction d'un for lorsque la condition est complexeGravatar xleroy2008-04-19
* Impression des 'for'Gravatar xleroy2008-04-19
* Detecter __builtin_xxxGravatar xleroy2008-04-19
* Amelioration compilation des switchGravatar xleroy2008-04-17
* Camlcoq.ml: interpret Caml's int32 as unsigned when converting to Integers.intGravatar xleroy2008-04-16
* Ajout du test vmachGravatar xleroy2008-04-15
* MAJGravatar xleroy2008-04-15
* Alignement de la pile dans PrintPPCGravatar xleroy2008-04-13
* Revu le traitement de la 'red zone' en bas de la pileGravatar xleroy2008-04-12
* Revu gestion retaddr et link dans StackingGravatar xleroy2008-04-12
* Meilleure selection pour if ((a && b) != 0), etcGravatar xleroy2008-03-27
* Revu removeproofGravatar xleroy2008-03-19