Commits · 30fbbdb86d2a2989062a9c82dc770a923fb19643 · CertiCompil / CompCert-KVX

Nov 10, 2009

Added support for jump tables in back end. · 74487f07

xleroy authored 15 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1171 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

74487f07

Jun 05, 2009

Adapted to work with Coq 8.2-1 · 615fb53c

xleroy authored 15 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

615fb53c

Apr 17, 2008

Amelioration compilation des switch · 9e2f7e70

xleroy authored 16 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@616 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

9e2f7e70

Jan 27, 2008

Ajout license, README, copyright notices · 877b4347

xleroy authored 17 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

877b4347

Aug 04, 2007

Fusion des modifications faites sur les branches "tailcalls" et "smallstep". · 355b4abc

xleroy authored 17 years ago

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

355b4abc