-
- Downloads
- Added alignment constraints to memory loads and stores.
- In Cminor and below, removed pointer validity check in semantics of comparisons, so that evaluation of expressions is independent of memory state. - In Cminor and below, removed "alloc" instruction. - Cleaned up commented-away parts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- arm/Asm.v 0 additions, 14 deletionsarm/Asm.v
- arm/Asmgen.v 0 additions, 2 deletionsarm/Asmgen.v
- arm/Asmgenproof.v 3 additions, 63 deletionsarm/Asmgenproof.v
- arm/Asmgenproof1.v 7 additions, 110 deletionsarm/Asmgenproof1.v
- arm/Constprop.v 0 additions, 4 deletionsarm/Constprop.v
- arm/Constpropproof.v 74 additions, 84 deletionsarm/Constpropproof.v
- arm/Op.v 26 additions, 112 deletionsarm/Op.v
- arm/Selection.v 0 additions, 1 deletionarm/Selection.v
- arm/Selectionproof.v 18 additions, 30 deletionsarm/Selectionproof.v
- arm/linux/Conventions.v 0 additions, 4 deletionsarm/linux/Conventions.v
- backend/Allocation.v 0 additions, 4 deletionsbackend/Allocation.v
- backend/Allocproof.v 3 additions, 13 deletionsbackend/Allocproof.v
- backend/Alloctyping.v 0 additions, 2 deletionsbackend/Alloctyping.v
- backend/Bounds.v 1 addition, 3 deletionsbackend/Bounds.v
- backend/CSE.v 1 addition, 3 deletionsbackend/CSE.v
- backend/CSEproof.v 8 additions, 18 deletionsbackend/CSEproof.v
- backend/Cminor.v 13 additions, 32 deletionsbackend/Cminor.v
- backend/CminorSel.v 2 additions, 9 deletionsbackend/CminorSel.v
- backend/Coloring.v 0 additions, 6 deletionsbackend/Coloring.v
- backend/Coloringproof.v 0 additions, 47 deletionsbackend/Coloringproof.v
Loading
Please register or sign in to comment