aboutsummaryrefslogtreecommitdiffstats
path: root/test/c
Commit message (Collapse)AuthorAgeFilesLines
...
* Protoizedxleroy2010-03-021-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1267 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo in Makefilexleroy2010-02-171-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1254 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Reorganization test directoryxleroy2010-02-173-72/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1253 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* 3 more benchmarksxleroy2010-02-177-1/+863
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1252 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Backtracking on commit 1220v1.6xleroy2010-01-131-0/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Test result more reproduciblexleroy2009-12-162-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1201 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support Clight initializers of the form "int * x = &y;".xleroy2009-11-011-0/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1162 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Problem with const enum initializersxleroy2009-09-152-0/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1146 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Stronger constant folding, esp. w.r.t. floatsxleroy2009-08-212-0/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1137 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Endianness in testsxleroy2009-01-052-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Continuation of PowerPC/EABI portxleroy2008-12-312-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@933 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Flag to turn on/off the recognition of fused multiply-add and multiply-subxleroy2008-07-311-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@706 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
* 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
* Compilo C, preprocesseur, assembleur sont determines par configure et mis ↵xleroy2008-04-191-2/+3
| | | | | | dans Makefile.config git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@622 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
* Problemes d'alignement des variables globales et a l'interieur de leurs ↵xleroy2007-10-313-3/+53
| | | | | | 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-0/+1
| | | | | | 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
* Rendu le test lists.c plus interessantxleroy2007-08-061-4/+30
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@388 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-043-13/+4
| | | | | | | | | | | | En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation ↵xleroy2007-03-021-0/+5
| | | | | | 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
* Ajout test mark&sweep GCxleroy2006-10-271-0/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@134 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout et utilisation de compcert_stdio.hxleroy2006-10-223-6/+12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@123 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
* Davantage de testsxleroy2006-09-1733-33/+3010
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@104 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
* 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
* Integration du front-end CIL developpe par Thomas Moniotxleroy2006-09-071-78/+62
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@84 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