Fusion de la branche "traces":
- 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
Showing
- .depend 39 additions, 31 deletions.depend
- Makefile 11 additions, 7 deletionsMakefile
- backend/AST.v 65 additions, 31 deletionsbackend/AST.v
- backend/Allocation.v 25 additions, 16 deletionsbackend/Allocation.v
- backend/Allocproof.v 218 additions, 118 deletionsbackend/Allocproof.v
- backend/Allocproof_aux.v 0 additions, 850 deletionsbackend/Allocproof_aux.v
- backend/Alloctyping.v 62 additions, 12 deletionsbackend/Alloctyping.v
- backend/Alloctyping_aux.v 0 additions, 895 deletionsbackend/Alloctyping_aux.v
- backend/CSE.v 14 additions, 1 deletionbackend/CSE.v
- backend/CSEproof.v 101 additions, 33 deletionsbackend/CSEproof.v
- backend/Cmconstr.v 46 additions, 5 deletionsbackend/Cmconstr.v
- backend/Cmconstrproof.v 385 additions, 342 deletionsbackend/Cmconstrproof.v
- backend/Cminor.v 117 additions, 90 deletionsbackend/Cminor.v
- backend/Cminorgen.v 45 additions, 29 deletionsbackend/Cminorgen.v
- backend/Cminorgenproof.v 645 additions, 564 deletionsbackend/Cminorgenproof.v
- backend/Coloring.v 6 additions, 0 deletionsbackend/Coloring.v
- backend/Coloringproof.v 47 additions, 2 deletionsbackend/Coloringproof.v
- backend/Constprop.v 23 additions, 1 deletionbackend/Constprop.v
- backend/Constpropproof.v 68 additions, 44 deletionsbackend/Constpropproof.v
- backend/Conventions.v 65 additions, 50 deletionsbackend/Conventions.v
Loading
Please register or sign in to comment