More realistic treatment of jump tables: show the absence of overflow when accessing the table
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1172 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- backend/LTLintyping.v 2 additions, 0 deletionsbackend/LTLintyping.v
- backend/LTLtyping.v 2 additions, 0 deletionsbackend/LTLtyping.v
- backend/Lineartyping.v 2 additions, 0 deletionsbackend/Lineartyping.v
- backend/Machtyping.v 1 addition, 0 deletionsbackend/Machtyping.v
- backend/RTLtyping.v 4 additions, 2 deletionsbackend/RTLtyping.v
- backend/Tunnelingtyping.v 2 additions, 1 deletionbackend/Tunnelingtyping.v
- lib/Coqlib.v 7 additions, 0 deletionslib/Coqlib.v
- lib/Integers.v 7 additions, 0 deletionslib/Integers.v
- powerpc/Asm.v 9 additions, 6 deletionspowerpc/Asm.v
- powerpc/Asmgen.v 2 additions, 1 deletionpowerpc/Asmgen.v
- powerpc/Asmgenproof.v 39 additions, 13 deletionspowerpc/Asmgenproof.v
- powerpc/PrintAsm.ml 1 addition, 2 deletionspowerpc/PrintAsm.ml
Loading
Please register or sign in to comment