More faithful semantics for volatile reads and writes.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1346 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- .depend 1 addition, 1 deletion.depend
- Changelog 7 additions, 0 deletionsChangelog
- arm/Asm.v 1 addition, 1 deletionarm/Asm.v
- arm/Asmgenproof.v 11 additions, 2 deletionsarm/Asmgenproof.v
- backend/Allocproof.v 10 additions, 1 deletionbackend/Allocproof.v
- backend/CSEproof.v 6 additions, 1 deletionbackend/CSEproof.v
- backend/Cminor.v 2 additions, 2 deletionsbackend/Cminor.v
- backend/CminorSel.v 1 addition, 1 deletionbackend/CminorSel.v
- backend/Constpropproof.v 9 additions, 1 deletionbackend/Constpropproof.v
- backend/LTL.v 1 addition, 1 deletionbackend/LTL.v
- backend/LTLin.v 1 addition, 1 deletionbackend/LTLin.v
- backend/Linear.v 1 addition, 1 deletionbackend/Linear.v
- backend/Linearizeproof.v 6 additions, 1 deletionbackend/Linearizeproof.v
- backend/Machabstr.v 1 addition, 1 deletionbackend/Machabstr.v
- backend/Machabstr2concr.v 6 additions, 6 deletionsbackend/Machabstr2concr.v
- backend/Machconcr.v 1 addition, 1 deletionbackend/Machconcr.v
- backend/RTL.v 1 addition, 1 deletionbackend/RTL.v
- backend/RTLgenproof.v 7 additions, 1 deletionbackend/RTLgenproof.v
- backend/Reloadproof.v 6 additions, 1 deletionbackend/Reloadproof.v
- backend/Selectionproof.v 9 additions, 1 deletionbackend/Selectionproof.v
Loading
Please register or sign in to comment