Revised back-end so that only 2 integer registers are reserved for reloading.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@925 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- .depend 1 addition, 1 deletion.depend
- backend/Allocproof.v 1 addition, 1 deletionbackend/Allocproof.v
- backend/Alloctyping.v 11 additions, 4 deletionsbackend/Alloctyping.v
- backend/Coloring.v 26 additions, 7 deletionsbackend/Coloring.v
- backend/Coloringproof.v 136 additions, 32 deletionsbackend/Coloringproof.v
- backend/Conventions.v 5 additions, 1 deletionbackend/Conventions.v
- backend/LTLintyping.v 4 additions, 5 deletionsbackend/LTLintyping.v
- backend/LTLtyping.v 8 additions, 4 deletionsbackend/LTLtyping.v
- backend/Lineartyping.v 1 addition, 1 deletionbackend/Lineartyping.v
- backend/Locations.v 8 additions, 8 deletionsbackend/Locations.v
- backend/Op.v 30 additions, 2 deletionsbackend/Op.v
- backend/PPC.v 4 additions, 4 deletionsbackend/PPC.v
- backend/PPCgen.v 39 additions, 39 deletionsbackend/PPCgen.v
- backend/PPCgenproof.v 14 additions, 14 deletionsbackend/PPCgenproof.v
- backend/PPCgenproof1.v 57 additions, 57 deletionsbackend/PPCgenproof1.v
- backend/Parallelmove.v 0 additions, 10 deletionsbackend/Parallelmove.v
- backend/Reload.v 69 additions, 23 deletionsbackend/Reload.v
- backend/Reloadproof.v 324 additions, 168 deletionsbackend/Reloadproof.v
- backend/Reloadtyping.v 42 additions, 21 deletionsbackend/Reloadtyping.v
- backend/Selectionproof.v 1 addition, 1 deletionbackend/Selectionproof.v
Loading
Please register or sign in to comment