aboutsummaryrefslogtreecommitdiffstats
path: root/caml/Cil2Csyntax.ml
Commit message (Collapse)AuthorAgeFilesLines
* Clight: ajout Econdition, suppression Eindex.xleroy2008-09-271-6/+3
| | | | | | | | caml/PrintCsyntax.ml: afficher les formes a[b] et a->fld. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@789 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
* Camlcoq.ml: interpret Caml's int32 as unsigned when converting to Integers.intxleroy2008-04-161-4/+5
| | | | | | | 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 license, README, copyright noticesxleroy2008-01-271-0/+16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Problemes d'alignement des variables globales et a l'interieur de leurs ↵xleroy2007-10-311-44/+61
| | | | | | initialiseurs git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@444 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les ↵xleroy2007-08-281-33/+55
| | | | | | 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
* Relaxation des contraintes sur les struct recursivesxleroy2006-10-231-13/+9
| | | | 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-221-15/+0
| | | | | | 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
* 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
* 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
* 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
* 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
* Revu traitement des structures et unions recursives. Dans Cshmgen, ↵xleroy2006-09-111-4/+9
| | | | | | meilleure compilation de exit_if_false. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@94 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
* Suite de l'adaptation du front-end CILxleroy2006-09-081-236/+258
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@87 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integration du front-end CIL developpe par Thomas Moniotxleroy2006-09-071-0/+863
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-05 12:18:58 +0000