Fusion des modifications faites sur les branches "tailcalls" et "smallstep".
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
Showing
- .depend 56 additions, 44 deletions.depend
- Makefile 24 additions, 16 deletionsMakefile
- backend/Allocation.v 88 additions, 294 deletionsbackend/Allocation.v
- backend/Allocproof.v 496 additions, 1475 deletionsbackend/Allocproof.v
- backend/Alloctyping.v 71 additions, 445 deletionsbackend/Alloctyping.v
- backend/Bounds.v 357 additions, 0 deletionsbackend/Bounds.v
- backend/CSE.v 5 additions, 3 deletionsbackend/CSE.v
- backend/CSEproof.v 210 additions, 139 deletionsbackend/CSEproof.v
- backend/Cminor.v 236 additions, 97 deletionsbackend/Cminor.v
- backend/CminorSel.v 296 additions, 0 deletionsbackend/CminorSel.v
- backend/Coloring.v 2 additions, 0 deletionsbackend/Coloring.v
- backend/Coloringproof.v 1 addition, 0 deletionsbackend/Coloringproof.v
- backend/Constprop.v 32 additions, 26 deletionsbackend/Constprop.v
- backend/Constpropproof.v 322 additions, 287 deletionsbackend/Constpropproof.v
- backend/Conventions.v 196 additions, 85 deletionsbackend/Conventions.v
- backend/LTL.v 242 additions, 262 deletionsbackend/LTL.v
- backend/LTLin.v 255 additions, 0 deletionsbackend/LTLin.v
- backend/LTLintyping.v 104 additions, 0 deletionsbackend/LTLintyping.v
- backend/LTLtyping.v 87 additions, 73 deletionsbackend/LTLtyping.v
- backend/Linear.v 138 additions, 105 deletionsbackend/Linear.v
Loading
Please register or sign in to comment