Revu traitement des variables globales dans AST.program et dans Globalenvs.
Adaptation frontend, backend en consequence. Integration passe C -> C#minor dans common/Main.v. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@77 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- backend/CSEproof.v 2 additions, 2 deletionsbackend/CSEproof.v
- backend/Cminor.v 1 addition, 1 deletionbackend/Cminor.v
- backend/Constpropproof.v 2 additions, 2 deletionsbackend/Constpropproof.v
- backend/LTL.v 1 addition, 1 deletionbackend/LTL.v
- backend/Linear.v 1 addition, 1 deletionbackend/Linear.v
- backend/Linearizeproof.v 3 additions, 3 deletionsbackend/Linearizeproof.v
- backend/Mach.v 1 addition, 1 deletionbackend/Mach.v
- backend/PPC.v 1 addition, 1 deletionbackend/PPC.v
- backend/RTL.v 1 addition, 1 deletionbackend/RTL.v
- backend/RTLtyping.v 2 additions, 2 deletionsbackend/RTLtyping.v
- backend/Tunnelingproof.v 3 additions, 3 deletionsbackend/Tunnelingproof.v
- cfrontend/Cminorgen.v 6 additions, 4 deletionscfrontend/Cminorgen.v
- cfrontend/Cminorgenproof.v 13 additions, 15 deletionscfrontend/Cminorgenproof.v
- cfrontend/Csem.v 2 additions, 8 deletionscfrontend/Csem.v
- cfrontend/Csharpminor.v 5 additions, 15 deletionscfrontend/Csharpminor.v
- cfrontend/Cshmgen.v 6 additions, 15 deletionscfrontend/Cshmgen.v
- cfrontend/Cshmgenproof1.v 11 additions, 29 deletionscfrontend/Cshmgenproof1.v
- cfrontend/Cshmgenproof3.v 27 additions, 30 deletionscfrontend/Cshmgenproof3.v
- cfrontend/Csyntax.v 1 addition, 16 deletionscfrontend/Csyntax.v
- cfrontend/Ctyping.v 4 additions, 4 deletionscfrontend/Ctyping.v
Loading
Please register or sign in to comment