summaryrefslogtreecommitdiff
path: root/test
Commit message (Collapse)AuthorAge
* Suppressed -fall-extensions option, too dangerous wrt flonglongGravatar xleroy2010-03-03
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1275 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated raytracer test. Added SPASS test.Gravatar xleroy2010-03-03
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Switching to the new C parser/elaborator/simplifierGravatar xleroy2010-03-03
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ProtoizedGravatar xleroy2010-03-02
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1268 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ProtoizedGravatar xleroy2010-03-02
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1267 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo in MakefileGravatar xleroy2010-02-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1254 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Reorganization test directoryGravatar xleroy2010-02-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1253 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* 3 more benchmarksGravatar xleroy2010-02-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1252 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Moved test harness C files hereGravatar xleroy2010-02-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1251 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Backtracking on commit 1220Gravatar xleroy2010-01-13
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Test result more reproducibleGravatar xleroy2009-12-16
| | | | 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;".Gravatar xleroy2009-11-01
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1162 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Problem with const enum initializersGravatar xleroy2009-09-15
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1146 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Stronger constant folding, esp. w.r.t. floatsGravatar xleroy2009-08-21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1137 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cil2Csyntax: added goto and labels; added assignment between structsGravatar xleroy2009-08-16
| | | | | | | | | | | | Kildall: simplified the interface Constprop, CSE, Allocation, Linearize: updated for the new Kildall RTL, LTL: removed the well-formedness condition on the CFG, it is no longer necessary with the new Kildall and it is problematic for validated optimizations. Maps: more efficient implementation of PTree.fold. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1124 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Elimination of "alloc" instruction in Caml files and test files.Gravatar xleroy2009-01-11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@946 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Test for int/float conversionsGravatar xleroy2009-01-07
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@943 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Endianness in testsGravatar xleroy2009-01-05
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Continuation of PowerPC/EABI portGravatar xleroy2008-12-31
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@933 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout nouveaux testsGravatar xleroy2008-08-09
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@708 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Flag to turn on/off the recognition of fused multiply-add and multiply-subGravatar xleroy2008-07-31
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@706 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update test resultsGravatar xleroy2008-07-31
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@704 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Augmenter le temps d'execution par defautGravatar xleroy2008-07-25
| | | | 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 ↵Gravatar xleroy2008-04-19
| | | | | | dans Makefile.config git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Amelioration compilation des switchGravatar xleroy2008-04-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@616 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout du test vmachGravatar xleroy2008-04-15
| | | | 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 ↵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
* Rendu le test lists.c plus interessantGravatar xleroy2007-08-06
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@388 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu MakefilesGravatar xleroy2007-08-06
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@387 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* DocumentationGravatar xleroy2007-08-05
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".Gravatar xleroy2007-08-04
| | | | | | | | | | | | 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 ↵Gravatar xleroy2007-03-02
| | | | | | 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
* NettoyageGravatar xleroy2007-03-02
| | | | 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 separesGravatar xleroy2007-03-02
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@180 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout test mark&sweep GCGravatar xleroy2006-10-27
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@134 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout test stop&copy GCGravatar xleroy2006-10-26
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@133 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout et utilisation de compcert_stdio.hGravatar xleroy2006-10-22
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@123 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Resolution d'un probleme (cf. big endian), etGravatar blazy2006-10-20
| | | | | | | | 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.Gravatar blazy2006-10-20
| | | | | | | | | | 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...Gravatar lrg2006-10-20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* interpreter for "little"Gravatar lrg2006-10-20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@119 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplification de Cminor: les affectations de variables locales ne sontGravatar xleroy2006-09-18
| | | | | | | | 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
* NettoyagesGravatar xleroy2006-09-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@108 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Davantage de testsGravatar xleroy2006-09-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@104 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout du test listsGravatar xleroy2006-09-11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@99 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJ des tests CGravatar xleroy2006-09-08
| | | | 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 MoniotGravatar xleroy2006-09-07
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@84 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion de la branche "traces":Gravatar xleroy2006-09-04
| | | | | | | | | | | | | - 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 de fabsGravatar xleroy2006-07-11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@49 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 16:04:08 +0000