summaryrefslogtreecommitdiff
path: root/caml/Cil2Csyntax.ml
Commit message (Collapse)AuthorAge
* Ajout license, README, copyright noticesGravatar xleroy2008-01-27
| | | | 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 ↵Gravatar xleroy2007-10-31
| | | | | | 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 ↵Gravatar xleroy2007-08-28
| | | | | | 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 recursivesGravatar xleroy2006-10-23
| | | | 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()Gravatar xleroy2006-10-23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@127 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Verification du type de retour de main()Gravatar xleroy2006-10-23
| | | | 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 ↵Gravatar xleroy2006-10-22
| | | | | | 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 ↵Gravatar xleroy2006-10-22
| | | | | | 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 fieldsGravatar xleroy2006-09-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@105 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bug dans le traitement des fonctions variadiques.Gravatar xleroy2006-09-17
| | | | | | | | | 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 ↵Gravatar xleroy2006-09-16
| | | | | | 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 ↵Gravatar xleroy2006-09-11
| | | | | | 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, ↵Gravatar xleroy2006-09-11
| | | | | | 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 = NULLGravatar xleroy2006-09-08
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@89 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suite de l'adaptation du front-end CILGravatar xleroy2006-09-08
| | | | 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 MoniotGravatar xleroy2006-09-07
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@84 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e