aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Updatev1.3xleroy2008-08-091-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@711 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Changes 1.2 -> 1.3xleroy2008-08-091-0/+42
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@709 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout nouveaux testsxleroy2008-08-0952-0/+8446
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@708 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Plus besoin de rectifier les URL invalidesxleroy2008-08-011-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@707 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Flag to turn on/off the recognition of fused multiply-add and multiply-subxleroy2008-07-317-61/+69
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@706 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added Slabel, Sgotoxleroy2008-07-311-0/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@705 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update test resultsxleroy2008-07-311-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@704 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJ documentationxleroy2008-07-277-362/+111
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@702 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplification de la semantique de LTL et LTLin. Les details lies aux ↵xleroy2008-07-258-523/+538
| | | | | | conventions d'appel sont maintenant geres de maniere plus locale dans la passe Reload. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@701 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Augmenter le temps d'execution par defautxleroy2008-07-252-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@700 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion partielle de la branche contsem: xleroy2008-07-0811-1789/+1778
| | | | | | | | | | - semantiques a continuation pour Cminor et CminorSel - goto dans Cminor Suppression de backend/RTLbigstep.v, devenu inutile. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@692 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Nettoyage du traitement des signatures au return dans LTL et LTLinxleroy2008-07-076-107/+96
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@690 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Utilisation de intoffloatu. Ajout du cas int + ptr.xleroy2008-05-314-15/+42
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@652 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs ↵xleroy2008-05-307-80/+138
| | | | | | vers des blocs differents! git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@649 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ↵xleroy2008-05-3019-10/+449
| | | | | | utilisee dans le front-end C. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suppression de 'exten', inutilisexleroy2008-05-301-6/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@646 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Compilo C, preprocesseur, assembleur sont determines par configure et mis ↵xleroy2008-04-196-12/+25
| | | | | | dans Makefile.config git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Erreur dans la traduction d'un for lorsque la condition est complexexleroy2008-04-191-22/+24
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@621 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Impression des 'for'xleroy2008-04-191-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@620 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Detecter __builtin_xxxxleroy2008-04-191-2/+11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@619 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Amelioration compilation des switchxleroy2008-04-173-42/+96
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@616 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Camlcoq.ml: interpret Caml's int32 as unsigned when converting to Integers.intxleroy2008-04-162-5/+8
| | | | | | | Cil2Csyntax.ml: terminating NUL character in strings within initialized data git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout du test vmachxleroy2008-04-153-1/+219
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@612 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJxleroy2008-04-152-147/+133
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@611 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Alignement de la pile dans PrintPPCxleroy2008-04-132-12/+16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@606 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu le traitement de la 'red zone' en bas de la pilexleroy2008-04-128-58/+65
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@605 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu gestion retaddr et link dans Stackingxleroy2008-04-1217-934/+1032
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@604 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Meilleure selection pour if ((a && b) != 0), etcxleroy2008-03-272-27/+277
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@581 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu removeproofxleroy2008-03-194-26/+50
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@567 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Nettoyages docxleroy2008-03-192-15/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@566 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Probleme echo -ne sur MacOS 10.5v1.2xleroy2008-03-041-0/+14
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@548 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Datesxleroy2008-01-281-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@491 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout license, README, copyright noticesxleroy2008-01-27110-4/+2027
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Function -> Definition (probleme de performance avec Coq8.1pl3)xleroy2008-01-071-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@470 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout corollaires et overlap pour le papier JAR (pas encore utilises dans ↵xleroy2007-12-081-6/+363
| | | | | | Compcert) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@460 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout find_symbol_not_nullptr; nettoyagesxleroy2007-12-061-39/+71
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@455 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In Clight, revised handling of comparisons between pointers and 0xleroy2007-11-134-39/+39
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@447 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout de global_addresses_distinctxleroy2007-11-031-16/+75
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@445 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Problemes d'alignement des variables globales et a l'interieur de leurs ↵xleroy2007-10-317-166/+234
| | | | | | initialiseurs git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@444 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplification des Cconst_symbol: seules les versions 'signed' sont conserveesxleroy2007-10-311-4/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@443 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplification des Cconst_symbol: seules les versions 'signed' sont conserveesxleroy2007-10-313-79/+59
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@442 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu l'heuristique de linearisationxleroy2007-10-301-46/+36
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@438 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFGxleroy2007-10-279-197/+363
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@437 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo dans le pseudocode en commentairexleroy2007-10-171-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@423 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJxleroy2007-10-171-107/+107
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@422 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJxleroy2007-10-172-5/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@421 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Relaxation de la regle d'evaluation Ecastxleroy2007-10-172-4/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@420 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Utilisation d'une monade avec types dependants pour garder trace des ↵xleroy2007-10-173-556/+461
| | | | | | proprietes state_incr git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@419 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les ↵xleroy2007-08-2833-3523/+4572
| | | | | | expressions sont maintenant pures et les appels de fonctions sont des statements. Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor. Preuve de preservation semantique pour les programmes qui divergent. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout de common/Complements.vxleroy2007-08-266-2/+674
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@405 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-13 02:58:07 +0000