Cil2Csyntax: added goto and labels; added assignment between structs
Kildall: simplified the interface Constprop, CSE, Allocation, Linearize: updated for the new Kildall RTL, LTL: removed the well-formedness condition on the CFG, it is no longer necessary with the new Kildall and it is problematic for validated optimizations. Maps: more efficient implementation of PTree.fold. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1124 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- arm/Constprop.v 2 additions, 17 deletionsarm/Constprop.v
- arm/Constpropproof.v 17 additions, 20 deletionsarm/Constpropproof.v
- backend/Allocation.v 2 additions, 14 deletionsbackend/Allocation.v
- backend/Allocproof.v 9 additions, 12 deletionsbackend/Allocproof.v
- backend/CSE.v 2 additions, 18 deletionsbackend/CSE.v
- backend/CSEproof.v 17 additions, 27 deletionsbackend/CSEproof.v
- backend/Kildall.v 264 additions, 203 deletionsbackend/Kildall.v
- backend/LTL.v 14 additions, 17 deletionsbackend/LTL.v
- backend/Linearize.v 0 additions, 1 deletionbackend/Linearize.v
- backend/Linearizeaux.ml 2 additions, 1 deletionbackend/Linearizeaux.ml
- backend/Linearizeproof.v 12 additions, 19 deletionsbackend/Linearizeproof.v
- backend/RTL.v 19 additions, 16 deletionsbackend/RTL.v
- backend/RTLgen.v 1 addition, 3 deletionsbackend/RTLgen.v
- backend/RTLgenspec.v 2 additions, 4 deletionsbackend/RTLgenspec.v
- backend/RTLtyping.v 1 addition, 1 deletionbackend/RTLtyping.v
- backend/Tunneling.v 1 addition, 13 deletionsbackend/Tunneling.v
- cfrontend/Cil2Csyntax.ml 164 additions, 64 deletionscfrontend/Cil2Csyntax.ml
- cfrontend/PrintCsyntax.ml 6 additions, 0 deletionscfrontend/PrintCsyntax.ml
- extraction/Kildall.ml.patch 14 additions, 33 deletionsextraction/Kildall.ml.patch
- lib/Lattice.v 0 additions, 3 deletionslib/Lattice.v
Loading
Please register or sign in to comment