Added 'going wrong' behaviors
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- .depend 3 additions, 2 deletions.depend
- Makefile 1 addition, 1 deletionMakefile
- arm/Asmgenproof.v 1 addition, 1 deletionarm/Asmgenproof.v
- arm/Constpropproof.v 1 addition, 1 deletionarm/Constpropproof.v
- arm/Selectionproof.v 1 addition, 1 deletionarm/Selectionproof.v
- backend/Allocproof.v 1 addition, 1 deletionbackend/Allocproof.v
- backend/CSEproof.v 1 addition, 1 deletionbackend/CSEproof.v
- backend/Linearizeproof.v 1 addition, 1 deletionbackend/Linearizeproof.v
- backend/Machabstr2concr.v 3 additions, 3 deletionsbackend/Machabstr2concr.v
- backend/RTLgenproof.v 1 addition, 1 deletionbackend/RTLgenproof.v
- backend/Reloadproof.v 1 addition, 1 deletionbackend/Reloadproof.v
- backend/Stackingproof.v 1 addition, 1 deletionbackend/Stackingproof.v
- backend/Tailcallproof.v 1 addition, 1 deletionbackend/Tailcallproof.v
- backend/Tunneling.v 22 additions, 29 deletionsbackend/Tunneling.v
- backend/Tunnelingproof.v 113 additions, 108 deletionsbackend/Tunnelingproof.v
- backend/Tunnelingtyping.v 22 additions, 18 deletionsbackend/Tunnelingtyping.v
- cfrontend/Cminorgenproof.v 1 addition, 1 deletioncfrontend/Cminorgenproof.v
- cfrontend/Cshmgenproof3.v 7 additions, 6 deletionscfrontend/Cshmgenproof3.v
- common/Smallstep.v 34 additions, 11 deletionscommon/Smallstep.v
- driver/Compiler.v 32 additions, 30 deletionsdriver/Compiler.v
Loading
Please register or sign in to comment