Transition semantics for Clight and Csharpminor
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1119 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- backend/RTLgenproof.v 17 additions, 23 deletionsbackend/RTLgenproof.v
- cfrontend/Cminorgen.v 96 additions, 19 deletionscfrontend/Cminorgen.v
- cfrontend/Cminorgenproof.v 799 additions, 726 deletionscfrontend/Cminorgenproof.v
- cfrontend/Csem.v 876 additions, 99 deletionscfrontend/Csem.v
- cfrontend/Csharpminor.v 249 additions, 280 deletionscfrontend/Csharpminor.v
- cfrontend/Cshmgen.v 16 additions, 29 deletionscfrontend/Cshmgen.v
- cfrontend/Cshmgenproof1.v 38 additions, 64 deletionscfrontend/Cshmgenproof1.v
- cfrontend/Cshmgenproof2.v 38 additions, 72 deletionscfrontend/Cshmgenproof2.v
- cfrontend/Cshmgenproof3.v 869 additions, 1052 deletionscfrontend/Cshmgenproof3.v
- cfrontend/Csyntax.v 8 additions, 1 deletioncfrontend/Csyntax.v
- cfrontend/Ctyping.v 7 additions, 0 deletionscfrontend/Ctyping.v
Loading
Please register or sign in to comment