summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* 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
* Nettoyages docGravatar xleroy2008-03-19
* Probleme echo -ne sur MacOS 10.5Gravatar xleroy2008-03-04
* DatesGravatar xleroy2008-01-28
* Ajout license, README, copyright noticesGravatar xleroy2008-01-27
* Function -> Definition (probleme de performance avec Coq8.1pl3)Gravatar xleroy2008-01-07
* Ajout corollaires et overlap pour le papier JAR (pas encore utilises dans Com...Gravatar xleroy2007-12-08
* Ajout find_symbol_not_nullptr; nettoyagesGravatar xleroy2007-12-06
* In Clight, revised handling of comparisons between pointers and 0Gravatar xleroy2007-11-13
* Ajout de global_addresses_distinctGravatar xleroy2007-11-03
* Problemes d'alignement des variables globales et a l'interieur de leurs initi...Gravatar xleroy2007-10-31
* Simplification des Cconst_symbol: seules les versions 'signed' sont conserveesGravatar xleroy2007-10-31
* Simplification des Cconst_symbol: seules les versions 'signed' sont conserveesGravatar xleroy2007-10-31
* Revu l'heuristique de linearisationGravatar xleroy2007-10-30
* Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFGGravatar xleroy2007-10-27
* Typo dans le pseudocode en commentaireGravatar xleroy2007-10-17
* MAJGravatar xleroy2007-10-17
* MAJGravatar xleroy2007-10-17
* Relaxation de la regle d'evaluation EcastGravatar xleroy2007-10-17
* Utilisation d'une monade avec types dependants pour garder trace des propriet...Gravatar xleroy2007-10-17
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...Gravatar xleroy2007-08-28
* Ajout de common/Complements.vGravatar xleroy2007-08-26
* Rendu le test lists.c plus interessantGravatar xleroy2007-08-06
* Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu MakefilesGravatar xleroy2007-08-06
* DocumentationGravatar xleroy2007-08-05
* Deplacement du repertoire "papers" dans la hierarchie SVNGravatar xleroy2007-08-04