aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation ↵xleroy2007-03-0221-1010/+594
| | | | | | de Lattice pour utiliser une notion d'egalite possiblement differente de =. Adaptation de Kildall et de ses utilisateurs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Nettoyagexleroy2007-03-021-1/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@181 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Mettre les 2 demi-espaces dans 2 blocs separesxleroy2007-03-021-9/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@180 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Preuve des 2 axiomes restantsxleroy2007-03-021-2/+17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@179 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout lemmes utiles sur egalite decidablexleroy2007-03-021-0/+31
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@178 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout operation eq dans PMap et IndexedMapxleroy2007-01-031-0/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@158 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Petites adaptations pour Coq 8.1gammaxleroy2006-11-118-20/+27
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@135 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout test mark&sweep GCxleroy2006-10-275-2/+439
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@134 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout test stop&copy GCxleroy2006-10-263-1/+404
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@133 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Rapport d'erreur dans CILxleroy2006-10-231-1/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@130 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Propagation des erreursxleroy2006-10-231-20/+94
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Relaxation des contraintes sur les struct recursivesxleroy2006-10-232-14/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@128 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Location pour erreur sur le type de main()xleroy2006-10-231-1/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@127 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Verification du type de retour de main()xleroy2006-10-231-10/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Lever la restriction sur les fonctions externes, restriction qui exigeait ↵xleroy2006-10-2219-167/+267
| | | | | | que tous les arguments resident en registres git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Meilleur traitement des fonctions forward declared. Ajout d'un warning sur ↵xleroy2006-10-221-0/+16
| | | | | | le nombre d'arguments d'une fonction externe, qui est actuellement limite par le back-end git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@124 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout et utilisation de compcert_stdio.hxleroy2006-10-226-6/+210
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@123 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Resolution d'un probleme (cf. big endian), etblazy2006-10-2011-20/+12
| | | | | | | | mise a jour des Makefile. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@122 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout du banc de tests de CCured (Olden benchmark suite, cf.blazy2006-10-20202-0/+12593
| | | | | | | | | | CCured: type-safe retrofitting of legacy code, G.Necula et al.) rapportCompcert_all.txt liste les erreurs produites par ccomp. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@121 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cleaning...lrg2006-10-201-2/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* interpreter for "little"lrg2006-10-2016-0/+1336
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@119 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Meilleure compilation de la negation booleennexleroy2006-09-195-7/+15
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@112 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplification de Cminor: les affectations de variables locales ne sontxleroy2006-09-1811-981/+792
| | | | | | | | plus des expressions mais des statements (Eassign -> Sassign). Cela simplifie les preuves et ameliore la qualite du RTL produit. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@111 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suite des stubs variadiques.xleroy2006-09-171-16/+13
| | | | | | | Correction bug dans Piuctf. Utiliser la 'red zone' en dessous de SP pour les conversions int<->float git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@110 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Preprocesser en definissant __ppc__ (utile pour l'emulation MacOSX/Intel)xleroy2006-09-171-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@109 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Nettoyagesxleroy2006-09-174-18/+16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@108 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu generation de stubs pour les fonctions variadiquesxleroy2006-09-171-28/+106
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@107 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* typo in commentxleroy2006-09-171-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@106 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Type unrolling in struct and union fieldsxleroy2006-09-171-5/+30
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@105 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Davantage de testsxleroy2006-09-1733-33/+3010
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@104 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bug dans le traitement des fonctions variadiques.xleroy2006-09-171-25/+54
| | | | | | | | | Tolerer les chaines litterales dans les initialiseurs. Forcer evaluation gauche-droite pour avoir les erreurs et warnings dans l'ordre du source. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@103 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Meilleur message de debug dans le cas Icallxleroy2006-09-171-6/+15
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@102 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout de Init_pointer (experimental)xleroy2006-09-174-4/+61
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Const.prop dans la taille des tableaux. Tolerer (avec warning) les ↵xleroy2006-09-161-5/+9
| | | | | | declarations extern ty var[]. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@100 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout du test listsxleroy2006-09-112-2/+57
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@99 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Utiliser l'extension .light.c au lieu de .clightxleroy2006-09-111-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@98 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo dans impression structsxleroy2006-09-111-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@97 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Eviter de caster les fonctions directement dans le cas variadique, gcc dit ↵xleroy2006-09-111-4/+1
| | | | | | que c'est interdit git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@96 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suppression des casts systematiques vers unsigned int dans les comparaisons ↵xleroy2006-09-111-9/+65
| | | | | | de pointeurs git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@95 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu traitement des structures et unions recursives. Dans Cshmgen, ↵xleroy2006-09-117-77/+82
| | | | | | meilleure compilation de exit_if_false. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@94 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Code de timingxleroy2006-09-111-0/+26
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@93 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJ suite ajouts dans Kildall. Compiler en code natif par defautxleroy2006-09-112-11/+29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@92 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Meilleure representation des worklists dans l'algo de Kildallxleroy2006-09-114-68/+209
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@91 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Encore une eta-expansion intempestivexleroy2006-09-111-4/+23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@90 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Traiter les initialisations x = NULLxleroy2006-09-081-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@89 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJxleroy2006-09-081-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@88 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suite de l'adaptation du front-end CILxleroy2006-09-084-267/+325
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@87 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJ des tests Cxleroy2006-09-088-61/+1082
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@86 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Stocker l'adresse de retour a l'offset 12 au lieu de l'offset 4 pour ↵xleroy2006-09-088-19/+19
| | | | | | meilleure compatibilite avec les conventions de MacOSX git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@85 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integration du front-end CIL developpe par Thomas Moniotxleroy2006-09-0722-119/+2688
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@84 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-04 00:42:53 +0000