aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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
* Permettre les casts entre types de fonctionxleroy2006-09-062-13/+21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@83 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Csem: l'hypothese de typage sur main est inutile (assuree par wt_program)xleroy2006-09-063-10/+21
| | | | | | | | Ctyping: relaxation de l'hypothese de typage sur main Cshmgenproof3: adaptation a ces changements. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@82 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout de dependances dans extraction/Makefiletristan2006-09-063-24/+32
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@80 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJxleroy2006-09-062-2/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@79 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Definition redondantexleroy2006-09-061-5/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@78 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu traitement des variables globales dans AST.program et dans Globalenvs.xleroy2006-09-0523-468/+538
| | | | | | | | Adaptation frontend, backend en consequence. Integration passe C -> C#minor dans common/Main.v. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@77 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ignorer les .vo dans cfrontend et commonxleroy2006-09-040-0/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@76 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ignorer les .vo dans cfrontend et commonxleroy2006-09-040-0/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@75 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Convenience commandxleroy2006-09-041-0/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@74 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu la repartition des sources Coq en sous-repertoiresxleroy2006-09-0412-67/+70
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@73 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion de la branche "traces":xleroy2006-09-0488-8418/+11331
| | | | | | | | | | | | | - Ajout de traces d'evenements d'E/S dans les semantiques - Ajout constructions switch et allocation dynamique - Initialisation des variables globales - Portage Coq 8.1 beta Debut d'integration du front-end C: - Traduction Clight -> Csharpminor dans cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout d'un type-checker (non certifie) pour Cminorxleroy2006-07-176-17/+397
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@51 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Declaration des variables avec .commxleroy2006-07-111-3/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@50 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout de fabsxleroy2006-07-111-0/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@49 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cast des litteraux de chaine en unsigned char *xleroy2006-07-112-12/+12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@48 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu sémantique de Eaddrof en Csharpminor: on peut prendre l'adresse de xleroy2006-07-113-165/+149
| | | | | | | | | globaux qui ne sont pas déclarés dans les variables du programme, notamment les fonctions. Adaptation de Cminorgen et de sa preuve en conséquence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@47 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Version C des tests Cminorxleroy2006-06-298-0/+1339
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@40 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJ suite aux changements dans Cminorgenxleroy2006-06-081-3/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@36 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout Sswitch dans Csharpminor. Renommage type variable_info -> var_kindxleroy2006-06-063-27/+61
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@35 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Optimisation des casts (idempotence, etc)xleroy2006-06-052-51/+121
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@33 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout construction Sswitch dans Cminorxleroy2006-06-051-8/+39
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@32 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout construction Sswitch dans Cminorxleroy2006-06-053-9/+103
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@31 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu gestion des variables globales dans Csharpminorxleroy2006-06-023-274/+457
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@30 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suppression de stmtlist dans Cminorxleroy2006-04-062-6/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@12 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Dans Cminor et Csharpminor: suppression de stmtlist, ajout de Sskip, Sseq.xleroy2006-04-069-349/+247
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@11 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suppression de stmtlist et de exec_stmtlist.xleroy2006-04-061-45/+31
| | | | | | | | Ajout de Sskip, Sseq. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@10 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Renommage List -> CList lors de l'extractionxleroy2006-03-096-229/+231
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@8 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PL: Un mot-cle Proof qui n'a rien a faire la...letouzey2006-02-161-1/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@5 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Propertiesxleroy2006-02-100-0/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@4 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-05 07:54:00 +0000