Simplification de Cminor: les affectations de variables locales ne sont
plus des expressions mais des statements (Eassign -> Sassign). Cela simplifie les preuves et ameliore la qualite du RTL produit. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@111 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- backend/Cmconstr.v 0 additions, 1 deletionbackend/Cmconstr.v
- backend/Cmconstrproof.v 290 additions, 290 deletionsbackend/Cmconstrproof.v
- backend/Cminor.v 79 additions, 81 deletionsbackend/Cminor.v
- backend/RTLgen.v 50 additions, 97 deletionsbackend/RTLgen.v
- backend/RTLgenproof.v 204 additions, 259 deletionsbackend/RTLgenproof.v
- backend/RTLgenproof1.v 66 additions, 152 deletionsbackend/RTLgenproof1.v
- caml/CMparser.mly 1 addition, 1 deletioncaml/CMparser.mly
- caml/CMtypecheck.ml 8 additions, 9 deletionscaml/CMtypecheck.ml
- cfrontend/Cminorgen.v 2 additions, 2 deletionscfrontend/Cminorgen.v
- cfrontend/Cminorgenproof.v 82 additions, 84 deletionscfrontend/Cminorgenproof.v
- test/cminor/aes.cmp 10 additions, 5 deletionstest/cminor/aes.cmp
Loading
Please register or sign in to comment