Lever la restriction sur les fonctions externes, restriction qui exigeait que...
Lever la restriction sur les fonctions externes, restriction qui exigeait que tous les arguments resident en registres git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- backend/Allocation.v 1 addition, 9 deletionsbackend/Allocation.v
- backend/Allocproof.v 2 additions, 4 deletionsbackend/Allocproof.v
- backend/Alloctyping.v 2 additions, 4 deletionsbackend/Alloctyping.v
- backend/Conventions.v 0 additions, 23 deletionsbackend/Conventions.v
- backend/LTLtyping.v 0 additions, 1 deletionbackend/LTLtyping.v
- backend/Lineartyping.v 0 additions, 1 deletionbackend/Lineartyping.v
- backend/Mach.v 21 additions, 1 deletionbackend/Mach.v
- backend/Machabstr.v 22 additions, 2 deletionsbackend/Machabstr.v
- backend/Machabstr2mach.v 26 additions, 1 deletionbackend/Machabstr2mach.v
- backend/Machtyping.v 0 additions, 1 deletionbackend/Machtyping.v
- backend/PPC.v 29 additions, 27 deletionsbackend/PPC.v
- backend/PPCgenproof.v 3 additions, 5 deletionsbackend/PPCgenproof.v
- backend/PPCgenproof1.v 57 additions, 40 deletionsbackend/PPCgenproof1.v
- backend/RTLtyping.v 0 additions, 19 deletionsbackend/RTLtyping.v
- backend/Stackingproof.v 45 additions, 2 deletionsbackend/Stackingproof.v
- backend/Stackingtyping.v 1 addition, 1 deletionbackend/Stackingtyping.v
- caml/Cil2Csyntax.ml 0 additions, 15 deletionscaml/Cil2Csyntax.ml
- extraction/.depend 15 additions, 10 deletionsextraction/.depend
- lib/Coqlib.v 43 additions, 1 deletionlib/Coqlib.v
Loading
Please register or sign in to comment